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 9 articles )
Showing results 1 to 9 of 9.
- Abbasi, Rosa; Ghassemi, Fatemeh; Khosravi, Ramtin: Verification of asynchronous systems with an unspecified component (2019)
- Karami, Farzane; Owe, Olaf; Ramezanifarkhani, Toktam: An evaluation of interaction paradigms for active objects (2019)
- Yousefi, Behnaz; Ghassemi, Fatemeh; Khosravi, Ramtin: Modeling and efficient verification of wireless ad hoc networks (2017)
- Sirjani, Marjan; Khamespanah, Ehsan: On time actors (2016)
- Yousefi, Behnaz; Ghassemi, Fatemeh; Khosravi, Ramtin: Modeling and efficient verification of broadcasting actors (2015) ioport
- 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