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 now 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 (cycle with an 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.