Rebeca (Informatik)

Überblick und Bedeutung

Rebeca (Reactive Objects Language) ist eine Modellierungssprache für Systeme, die auf dem Actor Model beruhen. Sie soll als praxistaugliches Werkzeug die Lücke zwischen formalen Methoden und Software Engineering schließen. Entwickelt wird sie an der Universität von Teheran und der Universität von Reykjavík.

Ein Rebeca-Modell beschreibt ein Gesamtsystem als mehrere nebenläufige, also gleichzeitig arbeitende Prozesse. Dadurch lassen sich insbesondere asynchrone und zeitkritische Systeme formal darstellen und überprüfen.

Aufbau eines Modells

Die nebenläufigen Prozesse heißen Rebecs und entsprechen den Aktoren des Actor Models. Jeder Rebec besitzt einen eigenen internen Zustand, der nicht von außen verändert werden kann. Rebecs kommunizieren asynchron miteinander, indem sie Nachrichten versenden. Anders als Aktoren in manchen anderen Modellen kann ein Rebec keine weiteren Rebecs erzeugen.

Die Syntax von Rebeca ist an Java angelehnt. Zustandsänderungen werden imperativ beschrieben, also durch auszuführende Anweisungen und nicht durch eine rein deklarative Festlegung des gewünschten Ergebnisses.

Die Definition eines Rebecs besteht aus vier Teilen:

• knownrebecs: legt fest, welche anderen Rebecs dem Rebec bekannt sind.
• statevars: enthält die Variablen, die den internen Zustand des Rebecs darstellen.
• Konstruktor: initialisiert den Rebec.
• msgsrv: bezeichnet mehrere Message Server, die eingehende Nachrichten verarbeiten und dabei den internen Zustand verändern.

Zusätzlich besitzt das Systemmodell eine main-Funktion. Sie erzeugt die Rebec-Instanzen und legt fest, welche Rebecs einander kennen.

Formale Überprüfung

Für Rebeca gibt es den Model Checker RMC. Model Checking ist ein Verfahren, mit dem ein Systemmodell systematisch auf bestimmte Eigenschaften untersucht wird. RMC kann insbesondere Deadlocks erkennen, also Situationen, in denen das System nicht mehr weiterarbeiten kann.

Weitere zu prüfende Eigenschaften können mit LTL (Linear Temporal Logic) formuliert werden. LTL ist eine temporale Logik, mit der Aussagen über den zeitlichen Ablauf eines Systems beschrieben werden. Für die Entwicklung von Rebeca-Modellen steht außerdem die auf Eclipse basierende Entwicklungsumgebung Afra zur Verfügung.

Zeitbezogene Erweiterung

Timed Rebeca erweitert die Kernsprache um die Modellierung von Zeit. Damit lässt sich nicht nur beschreiben, wie sich Zustände ändern, sondern auch, wie viel Zeit dabei vergeht.

Für einzelne Schritte der Nachrichtenverarbeitung kann eine Dauer angegeben werden. Latenzen lassen sich darstellen, indem festgelegt wird, dass eine Nachricht den Empfänger erst nach einer bestimmten Zeitspanne erreicht. Außerdem kann eine Nachricht eine deadline erhalten, also einen spätesten Zeitpunkt, zu dem sie verarbeitet werden darf.

Wahrscheinlichkeiten im Zeitmodell

Probabilistic Timed Rebeca baut auf Timed Rebeca auf. Zusätzlich zu zeitlichen Angaben können Werte von Variablen probabilistisch modelliert werden: Ein Wert muss nicht eindeutig festgelegt sein; stattdessen können für mögliche Werte Wahrscheinlichkeiten angegeben werden. So lassen sich zeitkritische Systeme untersuchen, deren Verhalten auch von unsicheren oder zufälligen Ergebnissen abhängt.