„Heuristiken zur Performanzsteigerung der Verifikation induktiver Invarianten“

In den letzten Jahren hat der Grad der Durchdringung von technischen Systemen durch eingebettete Software stetig zugenommen. Heutzutage gibt es nur noch sehr wenig Geräte, Automaten, Fahrzeuge etc., die ohne den Einsatz von Software auskommen. Ist eine Fehlfunktion der eingebetteten Software in Geräten der Unterhaltungselektronik ärgerlich, so ist in den Bereichen, in denen die fehlerfreie Funktion hohen Einfluß auf die Sicherheit des Systems hat (z.B. Fahrzeugelektronik), eine Fehlfunktion nicht tolerierbar.

Am Fachgebiet Systemanalyse und Modellierung wurde ein Verifikationsalgorithmus entworfen, der die Verifikation von strukturverändernde Systemen erlaubt. Solche Systeme treten bei der Modellierung von komplexen Systemen durch die UML aber auch im Bereich der selbst-adaptiven Systeme auf. Der Algorithmus nutzt spezielle Eigenschaften von Regeln – durch diese werden Strukturveränderungen beschrieben – sowie eine bestimmten Klasse verifizierbarer Eigenschaften aus. Es sind lediglich solche sicherheitskritischen Eigenschaften verifizierbar, die sich in Form induktiver Invarianten formulieren lassen. Das Verifikationsverfahren wird als Invariant Checking bezeichnet. Als wichtiges Charakteristikum, das den entwickelten Algorithmus von den klassichen Methoden der formalen Verifikation (häufig Model Checking) unterscheidet, ist die Möglichkeit der Verifikation von Systemen mit einem unendlich großen Zustandsraum. Diese Möglichkeit ist typischerweise bei anderen Verifikationsmethoden nicht gegeben.

Neben der rein diskreten Variante des Algorithmus, die zur Verifikation von Strukturveränderungen eingesetzt wirde, gibt es auch eine Erweiterung des Verfahrens, die zusätzlich die Verifikation von Echtzeiteigenschaften ermöglicht.

Aus Analysen der Worst Case Szenarios für die Laufzeit des Algorithmus wurde deutlich, dass seine Komplexität exponentiell zu der Größe der untersuchten Graphen und quadratisch in der Anzahl der untersuchten Regeln ist. Eine Reduktion der theoretischen Komplexität des Algorithmus scheint aufgrund der Komplexität der Berechnung von Teilgraphisomorphismen nicht möglich. Allerdings ist es durch die Hinzunahme von geeigneten Heuristiken möglich, die zu erwartende Laufzeit der Verifikation für praktisch relevante Situationen erheblich zu verringern. Ausgehend von einigen bereits vorliegenden Heuristiken und in der Literatur dokumentierten Ergebnissen, sollen in dieser Masterarbeit bekannte und eventuell eigene Heuristiken implementiert und bezüglich ihrer Eignung evaluiert werden.

Vorkenntnisse: Java-Programmierung, formale Verifikation, Graphentheorie sind vorteilhaft jedoch nicht zwingend erforderlich.

Ansprechpartner: Basil Becker