8 Übersetzung nach SMV
Smv [McM99a, McM99b] ist ein weit verbreiteter
symbolischer Model-Checker. Model-Checker werden benutzt, um festzustellen,
ob endliche Systeme bestimmte Eigenschaften besitzen. Man könnte z.B. die
Airbag-Steuerung eines Autos prüfen wollen; ob es beispielsweise möglich ist,
dass der Beifahrerairbag trotz vorheriger Deaktivierung unter bestimmten
Umständen auslöst.
Diese überprüften Eigenschaften werden üblicherweise in einer temporalen
Logik beschrieben, in dieser ist es möglich Eigenschaften der Art
"`immer/zu jeder Zeit gilt a b "' oder auch "`irgendwann gilt a
b c"' zu spezifizieren.
Smv besitzt eine eigene Eingabesprache, in der auf unterschiedliche Art und
Weise Systeme spezifiziert werden können. Hier ein Beispiel, wie man eine
sogenannte State machine modellieren kann:
MODULE main
VAR
request : boolean;
state : {ready,busy};
ASSIGN
init(state) := ready;
next(state) := case
state = ready & request : busy;
1 : {ready,busy};
esac;
Es werden zunächst zwei Variablen deklariert, eine boolesche request
sowie eine enumerative state. Letztere kann die Werte ready
und busy annehmen. Im ASSIGN-Part wird das Verhalten des
Systems spezifiziert. Initial wird die Variable state mit
ready belegt. Im next(state)-Teil wird beschrieben, wie
sich der Wert von state abhängig vom aktuellen Zustand verändert.
Wie man sieht ist nichts über request ausgesagt; folglich kann diese
Variable in jedem Schritt einen beliebigen Wert annehmen.
Die Aufgabe wird nun darin bestehen, ein SFC, welches ausschließlich boolesche
Varibalen besitzt, in diese Eingabesprache zu übersetzen. Diese Übersetzung
soll natürlich die Semantik des SFC's erhalten. Somit sollen alle
Ausführungssequenzen und erreichbaren Zustände des SFC's auch in der
Übersetzung vorhanden bzw. erreichbar sein. Danach können dann Eigenschaften
des erhaltenen SMV-Systems geprüft werden. Da die Übersetzung die Semantik
erhält, gelten diese Eigenschaften dann auch für das ursprüngliche SFC.
last generated May 2, 2001 (©Public License)