Rebeca (Reactive Objects Language) is an actor-based 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 Rebeca Verifier tool, as a front-end, to translate the codes into existing model-checker languages and thus, be 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.
Rebeca is an actor-based language for modeling and verification of reactive systems. Modeling a system in Rebeca requires one to specify reactive-object templates and a finite set of object instances that run in parallel. Properties can be specified in temporal logic. Different approaches are proposed for verifying correctness of these properties.
Professor, School of Computer Science, Mälardalen University, School of IDT, Västerås, Sweden
email marjan.sirjani "at" mdh.se
Assistant Professor, School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran
email r.khosravi "at" ut.ac.ir
Assistant Professor, School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran
email fghassemi "at" ut.ac.ir
Postdoc Researcher, School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran
email e.khamespanah "at" ut.ac.ir
Master Student, School of Computer Engineering, Sharif University of Technology, Tehran, Iran
email faryousefi "at" ce.sharif.edu
Postdoc Researcher, School of Computer Science, Reykjavik University, Reykjavik, Iceland
email ali11 "at" ru.is