Rebeca Modeling Language
Encyclopedia
Rebeca 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 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.
Besides having an appropriate and efficient way for modeling concurrent and distributed systems, one needs a formal verification approach to ensure their correctness. Rebeca is supported by a set of verification tools. Earlier tools provide a front-end to work with the Rebeca code, and translate the Rebeca codes into the input language of well-known and mature model checkers (like SPIN and NuSMV) and thus, are able to verify their properties.
Rebeca, since 2005, is supported by a direct model checker based on Modere (the Model checking Engine of Rebeca).
Modular verification and abstraction techniques are used to reduce the state space and make it possible to verify complicated reactive systems.
Besides these techniques, Modere supports partial order reduction and symmetry reduction.
Actor model
In computer science, the Actor model is a mathematical model of concurrent computation that treats "actors" as the universal primitives of concurrent digital computation: in response to a message that it receives, an actor can make local decisions, create more actors, send more messages, and...
-based modeling language
Modeling language
A modeling language is any artificial language that can be used to express information or knowledge or systems in a structure that is defined by a consistent set of rules...
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.
Besides having an appropriate and efficient way for modeling concurrent and distributed systems, one needs a formal verification approach to ensure their correctness. Rebeca is supported by a set of verification tools. Earlier tools provide a front-end to work with the Rebeca code, and translate the Rebeca codes into the input language of well-known and mature model checkers (like SPIN and NuSMV) and thus, are able to verify their properties.
Rebeca, since 2005, is supported by a direct model checker based on Modere (the Model checking Engine of Rebeca).
Modular verification and abstraction techniques are used to reduce the state space and make it possible to verify complicated reactive systems.
Besides these techniques, Modere supports partial order reduction and symmetry reduction.
See also
- Software engineeringSoftware engineeringSoftware Engineering is the application of a systematic, disciplined, quantifiable approach to the development, operation, and maintenance of software, and the study of these approaches; that is, the application of engineering to software...
- Actor modelActor modelIn computer science, the Actor model is a mathematical model of concurrent computation that treats "actors" as the universal primitives of concurrent digital computation: in response to a message that it receives, an actor can make local decisions, create more actors, send more messages, and...
- Formal methodsFormal methodsIn computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
- Model checkingModel checkingIn computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
- SPIN model checkerSPIN model checkerSPIN is a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980...