2006 & 2007
Aachen, Techn. Hochsch., Diss., 2006
Druckausgabe: 2006. - Onlineausgabe: 2007
Genehmigende Fakultät
Fak01
Hauptberichter/Gutachter
Tag der mündlichen Prüfung/Habilitation
2006-01-24
Online
URN: urn:nbn:de:hbz:82-opus-17709
URL: https://publications.rwth-aachen.de/record/61857/files/Weber_Michael.pdf
Einrichtungen
Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei) ; Verifikation (frei) ; paralleler Algorithmus (frei) ; endlicher Zustandsraum (frei) ; mu-Kalkül (frei) ; Model-Checking-Spiele (frei) ; Zustandsraumgenerierung (frei) ; mu-calculus (frei) ; model-checking games (frei) ; state space generation (frei) ; model checking (frei)
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
Das Model-Checking Problem ist die Frage ob ein gegebenes Modell eine bestimmte Eigenschaft erfüllt. Diese ist üblicherweise als temporal-logische Formel gegeben, und das Modell als beschriftetes Transitionssystem. Die Anwendbarkeit dieser Methode zur Verifikation wird eingeschränkt durch die sogenannte Zustandsraumexplosion: Transitionssysteme können im Vergleich zu ihrer Beschreibung exponentiell größer sein. Bekannte sequentielle Algorithmen können das Model-Checking Problem nicht mehr innerhalb der Resourcen eines einzelnen Computers lösen. In dieser Arbeit entwickeln wir parallele und insbesondere verteilte Algorithmen, die die kombinierten Resourcen eines Rechnernetzwerks zur Lösung großer Probleminstanzen heranziehen. Im zweiten Teil untersuchen wir Möglichkeiten zur effizienten Generierung von einfachen Transitionssystemen für unsere Algorithmen aus Modellbeschreibungen in einer Hochsprace. Wir schlagen einen Virtuelle-Maschine-basierten Ansatz vor, in dem eine Zwischensprache benutzt wird, um den Übersetzungsschritt zu vereinfachen. Es hat sich gezeigt, daß dieser Ansatz in der Praxis sehr schnell ist.The model-checking problem is the question whether a given system model satisfies a property. The property is usually given as formula of a temporal logic, and the system model as labelled transition system. However, the well-known state-space explosion effect is responsible for yielding transition systems of exponential size when compared to their description, and common sequential algorithms often are not capable to solve the model-checking problem with resources available on a single computer. In this thesis, we develop parallel and, in particular, distributed algorithms which exploit the combined resources of a network of commodity workstations to solve problem instances which are beyond the capabilities of today’s sequential algorithms. In a second part, we investigate ways to efficiently generate (low-level) transition systems suitable for many verification tools from compact high-level descriptions of the input model. We propose a virtual-machine based approach, which uses an intermediate format to break the translation from high-level to low-level representations of a model into two steps. This well-known compiler technique simplifies the translation and still is very fast in practice.
Fulltext:
PDF
Dokumenttyp
Dissertation / PhD Thesis
Format
online, print
Sprache
English
Externe Identnummern
HBZ: HT014978731
Interne Identnummern
RWTH-CONV-123475
Datensatz-ID: 61857
Beteiligte Länder
Germany