Previous Contents Next

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:






Figure 1: SFC


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: 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)
Previous Contents Next