Rebeca (acronym for Reactive Objects Language) is an actor-based modeling language with a formal foundation, designed in an effort to bridge the gap between formal verification approaches and real applications.
It is also a platform for developing object-based concurrent systems in practice.
Besides having an appropriate and efficient way for modeling concurrent and distributed systems, one needs a formal verification approach to ensure their correctness.
Earlier tools provided a front-end to work with Rebeca code, and to translate the Rebeca code into input languages of well-known and mature model checkers (like SPIN and NuSMV) and thus, were able to verify their properties.
Modular verification and abstraction techniques are used to reduce the state space and make it possible to verify complicated reactive systems.