B Informelle Semantik
Dieser Abschnitt beschreibt informell die Bedeutung der Sequential
Function Charts (SFC's), für die das Tool Snot entwickelt werden
soll. Die Semantik ist nur für gecheckte SFC's definiert (s.
Abschnitt 6); nicht-gecheckte SFC's sind bedeutungslos.
Insbesondere können der Simulator und der Model-Checker
(Abschnitt 7 und 9), die die Semantik
realisieren, von gecheckter Syntax ausgehen.
B.1 Sequential Function Charts
Wir erläutern die Semantik der SFC's anhand des folgenden Beispiels:
Die SFC's bestehen aus Knoten, genannt Steps, zu denen Aktionen
assoziiert sind, sowie aus Transitionen zwischen Steps, die mit
booleschen Guards versehen sind. Es sind immer einer oder mehrere der
Steps aktiv; die mit diesen aktiven Steps assoziierten Aktionen werden in
einem Arbeitszyklus ausgeführt. Die Transition von s1 zu s2 und s3
(mit doppelter horizontaler Linie) ist eine parallele Verzweigung, wird
diese Transition genommen, so wird s1 deaktiviert und s2 sowie s3
aktiviert.
Der oberste speziell markierte Step ist initial. Das "`N"' vor den Aktionen
ist ein Qualifier, er besagt, dass die Aktion in jedem Arbeitszyklus
ausgeführt werden soll, in dem der Step aktiv ist. Es gibt noch weitere
Qualifier, die wir aber erst einmal vernachlässigen.
Der Ablauf eines SFC's (ein Zyklus) ist wie folgt:
-
Inputs lesen von der Umgebung
- Aktionen der aktiven Steps ausführen
- Guards auswerten
- Transitionen nehmen (wenn möglich)
- Outputs schreiben
Dieser Zyklus wird immer wieder abgearbeitet. Die Schritte Inputs
lesen und Outputs schreiben sind für uns erst einmal irrelevant, da
wir nur abgeschlossene Systeme betrachten, d.h. Systeme, deren Variablen nur
durch das System selbst verändert werden.
Die Transitionen sind mit einem Guard ausgestattet sein, einem
booleschen Ausdruck. Eine Transition kann nur genommen werden,
falls sich der Guard zu true evaluiert.
Sind aufgrund einer parallelen Verzweigung mehrere Steps aktiv, so
erfolgt die Ausführung der zugehörigen Aktionen nichtdeterministisch, d.h. sie
sind in beliebiger Reihenfolge möglich (Interleaving-Semantik).
Folglich gibt es unter Umständen eine Vielzahl verschiedener Läufe eines
SFC's, abhängig von diesen Ausführungsreihenfolgen. Der Simulator soll dies
dadurch realisieren, dass er nach Wahl des Benutzers diesen fragt in welcher
Reihenfolge die Aktionen ausgeführt werden sollen, oder aber die Reihenfolge
per Zufallsgenerator festlegt.
Die Transition von s4 und s5 zu s8 schließt die paralelle Verzweigung
wieder. Solche Transitionenen können nur genommen werden, wenn alle
Quell-Steps aktiv sind. Folglich kann diese Transition nur genommen werden
kann, wenn ihr Guard zu true evaluiert wird, und ferner die beiden
Steps s4 und s5 aktiv sein.
B.2 Zustände
Der globale Zustand eines Programmes ist gegeben durch die Variablenbelegungen
und die Menge der aktiven Steps.
last generated May 8, 2001 (©Public License)
