Directed model checking for timed automata [Elektronische Ressource] / Sebastian Kupferschmid

Sebastian KupferschmidDirected Model Checking forTimed AutomataDoktorarbeitInstitut fur¨ InformatikTechnische Fakultat¨Albert-Ludwigs-Universitat¨ FreiburgNovember 2009Tag der Disputation:18. Dezember 2009Dekan:Prof. Dr. Hans Zappe, Albert-Ludwigs-Universitat¨ FreiburgGutachter:Prof. Dr. Bernhard Nebel,sitat¨ FreiburgProf. Dr. Andreas Podelski, Albert-Ludwigs-Universitat¨ FreiburgTo my familyZusammenfassungDie vorliegende Dissertation mit dem Titel “Directed Model Checking forTimed Automata” befasst sich mit der gerichteten Modellprufung¨ fur¨ Real-zeitsysteme. Die Arbeit gliedert sich in zwei einfuhrende¨ Teile und einen in-haltlichen Teil. Der erste Teil fuhrt¨ in das Gebiet der Modellprufung¨ ein. Hierwerden grundlegende Konzepte wie z. B. Kripke Struktur, temporale Logik unddas Problem der Modellprufung¨ vorgestellt. Der Teil endet mit einer kurzenBeschreibung existierender Modellprufungsv¨ erfahren.Der zweite Teil behandelt Realzeitsysteme und gerichtete Modellprufung.¨Er enthalt¨ die Definitionen, die zum Verstandnis¨ dieser Dissertation notig¨ sind.Zuerst wird die Syntax und die Semantik von Realzeitautomaten eingefuhrt.¨ DaZeit in diesem Modell durch reelle Zahlen modelliert wird, ist der Zustands-raum eines Realzeitautomaten ein uberabz¨ ahlbar¨ großes Transitionssystem. De-shalb scheinen Realzeitsysteme ungeeignet fur¨ die Modellprufung¨ zu sein.