B Semantics
The section informally describes the semantics of Sequential Function
Charts (SFC's), as realized in the tool Slime. The semantics is defined
for successfully checked SFC's (cf. Section 4);
unchecked SFC's don't have a meaning. Especially, the simultor and the
model-checker (Section 5 and 9), which
realize the semantics, can assume checked syntax
B.1 Sequential Function Charts
We explain the semantics with the help of the example from
Figure 1.
The SFC's consist of nodes, called steps, to which actions are
associated, and transitionen between steps, decorated with boolean
guards. Always, one ore more of the steps are active and the actions
associate with this active steps are executed within one cylcle. The
transition from s1 to both s2 and s3 (with double horizontal line) is
a parallel branching: if this transition is taken,
s1 is deactivated and both s2 and s3 get activated.
The topmost step (marked specifically) is initial. The ''N'' on the
left-hand side of the actions is a qualifier, stating that the action
is to be executed in each cycle in which the step is active. There are other
qualifiers, too, but we neglect them for the teme being,
Qualifier, die wir aber erst einmal vernachlässigen.
The behavior of an SFC during one cycle is as follows.
-
reading inputs from the environment
- executing the actions from the active steps
- evaluate the guards
- take transition(s) (if possible)
- write outputs
The cycle is executed repeatedly. The parts for reading inputs and
writing outputs are irrelevant for us, as we consider closed systems
ony, i.e., systems whose variables are changed only by the system itself, but
not by the outside.
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 States
The global state of a program is given by the assignment to all variables and
the set of all active steps.
last generated April 15, 2002 (©Public License)
