Previous Contents

C   Informelle Semantik

Dieser Abschnitt beschreibt informell die Bedeutung der Sequential Function Charts (SFC's), für die das Tool Snotentwickelt 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.

C.1   Sequential Function Charts

Wir erläutern die Semantik der SFC's anhand des folgenden Beispiels:





1.8mm(44.5,75)(-27,-15) ( 0, 55)( 0,-2.5)0.15(0,-1)6 ( 0,-5.5)(-1.5,0)0.2(1,0)3(2.5,0)(0,0)[l]  true (-12,-8.5)0.15(1,0)24 (-12,-9.5)0.15(1,0)24 (-12,-8.5)0.15(0,-1)4 ( 12,-8.5)0.15(0,-1)4 ( 2,0)0.15(1,0)2 (-2.5,-2.5)0.2(5,5)s1 (-2.2,-2.2)0.2(4.4,4.4)3cm    
N x := false
(-12, 40)( 0,-2.5)0.15(0,-1)25 ( 0,-14.5)(-1.5,0)0.2(1,0)3(2.5,0)(0,0)[l]  x and y ( 2,0)0.15(1,0)2 (-2.5,-2.5)0.2(5,5)s23cm    
N y := x
( 12, 40)( 0,-2.5)0.15(0,-1)4 ( -5,-6.5)0.15(1,0)10 ( -5,-6.5)0.15(0,-1)6 ( -5,-9.5)(-1.5,0)0.2(1,0)3(2.5,0)(0,0)[l]  y ( 5,-6.5)0.15(0,-1)6 ( 5,-9.5)(-1.5,0)0.2(1,0)3(2.5,0)(0,0)[l]  not y ( 2,0)0.15(1,0)2 (-2.5,-2.5)0.2(5,5)s33cm    
N x := not x
( 7, 25)( 0,-2.5)0.15(0,-1)6 ( 0,-5.5)(-1.5,0)0.2(1,0)3(2.5,0)(0,0)[l]  true (-2.5,-2.5)0.2(5,5)s5 ( 17, 25)( 0,-2.5)0.15(0,-1)6 ( 0,-5.5)(-1.5,0)0.2(1,0)3(2.5,0)(0,0)[l]  true (-2.5,-2.5)0.2(5,5)s6 ( 7, 19)( 0,-2.5)0.15(1,0)10 ( 5,-2.5)0.15(0,-1)4 ( 12, 10) (-2.5,-2.5)0.2(5,5)s7 ( 0,-2.5)0.15(0,-1)4

(-12, 10)( 0,-2.5)0.15(0,-1)4 ( 0,-5.5)0.15(1,0)24 ( 0,-6.5)0.15(1,0)24 ( 12,-6.5)0.15(0,-1)6 ( 12,-9.5)(-1.5,0)0.2(1,0)3(2.5,0)(0,0)[l]  true (-2.5,-2.5)0.2(5,5)s4 ( 0, -5)( 0,-2.5)0.15(0,-1)6 ( 0,-5.5)(-1.5,0)0.2(1,0)3(2.5,0)(0,0)[l]  true ( 0,-8.5)0.15(-1,0)20 (-20,-8.5)0.15(0,1)68.5 (-20,60 )0.15(1,0)17.5 (-2.5,-2.5)0.2(5,5)s8

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.

C.2   Zustände

Der globale Zustand eines Programmes ist gegeben durch die Variablenbelegungen und die Menge der aktiven Steps.

C.3   Kommunikationsmodell und Schritte

Die Bedeutung der Konstrukte wie Wertzuweisung, Anfangszustand etc., sollte unstrittig sein. Interpretationsspielraum gibt es für die Kommunikationskonstrukte und das Wesen der Parallelität.

Aufgrund der informellen Diskussion haben wir uns auf folgendes Modell geeinigt:

Das heißt genauer folgendes: Der Zustand des Programmes ändert sich in den Transitionen. Es gibt 4 Arten davon
  1. interne Aktionen (``tau'')
  2. Zuweisung
  3. Input
  4. Output
Die ersten beiden Aktionen werden von einem einzigen Prozeß alleine ausgeführt, d.h., wir haben eine Interleaving-Interpretation.2 Die t-Aktion läßt die Variablenbelegung unverändert, die Verwertzuweisung ändert sie. Daneben wechselt der Betroffene Prozess von einem state und einen Nachfolgezustand entsprechend der Transition.

Daneben gibt es zwei Arten von Kommunikationstransitionen (input und output) die immer komplementär und gleichzeitig ausgeführt werden (synchones Modell) und bei der immer genau zwei Partner beteiligt sind (zwei-Wege Kommunikation).3 Eine Kommunikation zwischen zwei Prozessen kann dann stattfinden, wenn sich beide in einem Zustand befinden, bei dem der eine eine Eingabe-, der andere eine Ausgabeaktion durchführen können (d.h. auch, ihre Guards evaluieren zu true). Falls daß der Fall ist, wechseln beide synchron in ihren Nachfolge-state, wobei der Empfängerprozeß auch noch seine Variablenbelegung durch den empfangenen Wert ändert.

Die Transitionen können mit einem Guard ausgestattet sein, einem booleschen Ausdruck. Eine Transition kann nur genommen werden, falls der Guard sich zu true evaluiert.

©Public License
Previous Contents