RMC: Rebeca Model Checking Engine


RMC is a tool for direct model checking of Rebeca models, without using back-end model checkers. The first direct model checker of Rebeca is Modere, developed in 2005. Modere performs LTL model checking for 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 checking 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.


Detailed Description

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.