Nachbearbeitung (U4) - mlachenmayr/FuFaBe GitHub Wiki

Failure-Controller

Der Failure-Controller ist zwar eine alternative Lösung, wenn beispielsweise eine Formel durch CTL nicht ausdrückbar ist. In einem solchen Falle wäre der Einsatz eines derartigen Controllers ein guter Workaround. Allerdings sollte immer versucht werden, etwas direkt durch LTL oder CLT-Formeln auszudrücken.

Zudem stellt er einen Eingriff in die Automatisierung der Verifikation dar, da explizit gesagt wird, welche Störungen in welchem Run des Modellcheckers auftreten dürfen. Dies birgt außerdem zusätzliches Wissen über das Modell, dass bei einem Einsatz eines FailureControllers zumindest dokumentiert werden muss.

Vorschlag: Der Failure-Controller kann (vorerst) im Modell bleiben; es werden alle Flags auf true gesetzt, sodass diese auch alle in jedem Run auftreten können. Die Formeln werden - wenn nötig - noch angepasst. Stellt sich dann heraus, dass alles auch ohne Failure Controller ausdrückbar ist, kann er entfernt werden.

Dualismus von Fehlern implementieren

Bisher wurde zu jeder Störung bzw. jeder Komponenten nur ein Programmgraph modelliert. Dieser trägt lediglich die Zustände NO und YES. Allerdings wird dadurch nicht ausgedrückt, welche Art von Störung an der Komponente auftrat. Am Beispiel des Kommunikationsmediums, dient der Programmgraph F06_CommunicationMedium sowohl für die Störung, dass eine Nachricht "verschluckt" wurde, als auch dafür, dass zusätzliche Nachrichten "generiert" werden (beispielsweise durch einen Hacker oder ein Mobiltelefon). Daher sollten immer beide Seiten eines Fehler betrachtet werden. Hierzu gibt es eine Art Satz-Template:

• er macht es, obwohl er es nicht soll
• er macht nichts, obwohl er es soll