• Startseite
• Recherche
• Veröffentlichen
• Hilfe

Eingang zum Volltext

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:bsz:25-opus-12344
URL: http://www.freidok.uni-freiburg.de/volltexte/1234/

Ayari, Abdelwaheb

System verification tools based on Monadic Logics

Werkzeuge zur Systemverifikation basierend auf monadischen Logiken

Kurzfassung in Deutsch

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.


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.


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.

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.

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.
Unsere Resultate ergeben, daß man sowohl Sicherheits- als auch
Lebendigkeitseigenschaften in monadischen Logiken über endlichen
Wörtern formalisieren und dadurch automatisch beweisen kann.


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.

Kurzfassung in Englisch

Fundamental work on monadic second-order logics began about forty
years ago. These logics are amongst the most expressive logics that
are known to be decidable. Their first application domain was
mathematics, where they were for example used to decide theories of
arithmetics. Recently, they have also been applied to formally reason
about a number of problems in computer science: despite their
non-elementary complexity, decision procedures for monadic logics over
finite words and finite trees have been implemented in numerous tools
(eg, Mona, MOSEL, and Step) and have been successfully
applied to problems such as the verification of hardware and software
systems. These logics suffer, however, from two drawbacks that
strongly limit their application, namely the low-level language they
provide to specify systems and properties, and the demanding
computational complexity of their decision procedures.



To make system verification based on monadic logics more viable in
practice, in this thesis we systematically address both these problems
at once. To this end, we first improve the existing approaches (i) by
formalizing a new specification language which is expressive,
intuitive and more user-friendly, and (ii) by providing a handle on
the complexity of the logics' decision procedures. Second, we develop
new efficient algorithms and approaches to cope with the state-space
explosion problem. Third, we investigate how to employ the monadic
logic over finite words to reason about non-terminating systems.
Finally, we implement our methods in three tools (Lisa, Monaco,
and Qubos) and show their applicability and scalability.