Event-B.org

Home of Event-B and the Rodin Platform

Deploy Logo

FP7 Logo

SourceForge.net Logo

 

Rodin Plug-ins

Plug-ins are installed from within Rodin. Select Help/Software Updates. The choose the "Available Software" tab and a list of update sites will appear. Select the appropriate update site from the list. The table below lists various plug-ins with details of which update site to use.

Name

Description

Installation

Atelier B Provers

The Atelier B Provers provide additional automated proof facilities to the existing Rodin provers. They come from the Atelier B tool for the B Method.

  • Select the Atelier B Provers update site.

UML-B

Provides a UML-like graphical front-end for Event-B modelling. It adds class oriented and state machine modelling capabilities. UML-B is automatically translated into Event-B for analysis and verification.

  • Select UML-B from the Main Rodin Update site.

ProB

Tool for automatic animation of EventB models  and can be used to systematically check a model for errors. In addition it can assist the proving process and can be used as a disprover on individual proof obligations. The plug-in is based on the ProB model checker for the B Method.
  • Select ProB from the www.stups.uni-duesseldorf.de Update site

AnimB

AnimB is an animator for the Rodin platform. It allows animation of complete model (all refinements), and can be used to create a complex animation with graphical interface

B2Rodin

Enables the importation of Atelier B models into Rodin.
Only event B compliant models are supported.

  • Select the B2rodin update site. See instructions here

B2Latex

Plug-in producing latex printing of event B models.

  • Install/upgrade using Main Rodin Update site.
  • After installation, you will see an L button on the menu bar in the Event-B perspective. Select the Machine or Context you want to translate to Latex and then press the L button. A latex file will be generated in a folder named Latex in your Event-B project directory.
  • bsymb.sty is required to process the latex.

Brama

Brama enables animating B models within Rodin Platform. Animation capabilities are twofold: first, debugging B models: the design can verify by experiment that a model and a system have similar behaviour. Second, connecting B models with flash animation: B models are used to trigger flash animation.
  • Install/upgrade using the update site bmethod.com/update_site/brama. See instructions here

Mobility

Used for the automatic verification of mobile agent systems. Implements a newly developed high level programming notation, hybrid of Event-B combined with constructs inspired by two process algebras (KLAIM and pi-calculus).. Furthermore, the tool is capable of model checking Event-B specifications (deadlock detection and invariants checks). The model checking engine is based on Petri nets unfoldings.

 

 

 

 

Event-B.org