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. |
|
