Rebeca (acronym for Reactive Objects Language) 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 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.
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.
rebeca, programming, language, this, article, multiple, issues, please, help, improve, discuss, these, issues, talk, page, learn, when, remove, these, template, messages, this, article, includes, list, references, related, reading, external, links, sources, re. This article has multiple issues Please help improve it or discuss these issues on the talk page Learn how and when to remove these template messages This article includes a list of references related reading or external links but its sources remain unclear because it lacks inline citations Please help improve this article by introducing more precise citations August 2019 Learn how and when to remove this template message The topic of this article may not meet Wikipedia s general notability guideline Please help to demonstrate the notability of the topic by citing reliable secondary sources that are independent of the topic and provide significant coverage of it beyond a mere trivial mention If notability cannot be shown the article is likely to be merged redirected or deleted Find sources Rebeca programming language news newspapers books scholar JSTOR January 2021 Learn how and when to remove this template message Learn how and when to remove this template message Rebeca acronym for Reactive Objects Language 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 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 editFormal methods Model checking SPIN model checkerReferences editM 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 editRebeca Home Page Formal Methods Laboratory University of Tehran nbsp This programming language related article is a stub You can help Wikipedia by expanding it vte Retrieved from https en wikipedia org w index php title Rebeca programming language amp oldid 1169890235, wikipedia, wiki, book, books, library,
