Rebeca is an actor-based language with a formal foundation for modeling concurrent and distributed systems which is designed in an effort to bridge the gap between formal verification approaches and real applications. Rebeca is supported by a tool-set for model checking Rebeca models. Inherent characteristics of Rebeca are used to introduce compositional verification, abstraction, symmetry and partial order reduction techniques for reducing the state space. Simple message-driven object-based computational model, Java-like syntax, and set of verification tools make Rebeca an interesting and easy-to-learn model for practitioners. This paper is to present theories, applications, and supporting tools of Rebeca in a consistent and distilled form.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Yousefi, Behnaz; Ghassemi, Fatemeh; Khosravi, Ramtin: Modeling and efficient verification of broadcasting actors (2015)
- De Boer, Frank; Jaghoori, Mahdi; Laneve, Cosimo; Zavattaro, Gianluigi: Decidability problems for actor systems (2014)
- de Boer, Frank S.; Grabe, Immo; Steffen, Martin: Termination detection for active objects (2012)
- Jaghoori, Mohammad Mahdi; Sirjani, Marjan; Mousavi, Mohammad Reza; Khamespanah, Ehsan; Movaghar, Ali: Symmetry and partial order reduction techniques in model checking Rebeca (2010)
- Sirjani, Marjan: Rebeca: Theory, applications, and tools (2007) ioport