9 Model Checker (optional)
Team:
Es soll die Möglichkeit gegeben werden, die Korrektheit des
eingegebenen SFC's zu überprüfen. Dies soll in einfacher Weise dadurch
geschehen, daß überprüft wird, ob auf allen Ausführungen des Programmes die
Assertions nicht verletzt werden.
Im wesentlichen wird eine Graphsuche implementiert: die
abstrakte Syntax wird in einem ersten Schritt in einen (expliziten oder
impliziten) Graphen übersetzt, der danach mittels Tiefensuche nach
Verletzung der Zusicherungen abgesucht wird.
Die Semantik der Sprache ist in Anhang B informell
beschrieben.
Schnittstelle
Im wesentlichen mit der Gui (Abschnitt 2):
Methode start_modcheck mit Parameter eines SFC's in abstrakter
Syntax. Rückgabe: noch zu klären: entweder mittels Ausnahme oder
boolescher Wert. Auf jeden Fall wird der Gui der Zustand zurückgegeben, in
welchem die Verletzung auftritt. Wie die Gui darauf reagiert, ist nicht
Sache des Modelcheckerpaketes (z.B. könnte der Zustand gehighlighted
werden).
last generated May 8, 2001 (©Public License)