Previous Contents Next

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