Verifying concurrent systems with symbolic execution [Elektronische Ressource] : temporal reasoning is symbolic execution with a little induction / von Michael Balser

Sujets

• Informatik

Informations

• Publié par: universitat_augsburg
• Publié le: 01 janvier 2006
• Nombre de lectures: 23
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Verifying Concurrent Systems
with
Symbolic Execution
Temporal Reasoning is Symbolic Execution with a Little Induction
Dissertation
zur Erlangung des Doktorgrades Dr. rer. nat.
der Fakult¨at fu¨r Angewandte Informatik
der Universit¨at Augsburg
im Jahr 2005 von
Michael Balser
O
N
S
KAB
U
C
G
R
H
O
0
Mii
Amtierender Dekan: Prof. Dr. Wolfgang Reif
Gutachter: Prof. Dr. Wolfgang Reif
Prof. Dr. Walter Vogler
Tag der Pruf¨ ung: 12. Juli 2005
Pruf¨ er: Prof. Dr. Wolfgang Reif
Prof. Dr. Bernhard Bauer
Prof. Dr. Bernhard Mo¨lleriii
Abstract
Symbolic execution is an intuitive strategy to verify sequential programs, which can be
automated to a large extent. We have successfully carried over this method of proof to
the interactive verification of concurrent systems. The resulting strategy can be applied
to the verification of complex parallel programs and arbitrary (linear) temporal formulas.
Our underlying logic is defined such that operators for parallel programs and temporal
logic can be arbitrarily nested. We support interleaving with explicit blocking, nonde-
terministic choice, and others. Most important, the semantics of all of the operators are
compositional. Thus, systems can be abstracted and proofs can be decomposed. This
ensures that our strategy of proof can be applied to the verification of large, concurrent
systems.ivPreface
The idea of concurrency is becoming more and more important in computer science, as
computers are widely connected over the internet and even the smallest device interacts
with other devices to implement complex functionality. For example, in automotive engi-
neering,anincreasingnumberofembeddedcomputersformaconcurrentsystemtocontrol
even safety critical parts like airbags, breaks, steering, and others. It is, however, much
more difficult to design a concurrent system compared to a sequential program. Instead
of a single flow of execution, the control flow is more complex. Particularly, for reactive
systems, not only the final result of execution but the sequence of output over time is
relevant to system behaviour; additional sources of errors are insufficient synchronisation,
deadlocks, livelocks, race conditions, priority issues, and others.
The possibility of finding errors by means of testing strategies is limited, because, es-
pecially for interleaved systems, an exponential amount of possible executions must be
considered. Theexecutionisnondeterministic, makingitdifficulttoreproduceerrors. An
alternativetotestingistheuseofformalmethodstospecifyandverifyconcurrentsystems
with mathematical rigour. In practice, automatic methods – especially model checking
– are successfully applied to discover flaws in the design and implementation of systems.
Part of the success of model checking is due to the fact that it can be applied by soft-
ware engineers without being experts in formal methods. However, automatic stategies
are limited to small and medium sized state finite applications. Large and state infinite
systems must be manually abstracted to ensure that formal analysis terminates. Manual
abstraction is difficult and calls for an expert with formal background; the soundness of
the abstraction must be ensured.
Instead of automatic algorithms, large and state infinite systems can be analysed with
interactive verification. Existing calculi to reason about concurrent systems are gener-
ally difficult to apply. The strategy of symbolic execution, on the other hand, has been
successfully applied to the interactive verification of sequential programs. Symbolic ex-
ecution gives intuitive proofs with a high degree of automation, and can therefore be
applied, to some extend, by non-experts. Our idea is to carry over symbolic execution to
the interactive verification of temporal properties of concurrent systems.
Related work This work is inspired by the following existing approaches.
vvi
Using Temporal Logic of Actions (TLA) [18], concurrent systems can be combined with
simple logical conjunction [1]. Conjunction of systems is compositional and proofs can be
decomposed! However,systemmodelsinTLAarerestrictedtosimplestatetransitionsys-
tems; complexprogrammingconstructslikeloops, conditionals, interleaving, synchronous
execution, etc. must be translated into basic transitions with additional program coun-
ters. The interactive calculus of [18] to verify temporal properties of systems in TLA is
very basic, and it is difficult to automate part of the deduction.
The Stanford Temporal Prover (STeP) [6] offers a rich input language supporting inter-
leaved parallel processes, message passing, and other features. The systems are auto-
matically translated into fair transition systems to which model checking or deductive
reasoning can be applied. Especially the use of verification diagrams as a high level
abstraction of proofs in temporal logic is of interest. However, verification diagrams in
practice are restricted to the verification of a certain class of temporal properties. We
hope that symbolic execution is more automatic than verification in STeP and that the
strategy can be efficiently applied to any type of temporal property. Furthermore, we try
to directly support the original system model within the interactive calculus instead of
translating the model to a (fair) transition system.
Our temporal logic is based on Interval Temporal Logic (ITL) [22] which is a linear time
logic and combines temporal formulas and program operators within the same formalism.
We have enriched the set of program operators by interleaving, nondeterministic choice,
and others. To some extent, we also consider branching time logics, e.g., Computation
Tree Logic (CTL) [8].
Early parts of this work have been integrated into the Verification Support Environment
(VSE)[16]. Amoreadvancedimplementationoftheproofmethodwithdirectsupportfor
parallel programs with interleaving and advanced heuristics for automation is available
in the KIV system [27] [4].
Overview Chapter1givesanextendedoverviewofourapproach. Syntaxandsemantics
of our logic is formally defined in Chapter 2. The recipe for interactive verification
of concurrent systems with symbolic execution is outlined in Chapter 3. It consists of
four ingredients: (i) symbolic execution which is described in Chapter 4, (ii) sequencing
to reduce the number of execution paths to be considered in a proof (see Chapter 5),
(iii) induction in Chapter 6, and (iv) abstraction to structure proofs for large systems
(Chapter 7). Chapter 8 contains a comparison, summarises open issues and concludes.
A list of calculus rules are part of the Appendices A and B. Proofs have been put into
Appendix C unless they directly contribute to the understanding of the material. Finally,
Appendix D contains a summary of mathematical symbols.
Acknowledgements I would like to thank Prof. Wolfgang Reif for his considerable
support and motivation, Dr. Gerhard Schellhorn for fruitful discussions and stimula-
tions,ChristophDuelli,JonathanSchmitt,SimonBa¨umler,FrankOrtmeier,andAndreasvii
Thums, members of our working group who were directly involved in the interactive ver-
ification of concurrent systems and who provided valuable feedback and ideas, Thomas
Sorg who defined first steps for this approach in his master thesis, Florian Nafz, Nadhem
Kachroudi, and Alwin Hoffmann, student workers who implemented and evaluated parts
of the strategy, all partners of the Protocure project where the proof method has been
applied to the verification of medical guidelines, Werner Balser for proof reading, and
Karin Balser for her loving support and understanding of a crazy logician.viiiContents
Preface v
1 Motivation 1
1.1 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.4 Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.5 Ingredient 1 – Symbolic Execution . . . . . . . . . . . . . . . . . . . . . . 6
1.6 Ingredient 2 – Sequencing . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.7 Ingredient 3 – Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.8 Ingredient 4 – Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.9 Outlook . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2 Syntax and Semantics 21
2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.3 Synchronisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
2.4 Interleaving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
2.5 SOS notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
2.6 Interleaving intervals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
2.7 Dijkstra’s choice operator . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.8 Atomic steps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
2.9 Labels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
ixx CONTENTS
2.10 Restricted expressi