h1

h2

h3

h4

h5
h6
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png

Parallel algorithms for verification of large systems = Parallele Algorithmen zur Verifikation von großen Systemen



VerantwortlichkeitsangabeMichael Weber

ImpressumAachen : RWTH, Department of Computer Science 2006

UmfangII, 133 S. : graph. Darst.

ReiheAachener Informatik-Berichte ; 2006,2


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

  1. Fachgruppe Informatik (120000)
  2. Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) (121310)

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:
Download 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

 GO


OpenAccess

QR Code for this record

The record appears in these collections:
Document types > Theses > Ph.D. Theses
Faculty of Mathematics, Computer Science and Natural Sciences (Fac.1) > Department of Computer Science
Publication server / Open Access
Public records
Publications database
120000
121310

 Record created 2013-01-28, last modified 2023-10-11


Fulltext:
Download fulltext PDF
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)