Modellbasierte Verifikation relevanter Eigenschaften komplexer Softwaresysteme

 

Die sehr hohe Komplexität heutiger Softwaresysteme, insbesondere zusammengesetzter Systems-of-Systems, führt dazu, dass ihre vollständige formale Verifikation kaum zu bewältigen ist. Für sicherheitskritische Systeme ist es allerdings notwendig, zumindest die für die betrachtete Anwendung relevanten Eigenschaften nachweisen zu können. Im Rahmen dieses Projektes wird deshalb untersucht, inwieweit sich auf Model Checking basierende Strategien auf als Erweiterte Endliche Automaten (EFSM) erfasste Entwurfsmodelle anwenden lassen.

Da Erweiterte Automaten die volle Ausdruckskraft der Berechenbarkeit besitzen, lässt sich im Allgemeinen die Erfüllung beliebiger Eigenschaften algorithmisch nicht entscheiden. Daher ist man in solchen Fällen auf den Einsatz heuristischer Verfahren angewiesen, deren Gestaltung und Einsetzbarkeit den Gegenstand des Vorhabens bilden.

Die betrachtete EFSM und die nachzuweisende temporallogische Eigenschaft können zunächst anhand einer weiteren EFSM gemeinsam kodiert werden. Es lässt sich dann feststellen, dass die Gültigkeit der temporallogischen Formel von der Existenz und der Ausführbarkeit formelspezifischer Pfade in dieser letzteren EFSM entscheidend abhängt. Für besondere temporallogische Formeln, die ausschlie├člich Allquantoren oder ausschlie├člich Existenzquantoren enthalten, führt insbesondere die Ermittlung spezieller ausführbarer Pfade zu Gegenbeispielen für Universalformeln bzw. zu Belegen für Existenzformeln.

Es wurde eine Implementierung eines Verfahrens vorgenommen, welches die Ermittlung von Pfadmengen in der untersuchten EFSM erlaubt, die als Belege für die Gültigkeit der zu verifizierenden Existenzformel bzw. für die Ungültigkeit der zu verifizierenden Universalformel in Frage kommen. Zur Untersuchung der tatsächlichen Ausführbarkeit dieser Pfade wurde im Rahmen einer studentischen Arbeit ein evolutionärer Algorithmus implementiert.

Zwecks Evaluierung des oben genannten Ansatzes wurden Systeme autonomer, kooperativer Roboter beispielhaft betrachtet und deren Modellierung durch EFSM untersucht. Solche Systeme lassen sich - wie die Lehrstuhlvorhaben R3-COP und R5-COP wiederholt bestätigen konnten - durch gefärbte Petri-Netze geeignet erfassen und analysieren. Bekanntlich erfordert eine Verifikation mittels Model Checking die Festlegung von Anfangsbedingungen anhand der zugehörigen Startmarkierung im Netz. In Roboteranwendungen ist allerdings davon auszugehen, dass diese Anfangsbedingungen (z.B. Missionsziele, Startpositionierung, Energiestand) über die Lebensdauer des Robotersystems stark variieren. Um dennoch praxisrelevante Eigenschaften, die sich typischerweise als Universalformel (z.B. Terminierung, Kollisionsfreiheit) darstellen lassen, weitgehend unabhängig von den Anfangsbedingungen zu überprüfen, bietet es sich an, die Einsetzbarkeit des beschriebenen Verifikationsverfahrens näher zu untersuchen.