System verification tools based on Monadic Logics

In der Mitte des letzten Jahrhunderts erschienen die ersten Arbeiten über monadische Logiken zweiter Stufe. Das Interesse an diesen Logiken lag zunächst hauptsächlich an Entscheidbarkeitsfragen von arithmetischen Theorien. Die monadischen Logiken zweiter Stufe über Wörter und Bäume gehören zu den ausdrucksstärksten Logiken, die noch entscheidbar sind. Gegenwärtig werden monadische Logiken auch in der Informatik zum Zweck der formalen Systemverifikation verwendet. Entscheidungsverfahren für diese Logiken wurden in verschiedenen Werkzeugen wie z.B. Mona, MOSEL und dem Step System implementiert und teilweise erfolgreich in unterschiedlichen Anwendungsgebieten, vor allem in der Hardware- und Protokoll-verifikation, eingesetzt. <br>Der Erfolg der auf monadischen Logiken basierten Verifikationswerkzeuge wird allerdings durch zwei große Nachteile, die diese Logiken mit sich bringen, erheblich vermindert. Zum einen sind diese Logiken wegen ihres geringen Abstraktionsgrades als Spezifikationssprachen ungeeignet; die Formalisierung von Systemen und Systemeigenschaften in diesen Logiken bedarf eines hohen Maßes an Erfahrung und Detailkenntnissen und ist mit der Programmierung in Assembler vergleichbar. Zum anderen haben die Entscheidungsverfahren für diese Logiken eine sehr hohe Berechnungskomplexität; oft brechen die oben genannten Werkzeuge ihre Berechnung aus Mangel an Speicherressourcen ab.<br>Die vorliegende Arbeit stellt mehrere Verfahren vor, die die erwähnten Nachteile überwinden und machen somit die monadischen Logiken für die Praxis besser nutzbar. Nachfolgend stellen wir die Beiträge in unserer Arbeit dar. Wir entwickeln zunächst eine neue auf monadische Logik über endliche Bäume basierende Spezifikationssprache, die intuitiv und benutzerfreundlich ist und Sprachkonstrukte bereitstellt, die einen höheren Abstraktionsgrad ermöglichen. Außerdem geben wir eine syntaktische Charakterisierung von Klassen von Formeln der neu entwickelten Spezifikationssprache an, die eine akzeptable Berechungskomplexität haben. <br>Desweiteren untersuchen wir das Problem der sogenannten Zustandsraumexplosion: Bei der Verifikation von großen Systemen in monadischen Logiken kann der Zustandsraum nicht-elementar groß werden. Um dieses Problem zu vermeiden, geben wir ein Verfahren an, das für die Generierung von Gegenbeispielen eine effektive und nicht-elementare Verbesserung gegenüber den herkömmlichen Entscheidungsverfahren bietet.<br>Schließlich beschäftigen wir uns auch mit der Frage, wie man, ausgehend von der Kernidee dieser Methode zur Generierung von Gegenbeispielen, monadische Logiken über endlichen Wörtern zum Nachweis von Eigenschaften nicht-terminierender Systeme benutzen kann.<br>Unsere Resultate ergeben, daß man sowohl Sicherheits- als auch Lebendigkeitseigenschaften in monadischen Logiken über endlichen Wörtern formalisieren und dadurch automatisch beweisen kann.<br>Die Praxistauglichkeit unserer theoretischen Resultate stellen wir durch die Implementierung von verschiedenen Verifikationswerkzeugen (Lisa, Monaco und Qubos) unter Beweis. Anwendbarkeit und Skalierbarkeit dieser Werkzeuge werden anhand nicht-trivialer Fallbeispiele evaluiert.

Author dc:creator

• Ayari, Abdelwaheb

Contributors dc:contributor

• Basin, David

• model checking
• bounded model checking
• sat solvers
• decidable logics

Repository record source_url

https://freidok.uni-freiburg.de/data/1234

OAI identifier oai:identifier

oai:freidok.uni-freiburg.de:1234