Rebeca Verifier (Roudabeh)
is a visual tool developed using Java language. In addition to
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
Updated: Wednesday 27 December 2006
Current Version: 1.2.7
Installation: java -jar Roudabeh-1.2.7_installer.jar
Some examples are provided in the tool.