Direkt zum Inhalt | Direkt zur Navigation

Eingang zum Volltext

Lizenz

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


Kupferschmid, Sebastian

Directed model checking for timed automata

Gerichtete Modellprüfung für Realzeitsysteme

Dokument1.pdf (1.200 KB) (md5sum: 1bd289ef64412a88c7444c5b6f28ce81)

Kurzfassung in Englisch

The thesis at hand entitled "Directed Model Checking for Timed Automata" is structured in three parts. The first part is an introduction to the area of model checking. It introduces fundamental concepts like Kripke structures, temporal logic, and the model checking problem. This part concludes with an description of prevailing model checking techniques.

The second part deals with real-time systems and directed model checking. It contains the necessary definitions and notations for this thesis. First, syntax and semantics of real-time systems are introduced. As time is modeled with the non-negative reals, the state space of timed automata is an uncountable transition system. Therefore, it seems like model checking is not an appropriate means for the analysis of timed automata. However this is not the case, as there is a finite and exact abstraction of the semantics. Afterwards, directed model checking is introduced. This includes the presentation of a basic directed model checking algorithm, as well as existent approaches for directed model checking.

The third part is the main part of the thesis. Here, different heuristics and search enhancements for directed model checking are introduced. In chapter 5, the most successful relaxation from AI planning is adapted and extended to directed model checking of timed automata. With the resulting heuristics it is possible to detect reachable error states in systems that could not be analyzed with previous heuristics. In the following chapter, predicate abstraction is used for the construction of pattern database heuristics. The combination of known techniques from the areas of model checking and artificial intelligence yields a family of heuristics, competitive with the state of the art. Chapter 7 presents another pattern database heuristics, based on a Russian doll principle. The approach homes on preserving those parts of the system that are of immediate relevance to the specification. The resulting heuristic is able to find shortest possible error traces in the largest case studies of our benchmark set. The technique presented in chapter 8 is a general approach to accelerate heuristic search. It can be combined with many heuristics and often scales much better than greedy search. Simultaneously, this approach often yields much shorter error traces than greedy search. The last chapter introduces counterexample-guided abstraction refinement for timed automata. Afterwards, an empirical evaluation demonstrates that directed model checking often outperforms abstraction refinement when dealing with erroneous systems.

A discussion of the the essential results concludes the third part of the thesis. It also gives an overview on future work in this area.


Kurzfassung in Deutsch

Die vorliegende Dissertation mit dem Titel "Directed Model Checking for Timed Automata" befasst sich mit der gerichteten Modellprüfung für Realzeitsysteme. Die Arbeit gliedert sich in zwei einführende Teile und einen inhaltlichen Teil. Der erste Teil führt in das Gebiet der Modellprüfung ein. Hier werden grundlegende Konzepte wie z.B. Kripke Struktur, temporale Logik und das Problem der Modellprüfung vorgestellt. Der Teil endet mit einer kurzen Beschreibung existierender Modellprüfungsverfahren.

Der zweite Teil behandelt Realzeitsysteme und gerichtete Modellprüfung. Er enthält die Definitionen, die zum Verständnis dieser Dissertation nötig sind. Zuerst wird die Syntax und die Semantik von Realzeitautomaten eingeführt. Da Zeit in diesem Modell durch reelle Zahlen modelliert wird, ist der Zustandsraum eines Realzeitautomaten ein überabzählbar großes Transitionssystem. Deshalb scheinen Realzeitsysteme ungeeignet für die Modellprüfung zu sein. Das ist allerdings nicht der Fall, da sich diese Zustandsräume endlich partitionieren lassen. Im Anschluss wird die gerichtete Modellprüfung für Realzeitsysteme eingeführt. Neben der Vorstellung eines allgemeinen Algorithmus für die gerichtete Modellprüfung werden hier auch existierende Ansätze für die gerichtete Modellprüfung diskutiert.

Der dritte Teil bildet den Hauptteil der Arbeit. Es werden verschiedene Heuristiken und Verbesserungen für die gerichtete Modellprüfung eingeführt. In Kapitel 5 wird die erfolgreichste Relaxierung aus dem Gebiet der Handlungsplanung auf die gerichtete Modellprüfung für Realzeitautomaten adaptiert und erweitert. Mit den resultierenden Heuristiken ist es möglich, erreichbare Fehlerzustände in Systemen zu finden, die mit zuvor vorgeschlagenen Heuristiken nicht entdeckt werden können. Im darauf folgenden Kapitel wird Prädikatenabstraktion verwendet, um sogenannte Musterdatenbanken zu erzeugen. Durch die Kombination von bekannten Techniken aus den Bereichen der Modellprüfung und der künstlichen Intelligenz erhält man eine Familie von Heuristiken, die mit dem aktuellen Stand der Technik mithalten können. In Kapitel 7 wird eine weitere Musterdatenbank-Heuristik, die auf dem Prinzip der russischen Puppen basiert präsentiert. Der Ansatz zielt darauf ab, diejenigen Teile des Systems so gut wie möglich zu erhalten, die unmittelbar relevant für die zu überprüfende Eigenschaft sind. Mit der resultierenden Heuristik lassen sich beweisbar kürzeste Fehlerpfade in den größten unserer Fallbeispiele finden. Mit der Technik, die in Kapitel 8 präsentiert wird, lässt sich heuristische Suche im Allgemeinen deutlich beschleunigen. Dieser Ansatz kann mit vielen Heuristiken kombiniert werden und skaliert oft deutlich besser als gierige Suche. Gleichzeitig liefert das Verfahren erheblich kürzere Fehlerpfade als gierige Suche. Im letzten Kapitel wird zuerst eine auf Gegenbeispielen basierende Abstraktionsverfeinerung für Realzeitsysteme präsentiert. Danach wird anhand einiger Beispiele demonstriert, dass gerichtete Modellprüfung bei fehlerhaften Systemen oft deutlich performanter als Abstraktionsverfeinerung ist.

Die Dissertation schließt mit einer Diskussion der wesentlichen Ergebnisse des dritten Teils und einem Ausblick auf zukünftige Forschungsaufgaben in diesem Gebiet.


SWD-Schlagwörter: Model Checking
Freie Schlagwörter (deutsch): Heuristische Suche , Fehlererkennung , Realzeitsysteme
Freie Schlagwörter (englisch): Heuristic Search , Error Detection , Timed Automata
CCS Klassifikation I.2.8
Institut: Institut für Informatik
Fakultät: Technische Fakultät (bisher: Fak. f. Angew. Wiss.)
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Erstgutachter: Nebel, Bernhard (Prof. Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 18.12.2009
Erstellungsjahr: 2009
Publikationsdatum: 03.05.2010
Indexliste