Rebeca Modeling Language

Actor-based Language with Formal Foundation

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

dashboard

Actors and Components

Rebeca uses actor-based concepts for the specification of reactive systems and their communications. It introduces components as an additional structure for verification purposes.

settings

Formal Semantics

Rebeca provides a formal semantics for the model and components, comprising their states, communications, state transitions, and the knowledge of accessible interfaces.

playlist_add_check

Model Checker

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.

filter_list

Abstraction

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.

done_all

Compositional Verification

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.

lock_open

Open Source