Afra
Afra is a tool developed in the context of the project Sysfier. It includes
- Rebeca Model Checker (RMC)
- ReUML
- SyMon
Download Afra 1.4.2 (117MB, Feb 2009)
Afra with SystemC support
Afra is a tool developed in the context of the project Sysfier. The goal of Sysfier is to develop an integrated environment for modeling and verifying SystemC designs by formalizing SystemC semantics and providing model checking tools. The tool Afra is developed to integrate Sytra, Modere and SyMon in addition to Rebeca and SystemC modeling environments. Afra gets SystemC models and LTL or CTL properties from the designer, and verifies the models. If a property is not satisfied, a counter-example is displayed. For verifying SystemC models, Afra translates SystemC codes to Rebeca using Sytra. It then utilizes the Rebeca verification tool set to verify the given properties. Where applicable, reduction techniques are used to tackle the state explosion problem.
Contact Marjan Sirjani for more information.
Rebeca Model Checker Engine (RMC)
Rebeca Model Checker is a tool for direct model checking of Rebeca models, without using back-end model checkers. Properties can be specified based on state variables of rebecs. The first direct model checker of Rebeca is Modere, developed in 2005. Modere performs LTL model checking on Rebeca models. In the new releases, the architecture of RMC has been re-engineered to make it more extensible and reusable in different contexts. The model checker algorithm, the mechanism for storing the state space, and the translator of the input model are separated and decoupled, hence making the tool more flexible.
Modere: The Model Checking Engine of Rebeca
The Model checking Engine of Rebeca (Modere) is the part of Rebeca model checker that performs the LTL model checking. Modere uses the automata-theoretic method for model checking. In this method, the system and the negation of the specification are specified each with a Buchi automaton. The system satisfies the specification iff the language of the automata generated by the synchronous product of these two automata is empty. Otherwise, the product automata has an accepting cycle (a cycle reachable from the initial state and containing at least one accepting state) that shows the undesired behavior of the system. Given a Rebeca model, the Rebeca model checker generates the automata for the system and the negation of the specification, as C++ classes (in separate files). These files are placed automatically beside the file that contains the engine of Modere. The whole package must be compiled to produce an executable for model checking the given Rebeca model.
State-space reduction
The generated C++ files include special pieces of code for partial order and symmetry reduction. These parts are surrounded by compiler directives. Thus, by defining the proper compiler directives, the modeler can enable each reduction technique. Compiling these files then generates an executable that is optimized for the pre-selected reduction method(s).
In partial-order reduction, the reduction points (i.e., safe actions) are statically computed which will be used if the reduction is selected at model checking time. The symmetry technique, however, consists of two phases: detection and reduction. Detection can be based on inter- or intra-rebec symmetry. The former looks for symmetries in the static communication graph of the rebecs (formed using the known-rebec relation). The latter, additionally, looks into the each rebec definition to find internal symmetries; the internal symmetries should be made explicit by the modeler using scalar-sets. For either of the detection techniques, one can statically compute the symmetries and use them for a thorough reduction, called the "naive" approach. Alternatively, one can choose to use the "on-the-fly" detection and reduction method. The on-the-fly approach is usually faster but less efficient in terms of reduction.
The current release version of the tool is available here. To process the examples provided (from our publication in Acta Informatica) please read the instructions first.
Sarir
Sarir tool, is a Rebeca to mcrl2 compiler.
Download Sarir 1.0 (25KB, April 2007)
ReUML
ReUML Designer is developed for UML modelers and Rebeca developers. It lets UML modelers to verify their models without being concerned about details of Rebeca, and it allows Rebeca developers to model their systems with UML and use automatic code generation.
The tool has been developed using Java language, so it is portable and can be run on any platform that has a Java Runtime Environment support.
Current version of this tool support the following features in Rebeca model.
- Reactive Classes
- Main (system description)
- Known objects
- Message Servers
- State Variables
- Parameter passing in Message Servers
- Non-deterministic choice
- Asynchronous messages between Rebecs
- Synchronous messages between Rebeca model and external systems
- Per rebec queue length
Download ReUML Designer 1.0 (April 2007, 205KB)
Other tools
The following tools are not maintained anymore.
Rebeca Verifier
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 b27 December 2006e 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 Roudabeh 1.2.7 (3.6MB, December 2006)
Download documentation
Rebeca to Promela
Rebeca to Promela translator, is a tool for automatic translation of Rebeca models into Promela codes, so that the model can be verified with SPIN model checker.
The tool has been developed using Java language, so it is portable and can be run on any platform that has a Java Runtime Environment support.
Current version of this tool support the following features in Rebeca model:
- Reactive Classes
- Main (system description)
- Known objects
- Message Servers
- State Variables
- Boolean variable type
- Integer variable type
- Single parameter passing in Message Servers
- Non-deterministic choice
- Synchronous Messages (as rendezvous) between Rebecs (provided for extended-Rebeca)
Download Rebeca2Promela 2.4.1 (490KB, June 2007)
Rebeca to SMV
Rebeca to SMV translator, is a tool for automatic translation of Rebeca models into SMV codesl, so that the model can be verified with NuSMV model checker.
The tool has been developed using Java language, so it is portable and can be run on any platform that has a Java Runtime Environment support.
Current version of this tool support the following features in Rebeca model:
- (Re)Active Classes
- Main (system description)
- Known objects
- Message Servers
- State Variables
- Boolean variable type