Previous Contents Next

6   Übersetzung nach SMV

Team: Tobias Kloss, Kevin Koeser



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 Variablen 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 17, 2001 (©Public License)
Previous Contents Next