Explicit state space verification [Elektronische Ressource] / von Karsten Schmidt

Karsten Schmidt

Sujets

• Mathematics
• Informatik

Informations

• Publié par: humboldt-universitat_zu_berlin
• Publié le: 01 janvier 2002
• Nombre de lectures: 17
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Explicit State Space Verification
H A B I L I T A T I O N S S C H R I F T
zur Erlangung der Lehrbef¨ahigung
im Fach Informatik
vorgelegt dem Rat der
Mathematisch-Naturwissenschaftlichen Fakult¨at II
der Humboldt-Universit¨at zu Berlin
von
Herr Dr. rer. nat. Karsten Schmidt
geboren am 3.3.1967 in Berlin
Pr¨asident der Humboldt-Universit¨at zu Berlin:
Prof. Dr. Jurg¨ en Mlynek
Dekan der Mathematisch-Naturwissenschaftlichen Fakult¨at II:
Prof. Dr. Elmar Kulke
Gutachter:
1. Prof. Dr. Peter Starke
2. Prof. Dr. Antti Valmari
3. Prof. Dr. Javier Esparza
eingereicht am: 4. Februar 2002
Tag des Fachgespr¨achs: 15. November 2002Abstract
Verification is the task of determining whether a (model of a) system holds a
given behavioral property. State space verification comprises a class of com-
puter aided verification techniques where the property is verified through
exhaustive exploration of the reachable states of the system. Brute force
implementations of state space verification are intractable, due to the well
known state explosion problem. Explicit state space verification techniques
explore the state space one state at a time, and rely usually on data struc-
tures where the size of the data structure increases monotonously with an
increasing number of explored states. They alleviate state explosion by con-
structing a reduced state space that, by a mathematically founded construc-
tion,behavesliketheoriginalsystemwithrespecttothespecifiedproperties.
Thereby, decrease of the number of states in the reduced system is the core
issueofareductiontechniquethusreducingtheamountofmemoryrequired.
An explicit state space verification technique comprises of
• a theory that establishes whether, and how, certain properties can be
preserved through a construction of a reduced state space;
• a set of procedures to execute the actual construction efficiently.In this thesis, we contribute to several existing explicit state space verifi-
cation techniques in either of these two respects.
We extend the class of stubborn set methods (an instance of partial or-
der reduction) by constructions that preserve previously unsupported classes
of properties. Many existing constructions rely on the existence of ”invis-
ible” actions, i.e. actions whose effect does not immediately influence the
verified property. We propose efficient constructions that can be applied
without having such invisible actions, and prove that they preserve reacha-
bility properties as well as certain classes of more complex behavioral system
properties. This way, so called ”global” properties can now be approached
with better stubborn set methods.
We pick up a graph automorphism based approach to symmetry reduc-
tion and propose a set of construction algorithms that make this approach
feasible. In difference to established symmetry techniques that rely on spe-
cial ”symmetry creating” data types, a broader range of symmetries can be
handled with our approach thus obtaining smaller reduced state spaces.
Coverability graph construction leads to a finite representation of an in-
finite state space of a Petri net by condensing diverging sequences of states
to their limit. We prove rules to determine temporal logic properties of the
original system from its coverability graph, far beyond the few properties
known to be preserved so far.
We employ the Petri net concept of linear algebraic invariants for com-
pressing states as well as for leaving states out of explicit storage. Compres-
sionusesplaceinvariantsforreplacingstatesbysmallerfingerprintsthatstill
uniquely identify a state (unlike many hash compression techniques). For re-
ducing the number of explicitly stored states, we rely on the capability of
Petri net transition invariants to characterize cycles in the state space. For
terminationofanexhaustiveexplorationofafinitestatespace,itissufficient
tocoverallcycleswithexplicitlystoredstates. Bothtechniquesareeasycon-
sequences of well known facts about invariants. As a novel contribution, we
observe that both techniques can be applied without computing an explicit
representationof(ageneratingsetfor)therespectiveinvariants. Thisspeeds
up the constructions considerably and saves a significant amount of memory.
For all presented techniques, we illustrate their capabilities to reduce the
complexity of state space reduction using a few academic benchmark exam-
ples. We addresscompatibilityissues, i.e. thepossibilitytoapplytechniques
incombination,orinconnectionwithdifferentstrategiesforexploringthere-
2ducedstatespace. Weproposeaschemetodistributestatespaceexploration
on a cluster of workstations and discuss consequences for using this scheme
for state space reduction. We collect observations concerning the impact of
the choice of system description formalisms, and property specification lan-
guages, on the availability of explicit state space verification techniques.
Keywords:
Computer Aided Verification, State space analysis, Reduction techniques,
Model Checking
3Zusammenfassung
Gegenstand der Arbeit ist die Verifikation von verteilten diskreten Syste-
meninbezugaufSpezifikationenihresVerhaltens.DiskreteSystemebestehen
aus einer abz¨ahlbaren Zustandsmenge und einer Zustandsub¨ ergangsrelation.
Bei verteilten Systemen ist eine signifikante Zahl von Zustandsubergangen¨ ¨
nur durch eine kleine Zahl von Komponenten eines strukturierten Zustands-
raumes bedingt und andert auch nur wenige Komponenten. Bei praktisch¨
relevanten Systemen ist die Zustandszahl unbeherrschbar groß. Dieses Pha-¨
nomen wird Zustandsraumexplosion genannt. Verteiltheit gilt als eine der
wesentlichenUrsachenfurZustandsraumexplosion,weilnebenlaufigmogliche¨ ¨ ¨
lokale Zustandsub¨ erg¨ange abhang¨ ig von ihren exponentiell vielen Ausfuh-¨
rungsreihenfolgen exponentiell viele verschiedene Zwischenzustande erzeu-¨
gen konnen.¨ Fur¨ Verifikationsaufgaben sind Systeme daher implizit gegeben
durch eine Beschreibung von Anfangszustanden und (lokale) Regeln zur Ge-¨
nerierungvonFolgezustanden.¨ SolcheSystembeschreibungenfolgenverschie-
denenParadigmen,z.B.demvariablenorientiertenParadigma(Zustandesind¨
Werte von Variablen, die durch Zustandsub¨ erg¨ange gelesen und geschrieben
werden) oder dem ressourcenorientierten Paradigma (Zustande¨ sind Vertei-
lungen von Ressourcen im System, die durch Zustandsubergange konsumiert¨ ¨
oder produziert werden). Die Verfugba¨ rkeit von Verifikationstechniken oder
spezifischen Implementationen hangt vom zugrundeliegenden Paradigma ab.¨
Als Sprache zur Formulierung von Spezifikationen des Verhaltens ver-
wenden wir etablierte temporale Logiken und fur die Praxis bedeutsame¨
Fragmente solcher Logiken. Temporale Logik beschreibt Eigenschaften von
Abfolgen von Zustanden, basierend auf elementaren, einzelne Zustande be-¨ ¨
treffenden Eigenschaften. Auf einer expliziten Systemdarstellung lassen sich
temporallogische Eigenschaften effizient, d.h. mit einer linear von der Zu-
standszahl abhangigen Laufzeit, verifizieren. Eine solche Verifikation basiert¨
auf einfachen Suchalgorithmen in dem durch das System definierten Zu-
standsgraph. Ein solcher Verifikationsansatz ist aber wegen der genannten
Zustandsraumexplosion nicht durchfuhrba¨ r.Im wesentlichen werden drei Losungsansatze in Richtung durchfuhrbarer¨ ¨ ¨
Verifikationsalgorithmen verfolgt. Die strukturelle Verifikation versucht, Ei-
genschaftendirektausspezifischenMusterninderimplizitenSystembeschrei-
bung abzuleiten. Der derzeitige Stand der Technik gestattet solche Ableitun-
gen nur fur wenige und einfach strukturierte Verhaltensspezifikationen und¨
erfordert auch dann in einigen Fallen recht aufwendige Berechnungen. Bei¨
der symbolischen Zustandsraumanalyse wird der Zustandsraum ersch¨opfend
durchmustert, allerdings unter Benutzung von Datenstrukturen, deren ele-
mentare Objekte ganze Mengen von Zustanden¨ beschreiben, und deren ele-
mentare Operationen die Folgezustandefurganze solche Mengen aus derim-¨ ¨
plizitenSystembeschreibungerrechnen.BeiderexplizitenZustandsraumveri-
fikation,demThemadervorliegendenHabilitationsschrift,wirdeineexplizite
Reprasen¨ tation eines Zustandsraumes generiert, der wesentlich kleiner ist als
der Zustandsraum des untersuchten Systems, in bezug auf die untersuchte
EigenschaftaberperKonstruktionaquivalentzumoriginalenSystemist.Zur¨
Konstruktion werden Informationen aus der impliziten Systembeschreibung
herangezogen.
EineTechnologiezurexplizitenZustandsraumverifikationbestehtalsoaus
• Einer mathematisch fundierten Theorie, die einer bestimmten Kon-
struktionsmethodebescheinigt,welcheEigenschaftendurchsiebewahrt
werden;
• effizientenAlgorithmenzurImplementationeinesolchenKonstruktion;
DieArbeitenthalt¨ ,fur¨ mehrerebekannteVerfahren,Beitr¨agezujeweilsmin-
destens einem der beiden Bestandteile einer expliziten Zustandsraumverifi-
kationstechnik.
Die Methode der sturen Mengen verkleinert den explizit zu konstruie-
renden Zustandsraum dadurch, daß von den in einem Zustand mog¨ lichen
Zustandsubergangen nur einige tatsachlich untersucht werden, so daß weit¨ ¨ ¨
weniger Zwischenz