Rebeca (programming language): Difference between revisions

Revision as of 03:04, 8 March 2009

Latest revision as of 23:22, 11 August 2023

(23 intermediate revisions by 15 users not shown)

Line 1:

{{Multiple issues|

{{Unreferenced|date=March 2009}}

{{No footnotes|date=August 2019}}

'''Rebeca''' (<u>'''Re'''</u>active O<u>'''b'''</u>j<u>'''ec'''</u>ts L<u>'''a'''</u>nguage) is an [[Actor model|actor]]-based [[programming 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.

{{Notability|date=January 2021}}

}}

'''Rebeca''' (<u>'''Re'''</u>activeacronym O<u>'''b'''</u>j<u>'''ec'''</u>tsfor L<u>'''a'''</u>nguageReactive Objects Language) is an [[Actor model|actor]]-based [[programmingmodeling 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 computing|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.

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 Rebecaa Verifierset tool,of verification tools. asEarlier tools provided a front-end, to translatework thewith codesRebeca intocode, existingand model-checkerto languagestranslate andthe thus,Rebeca becode ableinto toinput verifylanguages theirof properties. Modular verificationwell-known and abstractionmature techniquesmodel arecheckers used(like toSPIN reduceand the state spaceNuSMV) and makethus, itwere possibleable to verify complicatedtheir reactive systemsproperties.

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 ==

* [[Software engineering]]

* [[Actor model]]

* [[Formal methods]]

* [[Model checking]]

* [[SPIN model checker]]

== References ==

* M. Sirjani. Formal Specification and Verification of Concurrent and Reactive Systems, [http://ece.ut.ac.ir/msirjani/publications/SirjaniThesis.pdf 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 ==

* [http://khorshidwww.ut.ac.ir/~rebeca/-lang.org Rebeca Home Page]

* [http://ece.ut.ac.ir/FML/ Formal Methods Laboratory, University of Tehran]

[[Category:LogicConcurrent programming languages]]