Exploring the Limits of Parameterized System Verification

This thesis addresses the problem of verification of parameterized systems. A parameterized system is given by a system description containing some parameters that can be instantiated by different values, such that different parameter instantiations may lead to different finite-state systems. It is known that the general verification problem for parameterized systems is undecidable. A framework for modeling parameterized systems and for deriving a classification of subclasses is presented. This classification is used to investigate the boundary between decidable and a number of undecidable parameterized system classes. Moreover, a verification method for parameterized systems based on abstraction is given. This method can be used to verify liveness properties as well, by deriving fairness constraints from the concrete system. The method is implemented in a tool set called pax. These tools can be used to automatically compute abstractions of parameterized systems and to translate these constructed abstract systems to input languages of existing model-checkers. Applicability of the verification method is demonstrated by presenting a case study of a cache-coherence protocol, and proving both its safety and its liveness properties.

Vorschau

Rechte

Nutzung und Vervielfältigung:

Keine Lizenz. Es gelten die Bestimmungen des deutschen Urheberrechts (UrhG).

Bitte beachten Sie, dass einzelne Bestandteile der Publikation anderweitigen Lizenz- bzw. urheberrechtlichen Bedingungen unterliegen können.

Zitieren

Zitierform:
Zitierform konnte nicht geladen werden.