Rebeca Verifier (Roudabeh)
is a visual tool developed using Java language. In addition to
integrating R2SMV tool in a visual
environment, Roudabeh can extract component models from closed-world models
automatically, verify them and show the results in graphical window. Here is
the list of features:
- Rebeca model editor - For writing, saving and editing Rebeca models.
- Includes R2SMV - The tool can convert Rebeca models automatically to SMV codes.
- Automatic topology extraction - The tool can read the Rebeca model, and discover the different rebecs participating in the system, and find out which rebec is bound to which of the other ones.
- Graphical view of topology - System topology can be viewed graphically as a graph, with the nodes representing rebecs, and edges representing binding between them.
- Automatic component model generation - After the user selects the rebecs which shall be included in a component, the tool can automatically generate a component Rebeca model for the part of the system chosen by the user. The environment is extracted from the whole system, according to the rebecs in the components. Translation to SMV can be done automatically.
- Rebeca Property Parser - User can provide the properties of the system to be proved, based on variables in the Rebeca model. Property parser will translate it automatically into NuSMV property specifications.
- Integration with NuSMV - (to be done) The tool run NuSMV in the background, manage the input/output of the program and use it for model checking Rebeca models which are translated to SMV. The result of verification is displayed in another window in Roudabeh after it is completed.
Download
Updated: Wednesday 27 December 2006
Current Version: 1.2.7
Download:
Roudabeh-1.2.7_installer.jar
Installation: java -jar Roudabeh-1.2.7_installer.jar
Documentation
Some examples are provided in the tool.