2.4 Kommunizierende endliche Automaten
55
Definition 2.8 (Bengtson [44]): Ein zeitgesteuerter Automat ist ein Tupel (S, s 0 , E, I)
mit:
• einer endlichen Menge an Zuständen S,
• einem Anfangszustand s 0 ,
• der Kantenmenge E ⊆ S × B(C) × Σ × 2 C × S. B(C) modelliert die konjunktive
Bedingung, die gelten muss, und Σ modelliert den Eingang, der für die Aktivierung eines Übergangs notwendig ist. 2 C stellt die Menge an Uhrvariablen dar, die
zurückgesetzt werden, wenn die Transition aktiv wird.
• I : S → B(C) ist die Menge der Invarianten für jeden einzelnen Zustand. B(C)
stellt die für einen bestimmten Zustand S zutreffende Invariante dar. Diese Invariante wird durch eine konjunktive Formel beschrieben.
Diese erste Definition wird meist erweitert, um parallel arbeitende zeitgesteuerte
Automaten beschreiben zu können. Zeitgesteuerte Automaten mit einer großen Anzahl von Uhren sind meist schwer zu verstehen. Weitere Details über zeitgesteuerte
Automaten finden sich z.B. in Veröffentlichungen von Dill et al. [133] und Bengtsson
et al. [44].
Die Simulation und Verifikation von zeitbehafteten Automaten ist mit dem populären Werkzeug UPPAAL möglich11. UPPAAL unterstützt Nebenläufigkeit und
Datenvariablen.
Zeitgesteuerte Automaten erweitern klassische Automaten um Zeitinformation.
Sie erfüllen damit aber viele unserer anderen Anforderungen an Spezifikationstechniken nicht. Insbesondere verfügen sie in der hier beschriebenen Standardform weder
über Hierarchie noch über Nebenläufigkeit.
2.4.2 StateCharts: implizite Kommunikation über gemeinsamen
Speicher
Die hier vorgestellte StateCharts-Sprache ist ein bekanntes Beispiel einer automatenbasierten Sprache, die hierarchische Modelle und Nebenläufigkeit unterstützt. Sie
beinhaltet zudem eingeschränkte Möglichkeiten zur Angabe von Zeitinformationen.
StateCharts wurde 1987 von David Harel [204] vorgestellt und später detaillierter
beschrieben [141]. Den Namen hat Harel angeblich so gewählt, weil es „die einzige
unbenutzte Kombination von flow oder state mit diagram oder chart “ war.
Modellierung von Hierarchie
Die StateCharts-Sprache beschreibt erweiterte endliche Automaten, sie ist daher gut
dazu geeignet, zustandsorientiertes Verhalten abzubilden. Die wichtigste Erweite11 Die akademische Version ist unter http://www.uppaal.org und die kommerzielle Version ist unter
http://www.uppaal.com erhältlich.
55
Definition 2.8 (Bengtson [44]): Ein zeitgesteuerter Automat ist ein Tupel (S, s 0 , E, I)
mit:
• einer endlichen Menge an Zuständen S,
• einem Anfangszustand s 0 ,
• der Kantenmenge E ⊆ S × B(C) × Σ × 2 C × S. B(C) modelliert die konjunktive
Bedingung, die gelten muss, und Σ modelliert den Eingang, der für die Aktivierung eines Übergangs notwendig ist. 2 C stellt die Menge an Uhrvariablen dar, die
zurückgesetzt werden, wenn die Transition aktiv wird.
• I : S → B(C) ist die Menge der Invarianten für jeden einzelnen Zustand. B(C)
stellt die für einen bestimmten Zustand S zutreffende Invariante dar. Diese Invariante wird durch eine konjunktive Formel beschrieben.
Diese erste Definition wird meist erweitert, um parallel arbeitende zeitgesteuerte
Automaten beschreiben zu können. Zeitgesteuerte Automaten mit einer großen Anzahl von Uhren sind meist schwer zu verstehen. Weitere Details über zeitgesteuerte
Automaten finden sich z.B. in Veröffentlichungen von Dill et al. [133] und Bengtsson
et al. [44].
Die Simulation und Verifikation von zeitbehafteten Automaten ist mit dem populären Werkzeug UPPAAL möglich11. UPPAAL unterstützt Nebenläufigkeit und
Datenvariablen.
Zeitgesteuerte Automaten erweitern klassische Automaten um Zeitinformation.
Sie erfüllen damit aber viele unserer anderen Anforderungen an Spezifikationstechniken nicht. Insbesondere verfügen sie in der hier beschriebenen Standardform weder
über Hierarchie noch über Nebenläufigkeit.
2.4.2 StateCharts: implizite Kommunikation über gemeinsamen
Speicher
Die hier vorgestellte StateCharts-Sprache ist ein bekanntes Beispiel einer automatenbasierten Sprache, die hierarchische Modelle und Nebenläufigkeit unterstützt. Sie
beinhaltet zudem eingeschränkte Möglichkeiten zur Angabe von Zeitinformationen.
StateCharts wurde 1987 von David Harel [204] vorgestellt und später detaillierter
beschrieben [141]. Den Namen hat Harel angeblich so gewählt, weil es „die einzige
unbenutzte Kombination von flow oder state mit diagram oder chart “ war.
Modellierung von Hierarchie
Die StateCharts-Sprache beschreibt erweiterte endliche Automaten, sie ist daher gut
dazu geeignet, zustandsorientiertes Verhalten abzubilden. Die wichtigste Erweite11 Die akademische Version ist unter http://www.uppaal.org und die kommerzielle Version ist unter
http://www.uppaal.com erhältlich.