Incomplete Property Checking for Asynchronous Reactive Systems

Abstract

Asynchrone Reaktive Systeme kommen in einem breiten Spektrum von Softwaresystemen, so z. B. in Kommunikationsprotokollen und eingebetteten Softwaresystemen, zur Anwendung. Es ist von großer Wichtigkeit zu zeigen, dass diese Systeme korrekt entworfen sind, da ein solcher korrekter Entwurf die Grundlage dafür ist, dass diese Systeme Dienste von hoher Qualität liefern. Formale Ansätze zur Verifikation solcher Systeme, wie z. B. Model Checking, sind aufgrund der extrem großen oder sogar unendlichen Zustandsräume, die diese Systeme besitzen, nur schwer anwendbar. Im Fall von Systemen mit unendlichen Zustandsraum werden viele interessante Verfikationsprobleme unentscheidbar, und traditionelle Model Checking Techniken für endliche Zustandsräume sind dann nicht mehr anwendbar.Wir schlagen ein auf ganzzahliger Programmierung beruhendes Gerüst zur Verifikation vor, welches auf der lokalen Analyse des zyklischen Verhaltens einer jeden Systemkomponente beruht. Dadurch vermeiden wir die Exploration des sehr großen oder sogar unendlichen Zustandsraums des Systems. Um genau zu sein, verwenden wir automatisierte Abstraktionstechniken, um ein zu analysierendes System in eine Menge von Kontrollflusszyklen zu überführen und den Nachrichten-Austauscheffekt dieser Zyklen zu überapproximieren. Für eine zu analysierende Eigenschaft bestimmen wir notwendige Bedingungen an die Kontrollflusszyklen, welche die Verletzung dieser Eigenschaft anzeigen. Diese Bedingungen werden dann in ein ganzzahliges Programmierungsproblem überführt, so dass dessen Lösungsraum das Eigenschaften verletzende Verhalten des Systems repräsentiert. Die Unlösbarkeit des ganzzahligen Programmierungsproblems beweist damit die Erfüllung der Eigenschaft durch das System. Das ganzzahlige Programmierungsproblem kann dann in polynomieller Zeit auf seine Lösbarkeit hin überprüft werden. Wir haben unser Verifikationsgerüst für die Verifikation der konkreten Eigenschaften der Beschränktheit von Kommunikationspuffern (boundedness of buffers) und der Abwesenheit von divergierendem Systemverhalten (absence of livelock) konkretisiert. Diese beiden Eigenschaften sind für asynchrone reaktive Systeme mit einem unendlichen Zustandsraum unentscheidbar.Dem gegenüber ist unser Verifikationsgerüst effizient, da es nicht alle exponentiell vielen linearisierten Ausführungsfolgen der Systemkomponenten betrachten muss. Es erhält die Lokalität der Analyse jeder einzelnen Systemkomponente und reduziert das ursprüngliche Verifikationsproblem zu einem Problem, das in polynomieller Zeit gelöst werden kann. Auf der anderen Seite ist unser Verifikationsgerüst unvollständig: es zeigt entweder die Erfüllung einer Eigenschaft, oder es endet mit einem untentschiedenen Verdikt, das wir mit UNKNOWN bezeichnen. In diesem Fall ist die Eigenschaft für das untersuchte System entweder erfüllt, oder nicht erfüllt. Diese Unschärfe wird durch die Grobheit der von unserem Verifikationsgerüst verwendeten Abstraktion hervorgerufen. Die Unvollständigkeit unseres Verfikationsgerüstes ist in jedem Fall unvermeidbar, da die überprüften Eigenschaften unentscheidbar sind.Da die Präzision unseres auf Abstraktion beruhenden Verifikationsgerüsts ein kritischer Punkt ist, schlagen wir automatische, auf Gegenbeispielen beruhende Abstraktionsverfeinerungsschritte vor. Diese beruhen auf der Entdeckung von Abhängigkeiten zwischen den Kontrollflusszyklen. Die entdeckten Abhängigkeiten können effizient in lineare Ungleichungen übersetzt werden, die dann dazu verwendet werden, die Menge der zur Lösung des ursprünglichen ILP Problems ermittelten linearen Ungleichungen zu erweitern. Die zusätzlichen Ungleichungen schließen möglicherweise nicht zulässiges Verhalten aus, welches zu einer Eigenschaftsverletzung führte, und verfeinern somit die ursprüngliche Abstraktion. Die Methoden zur Entdeckung von Zyklenabhängigkeiten sind ebenfalls unvollständig. Dies bedeutet, dass ein Teil des unzulässigen Verhaltens, das Eigenschaftsverletzungen zur Folge hat, möglicherweise durch die von uns entdeckten Zyklenabhängigkeiten nie entdeckt werden kann.Die resultierenden Verifikationsverfahren werden durch die Entwicklung von geeigneten Code-Abstraktionstechniken für zwei häufig verwendete Modellierungssprachen, nämlich Promela und UML RT, angepasst. Diese Techniken berücksichtigen spezifische Aspekte der beiden Sprachen, so besonders die Definition von Nachrichten, Prozessinstanziierungen, die Zuweisung von Nachrichtenpuffern, etc. Darüber hinaus haben wir eine automatische, unvollständige Methode zum Beweis der Termination von Programmschleifen entwickelt, welche ohne die explizite Konstruktion von Rangfolge-Funktionen auskommt. Schließlich haben wir mehrere Prototypen-Werkzeuge entwickelt, mit deren Hilfe wir viel versprechende experimentelle Resultate für reale Software-Modelle erhalten haben.