Rebeca uses actor-based concepts for the specification of reactive systems and their communications. It introduces components as an additional structure for verification purposes.
Rebeca provides a formal semantics for the model and components, comprising their states, communications, state transitions, and the knowledge of accessible interfaces.
Rebeca models can be directly model checked using RMC. Translating Rebeca models into target languages of existing model checkers is also supported, making it possible to model check open, distributed systems using your favorite model checker.
Rebeca uses different abstraction techniques, which preserve a set of behavioral specification in temporal logic, and reduce the state space of a model, making it more suitable for model checking techniques.
Soundness of abstraction techniques is established by proving a weak simulation relation between the constructs. This enables the Rebeca Model Checker to apply a compositional verification approach, using the specified abstraction techniques.