Abstraktionsverfeinerung mittels Gegenbeispielen f\"ur die Verifikation hybrider SFCs

In dieser Bachelor Arbeit wird ein Ansatz zur Verifikation von Anlagensteuerung vorgestellt. Bei der Verifikation wird zusätzlich zum
diskreten Steuerungsprogramms auch das dynamische Verhalten der Anlage berücksichtigt. Wir speichern dieses Verhalten als bedingte
gewöhnliche Differentialgleichungssysteme und kombinieren diese mit Sequential Function Charts (SFCs), um hybride SFCs (HSFCs) zu
erstellen. Diese HSFCs werden in hybride Automaten transformiert. Wir benutzen die SpaceEx Tool Platform, um eine Erreichbarkeitsanalyse
durchzuführen. Eine erfolgreiche Verifikation weist nach, dass das Modell korrekt ist, ansonsten liefert die Analyse ein Gegenbeispiel,
d.h. das Modell ist inkorrekt. Um einer Explosion des Zustandsraums entgegen zu wirken, erweitern wir das Verfahren um einen Verfeinerungsalgorithmus. Wir abstrahieren das
dynamische Verhalten der Anlage und verfeinern das Modell iterativ durch Hinzufügen von bedingten Differentialgleichungssystemen, falls

die Verifikation fehlschlägt. Dazu analysieren wir das Gegenbeispiel, um mit Hilfe geeigneter Heuristiken das dynamische Verhalten, das bei der Verfeinerung berücksichtigt wird, zu bestimmen. Anschließend wird
die Erreichbarkeitsanalyse erneut durchgeführt, bis das Modell entweder korrekt ist, oder das Modell inkorrekt ist, aber keine weitere Verfeinerung mehr möglich ist. Es werden drei verschiedene
Heuristiken präsentiert, die zur Verfeinerung genutzt werden können.