Rebeca (Reactive Objects Language) is an actor-based language with a formal foundation, designed in an effort to bridge the gap between formal verification approaches and real applications. It can be considered as a reference model for concurrent computation, based on an operational interpretation of the actor model. It is also a platform for developing object-based concurrent systems in practice. Learn More
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.