Rebeca Modeling Language

Rebeca Modeling Language

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.

See also

* Software engineering
* Actor model
* Formal methods
* Model checking
* SPIN model checker

External links

* [http://khorshid.ut.ac.ir/~rebeca/ Rebeca]


Wikimedia Foundation. 2010.

Игры ⚽ Поможем решить контрольную работу

Look at other dictionaries:

  • Modeling language — A modeling language is any artificial language that can be used to express information or knowledge or systems in a structure that is defined by a consistent set of rules. The rules are used for interpretation of the meaning of components in the… …   Wikipedia

  • Rebeca (disambiguation) — Rebeca is a a pop eurodance singer, producer, songwriter and actress.Rebeca may also refer to: * Rebeca Modeling Language, an actor based language with a formal foundation, designed in an effort to bridge the gap between formal verification… …   Wikipedia

  • Actor model — In computer science, the Actor model is a mathematical model of concurrent computation that treats actors as the universal primitives of concurrent digital computation: in response to a message that it receives, an actor can make local decisions …   Wikipedia

  • Модель акторов — В компьютерных науках модель акторов представляет собой математическую модель параллельных вычислений, которая трактует понятие «актор» как универсальный примитив параллельного численного расчёта: в ответ на сообщения, которые он получает, актор… …   Википедия

  • Formal methods — In computer science and software engineering, formal methods are particular kind of mathematically based techniques for the specification, development and verification of software and hardware systems.cite web|author=R. W. Butler|title=What is… …   Wikipedia

  • Формальные методы — Пример формальной спецификации с использованием Z нотации В информатике и инженерии программного обеспечения формальными методами называется группа техник, основанных на математическом аппарате для …   Википедия

  • arts, East Asian — Introduction       music and visual and performing arts of China, Korea, and Japan. The literatures of these countries are covered in the articles Chinese literature, Korean literature, and Japanese literature.       Some studies of East Asia… …   Universalium

  • Mexico's Next Top Model, Cycle 1 — Promotional Photograph of Cycle 1 of Mexico s Next Top Model Format Reality television Created by …   Wikipedia

  • El Vacilón de la Mañana — was New York s top Spanish language morning radio show. It is broadcasted from La Mega (97.9 MHz) and it is syndicated live to a number of different markets in the US such as Providence, RI, Miami Orlando, FL, Atlanta, GA, Hartford, CT and Puerto …   Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”