Rebeca (computer science)

from Wikipedia, the free encyclopedia

Rebeca ( Re active O b j ec ts L a nguage) is a modeling language for systems based on the actor model . It is being developed as a practical tool to close the gap between formal methods and software engineering. Rebeca is being developed further at both the University of Tehran and the University of Reykjavík.

concept

In Rebeca, the overall system is modeled from a number of concurrent processes. These concurrent processes are called rebecs . Rebecs correspond to the actuators in the Actor Model, as they have their own state, which cannot be changed from the outside, and communicate with each other asynchronously via messages. However, a rebec cannot generate any further rebecs.

Rebeca is syntactically based on Java . The description of status changes is therefore imperative and not declarative. The definition of a Rebec consists of four parts:

  • knownrebecs: Defines other known rebecs.
  • statevars: Variables of the Rebec, represent the internal state.
  • Constructor: Initializes the Rebec.
  • msgsrv: Several message servers that process incoming messages and change the internal status of the Rebec.

A system model also has a main function that defines the instances of Rebecs and also makes them known to one another.

Model checking

A model checker called RMC is available for Rebeca . In addition to checking for deadlocks, this also allows you to define your own properties to be checked using LTL . In addition to the pure model checker, an Eclipse- based development environment for Rebeca models called Afra is also available.

Derivatives

In addition to Rebeca’s core definition, there are two extensions of the language that are particularly aimed at checking time-critical system models.

Timed Rebeca

In Timed Rebeca, in addition to the pure state change, the passage of time can also be included in the model. To do this, you can first define how long individual steps in message processing take. In order to be able to map latencies, it can be defined that a message only arrives at the recipient after a defined period of time. In addition, a message can be given a deadline , i.e. a processing time at the latest.

Probabilistic Timed Rebeca

Probabilistic Timed Rebeca extends the concept of Timed Rebeca by the fact that values ​​for variables do not have to be firmly defined, but probabilities for values ​​can be specified.

Web links

Publications

  • Aceto, Luca and Cimi Matteo and Ingolsdottir, Anna, and Reynisson, Arni H. and Sigurdarson, Steinar H. and Sirjani, Marjan: Modeling and Simulation of Asynchronous Real-Time Systems using Timed Rebeca . August 2011, doi : 10.4204 / EPTCS.58.1 , arxiv : 1108.0228 .