Rebeca (acronym for Reactive Objects Language) is an
actor
An actor or actress is a person who portrays a character in a performance. The actor performs "in the flesh" in the traditional medium of the theatre or in modern media such as film, radio, and television. The analogous Greek term is (), l ...
-based
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. The rules are used for interpretation of the meaning of components in the ...
with a formal foundation, designed in an effort to bridge the gap between
formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal met ...
approaches and real applications. It can be considered as a reference model for
concurrent computation
Concurrent computing is a form of computing in which several computations are executed '' concurrently''—during overlapping time periods—instead of ''sequentially—''with one completing before the next starts.
This is a property of a syst ...
, 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 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.
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
*
Formal methods
In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the exp ...
*
Model checking
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software system ...
*
SPIN model checker
SPIN is a general tool for verifying the correctness of concurrent 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 a ...
References
* M. Sirjani. Formal Specification and Verification of Concurrent and Reactive Systems
PhD Thesis Department of Computer Engineering, Sharif University of Technology, December 2004.
* M. Sirjani, A. Movaghar. An Object-Based Model for Agents, in Proceedings of Workshop on Agents for Information Management, Austrian Computer Society, October 2002.
External links
Rebeca Home PageFormal Methods Laboratory, University of Tehran
Logic programming languages
{{compu-lang-stub