Parallel algorithms for verification of large systems

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.

Grantor dc:publisher

RWTH, Department of Computer Science

Year dc:date

2006

Author dc:creator

• Weber, Michael

Contributors dc:contributor

• Indermark, Klaus

• info:eu-repo/classification/ddc/004
• Informatik
• Verifikation
• paralleler Algorithmus
• endlicher Zustandsraum
• mu-Kalkül
• Model-Checking-Spiele
• Zustandsraumgenerierung
• mu-calculus
• model-checking games
• state space generation
• model checking

Statement dc:rights

• info:eu-repo/semantics/openAccess

Language dc:language

eng

Identifier

https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123475%22

OAI identifier oai:identifier

oai:publications.rwth-aachen.de:61857