Rebeca (Informatik)

Rebeca (Reactive Objects Language) ist eine Modellierungssprache für auf dem Actor Model basierende Systeme. Sie wird als praxistaugliches Tool entwickelt, um die Lücke zwischen formalen Methoden und dem Software Engineering zu schließen. Rebeca wird sowohl an der Universität von Teheran als auch an der Universität von Reykjavík weiterentwickelt.

Konzept

In Rebeca wird das Gesamtsystem aus einer Anzahl von nebenläufigen Prozessen modelliert. Diese nebenläufigen Prozesse werden Rebecs genannt. Rebecs entsprechen den Aktoren im Actor Model, da sie einen eigenen Zustand haben, welcher nicht von außen verändert werden kann, und untereinander asynchron über Nachrichten kommunizieren. Ein Rebec kann jedoch keine weiteren Rebec erzeugen.

Rebeca ist syntaktisch an Java angelehnt. Die Beschreibung von Zustandsänderungen erfolgt somit imperativ und nicht deklarativ. Die Definition eines Rebecs besteht aus vier Teilen:

knownrebecs: Definiert bekannte andere Rebecs.
statevars: Variablen des Rebecs, stellen den internen Zustand dar.
Konstruktor: Initialisiert das Rebec.
msgsrv: Mehrere Message Server, die eingehende Nachrichten verarbeiten und den internen Zustand des Rebecs verändern.

Ein Systemmodell hat darüber hinaus eine main-Funktion die die Instanzen von Rebecs definiert und darüber hinaus untereinander bekannt macht.

Model Checking

Für Rebeca steht ein Model Checker namens RMC zur Verfügung. Dieser erlaubt neben der Prüfung auf Deadlocks auch die eigene Definition von zu prüfenden Eigenschaften mittels LTL. Neben dem reinen Model Checker steht auch eine auf Eclipse basierende Entwicklungsumgebung für Rebeca Modelle namens Afra zur Verfügung.

Derivate

Neben der Kerndefinition von Rebeca existieren zwei Erweiterungen der Sprache die insbesondere darauf abzielen zeitkritische Systemmodelle zu überprüfen.

Timed Rebeca

In Timed Rebeca kann neben der reinen Zustandsänderung auch das Verstreichen von Zeit ins Modell aufgenommen werden. Hierfür kann zunächst definiert werden wie lange einzelne Schritte der Nachrichtenverarbeitung dauern. Um Latenzen abbilden zu können, kann definiert werden, dass eine Nachricht erst nach einer definierten Zeitspanne beim Empfänger ankommt. Darüber hinaus kann eine Nachricht mit einer deadline, also einem spätestens Verarbeitungszeitpunkt versehen werden.

Probabilistic Timed Rebeca

Probabilistic Timed Rebeca erweitert das Konzept von Timed Rebeca dadurch, dass Werte für Variablen nicht fest definiert werden müssen, sondern Wahrscheinlichkeiten für Werte angegeben werden können.

Weblinks

Publikationen

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