Parallel algorithms for verification of large systems [Elektronische Ressource] / Michael Weber. [RWTH Aachen, Department of Computer Science]

Michael Weber

Sujets

• Informatik

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2006
• Nombre de lectures: 7
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Aachen
Department of Computer Science
Technical Report
Parallel Algorithms for
Verification of Large Systems
Michael Weber
ISSN 0935–3232 · Aachener Informatik Berichte · AIB-2006-02
RWTH Aachen · Department of Computer Science · December 2006Parallel Algorithms for
Verification of Large Systems
Von der Fakultat¨ fur¨ Mathematik, Informatik und
Naturwissenschaftender Rheinisch-Westfalischen¨ Technischen
Hochschule Aachen zur Erlangung des akademischen Grades
eines Doktors der Naturwissenschaften genehmigte Dissertation
vorgelegt von
Diplom-Informatiker
Michael Weber
aus
¨Duren
Berichter: Prof. Dr. Klaus Indermark
Assoc.Prof. RNDr. LubosBˇ rim
Tag der mundlichen¨ Prufung:¨ 24.01.2006
Diese Dissertation ist auf den Internetseiten der Hochschulbibliothekonlineverfugbar¨ .Abstract
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 responsiblefor 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 availableon a singlecomputer.
In this thesis, we develop parallel and, in particular, distributedalgorithmswhich ex-
ploitthecombinedresources of anetworkof commodityworkstationstosolveproblem
instances which are beyond the capabilitiesof today’s sequential algorithms.
Specifically, our algorithms solve the model-checking problem for two important
fragments of the μ-calculus which subsume many well-known temporal logics (CTL,
∗LTL, CTL ). We describe our algorithms based on a characterization of the problem
at hand in terms of two-player games. The underlying data structure, the game graph,
is colored according to the player who has a winning strategy from the current game
configuration. Finally, the color of the initial configuration tells who is the winner of
the game, and thus whether thetransition systemsatisfies theproperty or not.
Through experimentation, we found that our algorithms scale well, and are able to
solve the largest problem instances of the VLTS benchmark suite.
In a second part, we investigate ways to efficiently generate (low-level) transition
systemssuitableformanyverificationtoolsfromcompacthigh-leveldescriptionsofthe
inputmodel. Weproposeavirtual-machinebasedapproach,whichusesanintermediate
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.
We show the practicality of our approach through the example of a compiler for the
PROMELA modelling language which targets our intermediate language—the virtual-
machine’s byte-code. With a comparison of benchmarks, we show that our approach
is competitive to state-of-the-art tools like SPIN in speed, with additional advantages,
like easier reusability, and application as component in distributed model-checking al-
gorithmslike theones we proposed earlier.Acknowledgements
Firstandforemost,IsincerelythankmyadvisorProf.Dr.KlausIndermark.
From the beginning, he provided me with large degrees of freedom to pur-
sue my research interests. He was a steady source of advice and encour-
agements, and I enjoyed the many stimulating discussions about scientific,
technological and other topics.
I am grateful to Prof. Dr. Lubosˇ Brim for being a member of my thesis
committee, and for inviting me to Brno in November 2004, which initiated
an interesting and hopefully long-lastingcooperation.
I also thank the graduate college 643 ”Software fur¨ Kommunikationssys-
teme” for their financial support during the first two years of my research.
Thanks are given to everybody at I2 for a pleasant and friendly research
environment, which contributed a lot to this thesis.
I thank my friend and fellow office mate Volker Stolz, for many lively dis-
cussions and for suffering through my rants about various research-related
and -unrelated topics. Also,Dr. Benedikt Bolligand Dr. Thomas Nollhave
been great discussionpartners through the years.
My special thanks go to my friend and colleague Dr. Martin Leucker, who
crossed my way already back during my graduate studies. He sparked my
initial interest in Formal Methods, and he has always been a great source
of inspiration and advice through the years. I very much enjoyed the many
scientific as well as personal discussions.
Last, but certainly not least, my sincerest gratitude goes to Irina for all her
love, care, and unfailing support throughout my thesis. I apologize for the
long working hours and uneventfulweekends during the last year.
MichaelWeber
Aachen,November 2005Contents
1. Thesis 1
1.1.Objective................................. 2
1.2.Contributions............... 2
1.3.Overview................................. 4
I. Parallel Model Checking 5
2. A Classification of Model-checking Algorithms 7
2.1.GlobalversusLocalAlgorithms..................... 7
2.2.Explicit-stateversusSymbolicAlgorithms........ 8
2.3.ParalelversusDistributedAlgorithms.................. 8
2.4.RelatedWork....................... 9
3. Parallel Model Checking Games 13
3.1.Preliminaries............................... 13
3.2. The μ-Calculus.............. 15
3.2.1.SyntaxandSemantics...................... 15
3.2.2.GraphsofFormulas............ 20
13.2.3. Complexityof Model Checking for L ............. 25
μ
3.2.4. Model-checking Games for the μ-calculus........ 27
13.3. Winning L-games............................ 32
μ
3.3.1.SequentialColoringAlgorithms......... 36
13.4. WinningGames for L-FormulasinParalel............... 46μ
3.4.1.DistributingtheGameGraph........... 46
3.4.2. Labellingthe Game Graph .................... 47
3.4.3.AFamilyofParallelColoringAlgorithms........ 48
3.4.4.AlgorithmicVariationsandOptimizationIsues......... 52
3.4.5.CalculatingWinningstrategies.............. 55
23.5. Extensionstowards L ...................... 56
μ
3.5.1.ReducingAlternationDepth............... 56
3.5.2.AlternationandGameGraphs.............. 57
23.5.3. Coloring Algorithmfor L .................... 58
μ
i4. Implementation and Empirical Results 63
4.1.TheUppDMCImplementation...................... 63
4.2.PracticalExperiences............... 65
II. State Space Generation 73
5. State Space Generation 75
5.1. Introduction................................ 75
5.2.StatusQuo............. 75
5.3.Contributions............................... 76
5.4.Overview................. 77
6. Intermediate Formats 79
6.1.DirectTranslation............................. 80
6.2.UsinganIntermediateFormat.......... 81
6.3.ParallelStateSpaceGeneration...................... 83
7. A Virtual Machine-based Approach 85
7.1.VirtualMachineSpecification...................... 85
7.1.1.MachineState............... 86
7.1.2.Invariants......................... 89
7.1.3.Byte-codeSemantics........... 90
7.1.4.Scheduling............................ 94
7.2.StateSpaceGeneration.......... 96
7.3. UseCase: PROMELA ........................... 96
7.4.Benchmarks................ 97
7.5. Evaluationas Intermediate Language . . . . . ..............102
7.6.RelatedWork.......................104
7.6.1. PROMELASemantics...................104
7.6.2.VirtualMachines.................104
7.7.Conclusions........................106
8. Conclusions and Future Research 107
ii1. Thesis
Model checking [25], originally proposed independently by Emerson and Clarke [40]
and Quielle and Sifakis [85], is becoming more and more popular for the verification
of complex hardware and software systems. These systems are usually given by means
ofaformal descriptionthatcanbetransformedintoa(labelled)transitionsystem(LTS)
which captures the system’s essential behavior. In addition, a desired property of the
systemisusuallyspecifiedasaformulaofatemporallogic. Model-checkingalgorithms
can then answer the question whether the transition system satisfies this property. Nu-
merouscasestudieshaveshownthatthisapproachimprovestheearlydetectionoferrors
during the design process. An overviewis givenby Clarke and Wing [26].
However, the well-known state-space explosion problem still limits a broader ap-
plication of model checking. The term refers to the problem that even small system
descriptions, when converted to notions digestible by model-checking algorithms, can
expand into enormously huge transition systems. This conversion process alone can be
very time and space consuming, if done without consideration. In addition, it can lead
to unexpected or misleadingresults if not formalized rigorously.
Duringthepast20years,considerableprogressintacklingstate-spaceexplosionhave
beenachieved. Themostprominentexamplesarepartial-orderreduction[82],symbolic
model checking [74], and bounded model checking [12]. However, typical verification
taskscanstilllastdaysonasingleworkstationorareeven(practically)undecidabledue
to memoryrestrictions(as reported, for example,by Gnesiet al. [46]). Note thatevena
tenfold reduction in run-time can make the difference between practical feasibility a