Rebeca (programming language): Difference between revisions

Revision as of 12:33, 17 July 2006

Latest revision as of 23:22, 11 August 2023

(34 intermediate revisions by 21 users not shown)

Line 1:

{{Multiple issues|

'''Rebeca''' (<u>Re</u>active O<u>b</u>j<u>ec</u>ts L<u>a</u>nguage) 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.

{{No footnotes|date=August 2019}}

<br/>

{{Notability|date=January 2021}}

Besides having an appropriate and efficient way for modelling 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''' (<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 [[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 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 modellingmodeling 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 ==

* [[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 HomepageHome Page]

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

[[Category:ProgrammingConcurrent programming languages]]

{{compu-lang-stub}}

[[Category:Programming languages]]

{{compu-lang-stub}}