Suchen und Finden
Service
Handbook of Model Checking
Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem
Verlag Springer-Verlag, 2018
ISBN 9783319105758 , 1210 Seiten
Format PDF, OL
Kopierschutz Wasserzeichen
Handbook of Model Checking
3
Foreword
6
Preface
7
Acknowledgements
8
Contents
10
Contributors
18
Chapter 1: Introduction to Model Checking
22
1.1 The Case for Computer-Aided Veri?cation
22
1.2 Temporal-Logic Model Checking in a Nutshell
27
1.2.1 Kripke Structures
27
1.2.2 The Temporal Logic CTL
28
1.2.3 The Temporal Logic CTL
31
1.2.4 The Temporal Logic LTL
33
1.3 A Very Brief Guide Through the Chapters of the Handbook
34
1.3.1 The Algorithmic Challenge
36
1.3.2 The Modeling Challenge
39
1.4 The Future of Model Checking
40
References
43
Chapter 2: Temporal Logic and Fair Discrete Systems
48
2.1 Introduction
49
2.2 Fair Discrete Systems
50
2.2.1 Kripke Structures
51
2.2.2 De?nition of Fair Discrete System
51
2.2.3 Representing Programs
54
2.2.4 Algorithms
58
2.3 Linear Temporal Logic
62
2.3.1 De?nition of Linear Temporal Logic
63
2.3.2 Safety Versus Liveness and the Temporal Hierarchy
64
2.3.3 Extensions of LTL
67
2.3.4 Temporal Testers, Satis?ability, and Model Checking
71
2.4 Computation Tree Logic
73
2.4.1 De?nition of Computation Tree Logic
74
2.4.2 Extensions
75
2.4.3 Model Checking and Satis?ability
77
2.5 Examples for LTL and CTL
80
2.5.1 Invariance and Safety
81
2.5.2 Liveness
82
2.5.3 Additional Examples
83
2.6 CTL*
84
2.6.1 Branching vs. Linear Time
84
2.6.2 CTL* De?nition
88
2.6.3 Examples of Usage of CTL*
89
2.6.4 Model Checking and Satis?ability
90
References
91
Chapter 3: Modeling for Veri?cation
95
3.1 Introduction
95
3.2 Major Considerations in System Modeling
97
3.2.1 Selecting a Modeling Formalism and Language
98
3.2.1.1 Type of System
98
3.2.1.2 Type of Property
99
3.2.1.3 Modeling the Environment
99
3.2.1.4 Level of Abstraction
100
3.2.1.5 Clarity and Modularity
100
3.2.1.6 Form of Composition
101
3.2.1.7 Computational Engines
101
3.2.1.8 Practical Ease of Modeling and Expressiveness
102
3.2.2 Modeling Languages
102
3.2.3 Challenges in Modeling
103
3.2.4 Scope of This Chapter
105
3.3 Modeling Basics
106
3.3.1 Syntax
106
3.3.2 Dynamics
107
3.3.3 Modeling Concepts
108
3.4 Examples
109
3.4.1 Synchronous Circuits
110
3.4.1.1 Router Design
110
3.4.1.2 Simpli?cations and sml Model
111
3.4.1.3 Veri?cation Task: Progress Through the Router
111
3.4.1.4 Data Type Abstraction
113
3.4.1.5 Environment Modeling
114
3.4.1.6 Summary
116
3.4.2 Synchronous Control Systems
116
3.4.3 Concurrent Software
118
3.5 Kripke Structures
120
3.5.1 Transition Systems
121
3.5.2 From sml Programs to Kripke Structures
122
3.6 Summary
123
References
123
Chapter 4: Automata Theory and Model Checking
126
4.1 Introduction
126
4.2 Nondeterministic Büchi Automata on In?nite Words
127
4.2.1 De?nitions
127
4.2.2 Closure Properties
129
4.2.2.1 Closure Under Union and Intersection
129
4.2.2.2 Closure Under Complementation
131
4.2.3 Determinization
139
4.3 Additional Acceptance Conditions
141
4.3.1 Translations Among the Different Classes
143
4.3.1.1 Translations Among the Different Conditions
143
4.3.1.2 Typeness
143
4.3.1.3 Translations That Require a New State Space
145
4.3.2 Determinization of NBWs
149
4.4 Decision Procedures
151
4.5 Alternating Automata on In?nite Words
154
4.5.1 De?nition
155
4.5.2 Closure Properties
156
4.5.3 Decision Procedures
158
4.6 Automata-Based Algorithms
160
4.6.1 Translating LTL to Büchi Automata
161
4.6.1.1 A Translation via ABWs
161
4.6.1.2 A Direct Translation to NBWs
163
4.6.1.3 The Blow-up in the LTL to NBW Translation
164
4.6.2 Model Checking and Satis?ability
165
References
167
Chapter 5: Explicit-State Model Checking
171
5.1 Introduction
171
5.1.1 The Importance of Abstraction
172
5.2 Basic Search Algorithms
173
5.3 Linear Temporal Logic
176
5.4 Omega Automata
176
5.5 Nested Depth-First Search
178
5.6 Abstraction
180
5.6.1 Tic-Tac-Toe
181
5.7 Model-Driven Veri?cation
185
5.8 Incomplete Storage
186
5.8.1 Bitstate Hashing and Bloom Filters
186
5.9 Extensions
187
5.10 Synopsis
188
References
188
Chapter 6: Partial-Order Reduction
190
6.1 Introduction
190
6.2 Partial Order Reduction
191
Reduction for LTL
193
On-the-Fly Model Checking
197
Reduction for CTL
198
Reduction for Process Algebra
199
Reducing Visibility
199
6.3 Reducing Edges While Preserving States
199
Sleep Sets
200
Trace Normal Form
201
Edge Lean Algorithm
204
6.4 Conclusions
205
References
205
Chapter 7: Binary Decision Diagrams
208
7.1 Introduction
208
7.2 Terminology
209
7.3 A Boolean Function API
210
7.4 OBDD Representation
212
7.5 Implementing OBDD Operations
214
7.6 Implementation Techniques
217
7.7 Variable Ordering and Reordering
219
7.8 Variant Representations
220
7.9 Representing Non-Boolean Functions
223
7.10 Scaling OBDD Capacity
227
Comparison to SAT Checking
229
7.11 Concluding Remarks
230
References
231
Chapter 8: BDD-Based Symbolic Model Checking
235
8.1 Introduction
235
8.2 Preliminaries
236
8.3 Binary Decision Diagrams: The Basics
238
8.3.1 Representing Sets and Relations
238
8.3.1.1 Characteristic Function
238
8.3.1.2 Representing Sets
239
8.3.1.3 Representing Relations
240
8.3.2 Image Computation
240
8.3.3 Partitioned Transition Relation
242
8.3.3.1 Disjunctive Decomposition
242
8.3.3.2 Conjunctive Decomposition
243
8.3.4 Historical Perspective
244
8.4 Model Checking Kripke Structures
246
8.4.1 Reachability/Invariant/AG
247
8.4.2 CTL Model Checking
247
8.4.3 Fair CTL Model Checking
249
8.4.3.1 Function egFairStates
250
8.4.3.2 Function ctlFairStates
251
8.4.4 LTL Model Checking
251
8.4.4.1 Restricted Path Formula
252
8.4.4.2 Algorithm ltlTableau
253
8.5 Push-Down Symbolic Model Checking
254
8.6 Conclusion
259
References
260
Chapter 9: Propositional SAT Solving
262
9.1 Introduction
262
9.2 Preliminaries
264
9.3 CDCL SAT Solvers: Organization
267
9.4 CDCL SAT Solvers
268
9.4.1 Clause Learning and Non-chronological Backtracking
269
9.4.2 Unique Implication Points
271
9.4.3 Learned Clause Minimization
274
9.4.4 Lazy Data Structures
276
9.4.5 Search Restarts
278
9.4.6 Lightweight Branching Heuristics
278
9.4.7 Additional Techniques and Recent Trends
279
9.5 SAT-Based Problem Solving
279
9.5.1 Incremental SAT
280
9.5.2 Unsatis?able Cores
280
9.5.3 CNF Encodings
281
9.5.4 Optimization
282
9.5.5 Model Enumeration
282
9.5.6 Minimal Sets
283
9.5.7 Quanti?cation
283
9.6 Research Directions
284
References
284
Chapter 10: SAT-Based Model Checking
291
10.1 Introduction
291
10.2 Bounded Model Checking on Kripke Structures
292
10.2.1 Kripke Structures
292
10.2.2 Safety Properties
293
10.2.3 Liveness Properties
294
10.2.3.1 Liveness to Safety Translation
295
10.2.3.2 k-Liveness
295
10.3 Bounded Model Checking for Hardware Designs
295
10.3.1 Hardware Description Languages (HDLs)
296
10.3.2 BMC on Net-Lists
296
10.4 Bounded Model Checking for Software
297
10.4.1 Monolithic Encodings
298
10.4.2 Path-Based Encodings
298
10.4.3 Completeness for Bounded Programs
299
10.4.4 BMC for Multi-threaded Programs
300
10.4.5 Bounded Model Checking for HW/SW Co-veri?cation
300
10.5 Encodings into Propositional SAT
301
10.5.1 Encoding Bit Vectors
301
10.5.2 Encoding Memory
302
10.5.3 Encodings with Under- and Over-approximation
302
10.6 Complete Model Checking with SAT
303
10.6.1 Completeness Thresholds
303
10.6.2 Image Computation with SAT
303
10.6.3 Basic Inductive Techniques
304
10.6.3.1 Strengthening the Inductive Argument
304
10.6.3.2 Equivalence Reasoning
304
10.6.3.3 Temporal Decomposition
305
10.6.3.4 k-Induction
305
10.6.4 Craig Interpolation
305
10.6.5 Iterative Inductive Strengthening
306
10.7 Abstraction Techniques Using SAT
306
10.7.1 Overview of Predicate Abstraction
306
10.7.2 Computing Abstractions with SAT
307
10.7.3 Simulation with SAT
308
10.7.4 Abstraction-Based Tools
308
10.8 Outlook and Conclusions
309
References
309
Chapter 11: Satis?ability Modulo Theories
318
11.1 Introduction
318
11.1.1 Technical Preliminaries
320
11.2 SMT in Model Checking
323
11.3 The Lazy Approach to SMT
325
11.3.1 A Basic Lazy SMT Solver
326
11.3.2 SAT Engine and Theory Solver Features
326
11.3.3 A General Framework and Architecture
328
11.4 Theory Solvers for Speci?c Theories
330
11.4.1 Uninterpreted Function Symbols
330
11.4.2 Real Arithmetic
331
11.4.3 Integer Arithmetic
332
11.4.4 Mixed Integer and Real Arithmetic
334
11.4.5 Difference Logic
334
11.4.6 Bit Vectors
335
11.4.7 Arrays
336
11.4.8 Other Theories
337
11.5 Combining Theory Solvers
337
11.5.1 A Basic Combination Method
338
11.5.2 Combination Variants and Extensions
339
11.6 SMT Solving Extensions and Enhancements
340
11.7 Eager Encodings to SAT
343
11.8 Additional Functionalities of SMT Solvers
345
References
348
Chapter 12: Compositional Reasoning
357
12.1 Introduction
357
12.2 Reasoning with Assertions
360
12.2.1 The (Non-compositional) Owicki-Gries Method
360
12.2.2 The Assume-Guarantee View: Localized Inductive Invariants
361
12.2.2.1 The Shared-Variable Program Model
362
A Note on Notation
362
Invariant Assertions
362
12.2.2.2 Split Invariants
363
12.2.3 Computing the Strongest Split Invariant
364
Split Invariance for N Processes
365
12.2.4 Relationship to Rely-Guarantee
366
12.2.5 Completeness Issues
366
12.2.6 Deadlock Detection with Local Invariants
368
12.2.7 Local Proofs for Termination, Temporal Properties, and Fairness
368
12.2.7.1 Background
368
12.2.7.2 Local Proof Rules for Liveness Properties
369
12.2.8 Algorithms for Local Analysis of Temporal Properties
370
12.2.9 Automating the Discovery of Auxiliary Variables
371
12.2.10 Local Symmetry
373
12.2.11 Further Reading
374
12.3 Automata-Based Assume-Guarantee Reasoning
374
12.3.1 Formalisms
374
12.3.1.1 Finite-State Machines
374
12.3.1.2 Parallel Composition of FSMs
375
12.3.1.3 Properties
375
12.3.1.4 Complementation
376
12.3.2 Assume-Guarantee Reasoning
376
12.3.2.1 Assume-Guarantee Triples
376
12.3.2.2 Weakest Assumption
376
12.3.2.3 Basic Assume-Guarantee Rule
377
Rule ASym
377
12.3.2.4 Soundness and Completeness
377
12.3.3 Automation of Basic Assume-Guarantee Rule
378
12.3.3.1 The L* algorithm
378
12.3.3.2 Learning-Based Assumption Generation
379
12.3.3.3 Correctness Arguments
381
12.3.4 Example
381
12.3.5 Additional Assume-Guarantee Rules and Their Automation
384
Rule ASymN
384
Rule Circ-0
385
Rule Sym
385
Rule SymN
386
Rule Circ
386
Rule Circ-Ind
386
12.4 Related Approaches
387
12.4.1 Learning for Compositional Veri?cation
387
12.4.2 Assumption Generation by Abstraction-Re?nement
387
12.4.3 Components and Interfaces
388
12.4.4 Other Modular Reasoning Frameworks
389
12.5 Conclusion
390
References
390
Chapter 13: Abstraction and Abstraction Re?nement
396
13.1 Introduction
396
13.2 Preliminaries
398
13.2.1 Abstraction Frameworks
398
13.2.2 Kripke Structures
399
13.2.3 The µ-Calculus
401
13.2.3.1 Some Notes on the Difference Between Lµ and CTL/CTL*
403
13.3 Simulation and Bisimulation Relations
405
13.3.1 Simulation Relation
405
13.3.2 Bisimulation Relation
407
13.3.3 Additional Reading
409
13.4 Abstraction Based on Simulation
410
13.4.1 Existential Abstraction
410
13.4.1.1 Speci?c Abstractions: Examples
412
13.4.2 Additional Reading
413
13.5 CounterExample-Guided Abstraction Re?nement (CEGAR)
413
13.5.1 The CEGAR Framework
415
13.5.1.1 Identifying Spurious Path Counterexamples
415
13.5.2 Additional Reading
417
13.6 Abstraction Based on Modal Simulation
417
13.6.1 A Three-Valued Setting
420
13.6.2 Re?nement
422
13.6.3 Additional Reading
422
13.7 Completeness
423
13.7.1 Additional Reading
424
References
425
Chapter 14: Interpolation and Model Checking
431
14.1 Introduction
431
14.2 Preliminaries
433
14.3 Model of Abstraction Re?nement
434
14.3.1 A Simple Programming Language and Proof System
435
14.3.2 The Abstractor
436
14.3.3 The Re?ner
438
14.4 Re?nement, Local Proofs, and Interpolants
438
14.4.1 Craig Interpolation
439
14.4.2 Feasible Interpolation in Model Checking
441
14.4.3 Interpolants and Local Proofs
441
14.5 Re?ners as Local Proof Systems
444
14.5.1 Strongest Post-condition
444
14.5.2 Weakest Pre-condition
447
14.5.3 Bounded Provers
448
14.5.4 Split Provers and Language Strati?cation
449
14.5.5 Constraint-Based Interpolation
450
14.5.6 Feasible Interpolation and Re?nement
450
14.5.7 Improving Interpolants
451
14.6 Abstractors as Proof Generalizers
451
14.7 Summary
453
References
454
Chapter 15: Predicate Abstraction for Program Veri?cation
457
15.1 Introduction
457
15.2 De?nitions
458
15.2.1 Programs
458
15.2.2 Correctness: Safety and Termination
461
15.3 Characterizing Correctness via Reachability
462
15.3.1 Safety and Reachability
462
15.3.2 Termination and Binary Reachability
463
15.4 Characterizing Correctness via Inductiveness
464
15.4.1 Safety and Closure Under post
464
15.4.2 Termination and Transitive Closure
467
15.5 Abstraction
469
15.5.1 Safety and Predicate Abstraction
470
15.5.2 Termination and Transition Predicate Abstraction
476
15.6 Abstraction Re?nement
481
15.6.1 Re?nement of Predicate Abstraction
482
15.6.2 Re?nement of Transition Predicate Abstraction
488
15.7 Solving Re?nement Constraints for Predicate Abstraction
491
15.7.1 Least Solution
492
15.7.2 Greatest Solution
493
15.7.3 Intermediate Solution Using Interpolation
495
15.8 Tools
496
15.9 Conclusion
497
References
497
Chapter 16: Combining Model Checking and Data-Flow Analysis
502
16.1 Introduction
503
16.2 General Considerations
503
16.2.1 Type Checking
503
16.2.2 Data-Flow Analysis
505
16.2.3 Model Checking
508
16.3 Unifying Formal Framework/Comparison of Algorithms
510
16.3.1 Preliminaries
510
16.3.2 Algorithm of Data-Flow Analysis
513
16.3.3 Algorithm of Model Checking
515
16.3.4 Uni?ed Algorithm Using Con?gurable Program Analysis
515
16.3.5 Discussion
518
16.3.6 Composition of Con?gurable Program Analyses
519
16.4 Classic Examples (Component Analyses)
520
16.4.1 Reachable-Code Analysis
520
16.4.2 Constant Propagation
521
16.4.3 Reaching De?nitions
522
16.4.4 Predicate Analysis
524
16.4.5 Explicit-Heap Analysis
525
16.4.6 BDD Analysis
526
16.4.7 Observer Automata
527
16.5 Combination Examples (Composite Analyses)
529
16.5.1 Predicate Analysis + Constant Propagation
529
16.5.2 Predicate Analysis + Constant Propagation + Strengthen
530
16.5.3 Predicate Analysis + Explicit-Heap Analysis
532
16.5.4 Predicate Analysis + Observer Automata
532
16.6 Algorithms for Constructing Program Invariants
534
16.6.1 Iterative and Monotonic Fixed-Point Approaches
534
16.6.2 Counterexample-Guided Abstraction Re?nement
535
16.6.3 Template- and Constraint-Based Approaches
536
16.6.4 Proof-Rule-Based Approaches
537
16.6.5 Iterative, but Non-monotonic Approaches
537
16.6.6 Comparison with Standard Recurrence Solving
538
16.6.7 Discussion
540
16.7 Combinations in Tool Implementations
541
16.8 Conclusion
541
References
543
Chapter 17: Model Checking Procedural Programs
550
17.1 Introduction
550
17.2 Models of Procedural Programs
552
17.2.1 (Extended) Recursive State Machines
553
17.2.2 Pushdown Systems
554
17.2.3 From RSMs to PDSs
555
17.3 Basic Veri?cation Algorithms
556
17.3.1 The State Reachability Problem: Computing Summaries
556
17.3.2 The Fair Computation Problem
559
17.3.3 The Con?guration Reachability Problem: Saturating Automata
560
17.3.3.1 Computing pre*(C) for a Regular Set C by Saturation
561
17.3.3.2 Computing post*(C) for a Regular Set C by Saturation
562
17.3.4 The Generalized Fair Computation Problem
564
17.4 Specifying Requirements
565
17.4.1 Nested Words
566
17.4.2 Nested Word Automata
567
17.4.2.1 RSMs as NWAs
568
17.4.2.2 NWAs for Requirements
569
17.4.2.3 Closure Properties
570
17.4.2.4 Decision Problems
570
17.4.2.5 MSO Equivalence
571
17.4.3 Temporal Logics
571
17.4.3.1 Abstract Next
572
17.4.3.2 Abstract Paths
573
17.4.3.3 Summary Paths
573
17.4.3.4 Model Checking
574
17.5 Bibliographical Remarks
575
17.5.1 Summarization
575
17.5.2 Saturation
576
17.5.3 Temporal Logic Model Checking
577
References
578
Chapter 18: Model Checking Concurrent Programs
582
18.1 Introduction
583
18.2 Concurrent System Model and Notation
585
18.2.1 Synchronization and Communication
587
18.2.2 Speci?cation Logic
587
18.2.3 Interacting Pushdown System (PDS) Model
588
18.3 PDS-Based Model Checking: Synchronization Patterns
589
18.3.1 Programs with Nested Locks
590
18.3.1.1 Pair-wise Reachability for Nested Locks
590
18.3.1.2 Model-Checking Programs with Nested Locks
591
18.3.2 Programs with Locks: Lock Causality Graph
595
18.3.3 Programs with Bounded Lock Chains
597
18.3.4 Discussion: Lock Patterns
600
18.3.5 Programs with Rendezvous
601
18.3.5.1 Computing Over-approximations of Path Languages
602
18.3.5.2 De?ning Re?nable Finite-Chain Abstractions
603
18.3.5.3 Checking Whether the Counterexample Is Spurious
604
18.3.5.4 The Semi-decision Procedure
604
18.4 PDS-Based Model-Checking: Communication Patterns
604
18.4.1 Reasoning About Programs with State Observation
605
18.4.1.1 Symbolic Representation of PDN Con?gurations
605
18.4.1.2 Reachability Analysis of PDNs
606
18.4.2 Multiphase Acyclic Pushdown Networks
606
18.4.2.1 The Reachability Problem for MAPNs
607
18.4.2.2 For MAPNs
608
18.4.2.3 A Semi-algorithm for k-Bounded Reachability for MAPNs
609
18.4.2.4 A Semi-algorithm for the Reachability Problem for General PDNs
610
18.4.3 Threads Communicating via Lossy Channels
610
18.5 Other Models: Finite State Systems and Sequential Programs
611
18.5.1 Partial-Order Reduction
612
18.5.2 Symbolic Reasoning with Memory Consistency Constraints
613
18.5.3 Concurrent Data?ow Analysis and Invariant Generation
614
18.5.4 Trace-Based Dynamic Model-Checking
615
18.5.5 Other Related Techniques
616
References
616
Chapter 19: Combining Model Checking and Testing
621
19.1 Introduction
621
19.2 Systematic Testing of Concurrent Software
623
19.2.1 Classical Model Checking
623
19.2.2 Software Model Checking Using a Dynamic Semantics
623
19.2.3 Systematic Testing with a Run-Time Scheduler
627
19.2.4 Stateless vs. Stateful Search
628
19.2.5 Systematic Testing for Multi-threaded Programs
629
19.2.6 Tools and Applications
631
19.3 Systematic Testing of Sequential Software
632
19.3.1 Classical Symbolic Execution
632
19.3.2 Static Test Generation
633
19.3.3 Dynamic Test Generation
634
19.3.4 Systematic Dynamic Test Generation
635
19.3.5 Strengths and Limitations
639
19.3.6 Tools and Applications
640
19.4 Systematic Testing of Concurrent Software with Data Inputs
641
19.4.1 Example
642
19.4.2 Comparison with Related Work
643
19.5 Other Related Work
645
19.6 Conclusion
648
References
648
Chapter 20: Combining Model Checking and Deduction
658
20.1 Introduction
658
20.2 Logic Background
663
20.2.1 Propositional Logic
663
20.2.2 First-Order Logic
668
20.2.3 Higher-Order Logic
672
20.2.4 PVS: Computation and Deduction
673
20.2.5 Hoare Logic
674
20.3 Deduction and Model Checking
677
20.3.1 Abstract Interpretation
677
20.3.2 Symbolic Model Checking
679
20.3.3 Predicate Abstraction
680
20.3.4 Bounded Model Checking and k-Induction
682
20.3.5 Symbolic Execution and Test Generation
683
20.3.6 Interpolation-Based Model Checking
684
20.3.7 Con?ict-Directed Reachability
685
20.4 Conclusions
687
References
687
Chapter 21: Model Checking Parameterized Systems
692
21.1 Introduction
692
21.2 Petri Nets
694
21.2.1 Simple Protocol
694
21.2.2 Petri Nets
695
21.2.3 Safety Properties
697
21.2.4 Backward Reachability Analysis
698
21.2.5 Liveness Properties
701
21.3 Regular Model Checking
702
21.3.1 Near-Neighbor Communication
702
21.3.2 Regular Model Checking
703
21.3.3 Acceleration Techniques
705
Safety Properties
705
Column Transducer
706
Quotienting
707
Example
709
21.4 Monotonic Abstraction
710
21.4.1 Example
711
21.4.2 Model
712
21.4.3 Over-Approximation
713
21.4.4 Backward Reachability Algorithm
714
21.5 Compositional Reasoning for Parameterized Veri?cation
716
21.5.1 Parameterized Protocols
716
Index Variables
717
States
717
Expressions
717
Assignments
717
Rules
718
Protocols
718
Safety Properties
718
21.5.2 The CMP Method
719
21.5.2.1 German's Protocol
720
21.5.2.2 Abstraction
720
21.5.2.3 Strengthening
722
21.5.2.4 Correctness
723
21.5.3 Evolution of the CMP Method
725
21.5.4 Applications
725
21.6 Related Work
726
References
728
Chapter 22: Model Checking Security Protocols
733
22.1 Introduction
733
22.2 History
737
22.3 Formal Model
739
22.3.1 Notational Preliminaries
740
22.3.2 Terms and Events
740
22.3.3 Protocols and Threads
742
22.3.4 Initial Adversary Knowledge
743
22.3.5 Execution Model
743
22.3.6 Property Speci?cation
745
22.3.7 Alternatives
746
22.4 Issues in Developing Model-Checking Algorithms for Security Protocols
747
22.4.1 Forward Versus Backward Search
747
22.4.2 Bounded Instances
748
22.4.3 Representing States
749
22.4.4 Partial-Order Reduction
751
22.4.5 Handling Equations
752
22.5 Systems and Algorithms
754
22.5.1 NPA and Maude-NPA
754
22.5.2 AVISPA and Related Tools
755
22.5.3 Athena, Scyther, and Tamarin
757
22.5.4 ProVerif
758
22.6 Research Problems
759
22.6.1 Link to Computational Soundness
759
22.6.2 Corruption Models
760
22.6.3 Channel Properties
761
22.6.4 Other Properties, Including Non-trace Properties
761
22.6.5 Probabilities
762
22.7 Conclusions
763
References
764
Chapter 23: Transfer of Model Checking to Industrial Practice
769
23.1 Introduction
769
23.1.1 Anything Worth Inventing Is Worth Reinventing
770
23.1.2 The Interplay Between Theory and Application
772
23.2 The Technology Transfer Problem
773
23.2.1 Initial Challenges
773
23.2.2 Barriers to Technology Transfer
774
23.2.3 Methodological Differences and New Potential Bene?ts
775
23.2.4 The Cost of Writing Properties vs. a Test Bench
776
23.2.5 Settling on a Scope for Model Checking
777
23.2.6 The First Commercial Successes
779
23.2.7 The Essentiality of Being Able to Compare Tools
780
23.2.8 In Summary
781
23.3 False Starts
782
23.4 A Framework for Technology Transfer
785
23.5 Formal Functional Veri?cation in Commercial Use Today
788
23.6 Algorithms
792
23.7 Future
794
23.8 Conclusion
795
References
796
Chapter 24: Functional Speci?cation of Hardware via Temporal Logic
800
24.1 Introduction
800
24.2 From LTL to Regular-Expression-Based Temporal Logic
802
24.2.1 Adding Expressive Power-Suf?x Implication
803
24.2.2 Adding Succinctness
804
24.2.2.1 Counting
804
24.2.2.2 First Match
805
24.2.2.3 Intersection
805
24.2.2.4 Fusion
806
24.2.2.5 Past Operators
807
24.2.3 Distinguishing Between Weak and Strong Regular Expressions
807
24.3 Clocks and Sampling
810
24.3.1 Hardware Clocks
810
24.3.2 Using a Clock as a Time-Sampling Abstraction
814
24.4 Hardware Resets and Other Sources of Truncated Paths
814
24.4.1 Hardware Resets
815
24.4.2 Other Sources of Truncated Paths
817
24.4.3 The Truncated Semantics and Classi?cation of Safety Formulas
820
24.5 The Simple Subset
822
24.6 Quanti?ed and Local Variables
823
24.6.1 Quanti?ed Variables
823
24.6.2 Local Variables
824
24.7 Summary and Open Issues
828
24.7.1 One-to-One Correspondence
828
24.7.2 Triggering Procedural Code from Within a Formula
829
24.7.3 Separation of Concerns
829
References
830
Chapter 25: Symbolic Trajectory Evaluation
835
25.1 Introduction
835
25.2 Notational Preliminaries
837
25.3 Sequential Circuit Models in STE
838
25.3.1 States and Sequences
838
25.3.2 Abstraction
839
25.3.3 Time-Dependent Behaviour
840
25.3.4 The Next State Function and Trajectories
841
25.4 Trajectory Evaluation Logic
842
25.4.1 Correctness Properties for Veri?cation
844
25.4.2 Correctness Properties Under Assumptions
846
25.4.3 Internal Combinational Circuitry
846
25.5 The Fundamental Theorem of Trajectory Evaluation
847
25.6 STE Model Checking
848
25.6.1 The Symbolic Model-Checking Algorithm
850
25.6.2 Some Small Examples in Detail
852
25.6.3 Model Checking Properties Under Assumptions
854
25.7 Abstraction and Symbolic Indexing
856
25.7.1 Symbolic Indexing
857
25.8 Compositional Reasoning
861
25.8.1 The STE Deductive System
862
25.8.2 Relational STE
864
25.9 GSTE and Other Extensions
866
25.9.1 Generalized Symbolic Trajectory Evaluation
868
25.10 Summary and Prospects
869
References
871
Chapter 26: The mu-calculus and Model Checking
875
26.1 Introduction
875
26.2 Basics
876
26.2.1 Syntax and Semantics
876
26.2.2 Alternation Depth
882
26.2.3 Semantics in Terms of Games
884
26.2.3.1 Games
886
26.2.3.2 Veri?cation Game
887
26.2.4 Model Checking
891
26.3 Fundamental Properties
894
26.3.1 Bisimulation Invariance and the Tree-Model Property
895
26.3.2 Modal Automata
896
26.3.3 Satis?ability
900
26.3.4 Alternation Hierarchy
903
26.3.5 Proof System
905
26.3.6 Interpolation Property
905
26.3.7 Division Property
906
26.4 Relations with Other Logics
908
26.4.1 MSOL, Binary Trees and Bisimulation Invariance
908
26.4.2 Embedding of Program Logics
910
26.4.3 Beyond µ-Calculus
912
26.4.3.1 Iterated Structures
912
26.4.3.2 Guarded Logics
914
26.5 Related Work
916
References
918
Chapter 27: Graph Games and Reactive Synthesis
924
27.1 Introduction
924
27.2 Theory of Graph-Based Games
926
27.2.1 Game Graphs and Strategies
927
27.2.2 Objectives
928
27.2.3 Winning and Optimal Strategies; Decision Problems
930
27.2.4 Complexity and Algorithms for Graph Games with Qualitative Objectives
930
27.2.5 Complexity and Algorithms for Graph Games with Quantitative Objectives
935
27.2.6 Reducibility Between Graph Games
937
27.2.7 Extensions
937
27.3 Reactive Synthesis
939
27.3.1 Introduction
939
27.3.2 Games, Transducers, Trees, and Automata
941
27.3.3 Realizability and Synthesis Problem
945
27.3.4 Classical Approach to LTL Synthesis
946
Step 1: LTL to NBW
946
Step 2: NBW to DPW
946
Step 3: DPW to DPT
947
Step 4: DPT Emptiness Check
947
Step 5: Construction of Finite-State Transducer
948
27.3.5 Recent Approaches to LTL Synthesis
949
27.3.5.1 Bounded (or Safraless) Approaches
949
Step 1: LTL to UCT
950
Step 2: UCT to k-UCT
951
Step 3: k-UCT Emptiness Check
952
Step 4: System Construction
954
27.3.5.2 Approaches for Fragments of LTL
954
27.4 Related Topics
956
References
957
Chapter 28: Model Checking Probabilistic Systems
966
28.1 Introduction
967
28.1.1 Temporal Logics for Specifying Probabilistic Properties
967
28.1.2 Model-Checking Algorithms for Probabilistic Systems
969
28.1.3 Outline
969
28.2 Modelling Probabilistic Concurrent Systems
969
28.2.1 Preliminaries
970
28.2.2 Markov Decision Processes
970
28.2.3 Markov Chains
973
28.2.4 Schedulers
973
28.2.5 Probability Measures in MDPs
974
28.2.6 Maximal and Minimal Probabilities for Path Events
975
28.2.7 Maximal and Minimal Expected Cost
976
28.3 Probabilistic Computation Tree Logic
978
28.3.1 Syntax of PCTL
978
28.3.2 Semantics of PCTL
979
28.3.3 Derived Operators
981
28.4 Model-Checking Algorithms for MDPs and PCTL
983
28.4.1 Probability Operator
983
28.4.2 Expectation Operator
986
28.5 Linear Temporal Logic
988
28.5.1 Syntax of LTL
988
28.5.2 Semantics of LTL
989
28.5.3 Derived Operators
989
28.5.4 LTL Model-Checking Problem
989
28.6 Model-Checking Algorithms for MDPs and LTL
990
28.7 Tools, Applications and Model Construction
993
28.7.1 Tool Support
993
28.7.2 Applications
994
28.7.3 Construction of Probabilistic Models
994
28.8 Extensions of the Model and Speci?cation Notations
995
28.9 Conclusion
996
References
996
Chapter 29: Model Checking Real-Time Systems
1003
29.1 Introduction
1003
29.2 Timed Automata
1005
29.3 Checking Reachability
1009
29.3.1 Region Equivalence
1009
29.3.2 Some Extensions of Timed Automata
1010
29.4 (Bi)simulation Checking
1012
29.4.1 (Bi)simulations for Timed Automata
1012
29.4.2 Checking (Bi)simulations
1013
29.5 Language-Theoretic Properties
1014
29.5.1 Language of a Timed Automaton
1014
29.5.2 Timed Automata with epsilon-Transitions
1014
29.5.3 Clock Constraints as Acceptance Conditions
1015
29.5.4 Intersection, Union, and Complement
1016
29.5.5 Language Emptiness, Inclusion
1017
29.6 Timed Temporal Logics
1020
29.6.1 Linear-Time Temporal Logics
1020
Continuous Semantics
1020
Pointwise Semantics
1021
29.6.2 Veri?cation of Linear-Time Temporal Logics
1021
29.6.3 Branching-Time Temporal Logics
1023
29.6.4 Veri?cation of Branching-Time Temporal Logics
1024
29.7 Symbolic Algorithms, Data Structures, Tools
1025
29.7.1 Zones and Operations
1025
29.7.2 Symbolic Datastructures
1026
29.7.3 Practical Ef?ciency
1028
29.7.4 Tools and Applications
1029
29.8 Weighted Timed Automata
1030
29.8.1 Cost-Optimal Schedules
1031
29.8.2 Weighted Temporal Logics
1033
29.8.3 Energy Constraints
1034
29.9 Timed Games
1036
29.10 Ongoing and Future Challenges
1039
References
1039
Chapter 30: Veri?cation of Hybrid Systems
1049
30.1 Introduction
1050
30.2 Basic De?nitions
1051
30.2.1 Predicates
1052
30.2.2 Hybrid Automata
1054
30.3 Decidability and Undecidability Results
1057
30.4 Set-Based Reachability Analysis
1060
30.4.1 Reachability Algorithm
1060
30.4.2 Piecewise Constant Dynamics
1062
30.4.3 Piecewise Af?ne Dynamics
1066
30.4.3.1 Successor Computations
1067
30.4.3.2 Set Representations
1072
30.4.3.3 Clustering
1076
30.4.4 Nonlinear Dynamics
1076
30.5 Abstraction-Based Veri?cation
1077
30.5.1 Discrete Abstractions
1078
30.5.2 Phase-Portrait Approximation
1080
30.5.3 Predicate Abstractions
1081
30.5.4 Abstraction Re?nement
1084
30.5.5 Approximate Bisimulations
1085
30.6 Logic-Based Veri?cation
1086
30.6.1 Polynomial Barrier Certi?cates
1089
30.6.2 Equational Certi?cates
1091
30.6.3 Differential Invariants and Logical Certi?cates
1092
30.7 Veri?cation Tools
1099
HSolver: Interval Constraint Propagation
1100
HyTech: The HYbrid TECHnology Tool
1100
KeYmaera: Logic and Differential Invariants for Compositional Veri?cation
1101
PHAVer: Polyhedral Hybrid Automaton Verifyer
1102
SpaceEx: State Space Explorer
1103
ToolboxLS: Level Set Methods
1103
References
1104
Chapter 31: Symbolic Model Checking in Non-Boolean Domains
1113
31.1 Introduction
1113
31.2 Transition Systems and Symbolic Veri?cation
1114
31.2.1 Systems: Transition Systems
1114
31.2.2 Properties and Algorithms: The µ-Calculus
1115
31.2.3 Symbolic Model Checking
1117
31.2.4 Examples of Properties and Their Veri?cation Algorithms
1118
31.2.5 Equivalence Relations and Termination
1120
31.3 Examples of Symbolic Veri?cation
1121
31.3.1 Program Veri?cation
1121
31.3.2 Antichain-Based Algorithms for Finite-State Automata
1123
31.3.3 Timed and Hybrid Systems
1126
31.3.4 Well-Structured Transition Systems
1130
31.4 Games and Symbolic Synthesis
1133
31.4.1 Deterministic Games
1133
31.4.2 The Boolean µ-Calculus on Games
1134
31.4.3 Linear-Time Properties
1135
31.4.4 From Veri?cation to Synthesis
1137
31.4.5 Examples of Synthesis
1138
31.5 Probabilistic Systems
1139
31.5.1 Probabilistic Games and Objectives
1140
31.5.2 The Quantitative µ-calculus
1141
31.6 Conclusion
1143
References
1145
Chapter 32: Process Algebra and Model Checking
1150
32.1 Introduction
1150
32.2 Foundations
1151
32.2.1 CCS: Process Algebra via Operational Semantics
1152
32.2.1.1 Syntax of CCS
1152
Actions in CCS
1152
CCS Operators
1153
32.2.1.2 The Operational Semantics of CCS
1154
32.2.1.3 CCS and Labeled Transition Systems
1155
32.2.1.4 Bisimulation
1156
32.2.1.5 A Logical Characterization of Bisimilarity
1158
Syntax of HML
1158
Semantics of HML
1159
Bisimulation vis-à-vis HML
1159
32.2.1.6 Observational Equivalence and Congruence for CCS
1160
32.2.1.7 Axiomatizations of Bisimilarity and Observational Congruence
1162
Inference Rules for Equational Reasoning
1162
Axiomatizing Bisimilarity
1163
Axiomatizing Observational Congruence
1164
Axiomatizing Full CCS
1164
32.2.2 CSP: Process Algebra via Denotational Semantics
1164
32.2.2.1 CSP Syntax
1165
Actions in CSP
1165
CSP Constructs
1166
32.2.2.2 Models for CSP Processes
1168
32.2.2.3 A Denotational Semantics for CSP
1171
32.2.2.4 Timed CSP
1173
32.2.3 ACP: Process Algebra via Equational Semantics
1173
32.2.3.1 BPA
1173
32.2.3.2 PA
1174
32.2.3.3 ACP
1175
32.3 Algorithms and Methodologies
1176
32.3.1 Bisimulation and Simulation
1176
32.3.2 Checking Re?nement over Behavioral Models
1178
32.3.3 Diagnostic Information (HML , FD)
1179
32.3.4 Compositional Veri?cation
1181
32.4 Tools
1182
32.4.1 FDR
1182
32.4.1.1 Using FDR
1183
32.4.2 The Concurrency Workbench
1184
32.4.3 XMC
1185
32.4.4 mCRL2
1185
32.5 Case Studies
1186
32.5.1 Distributed Leadership Election (FDR)
1186
32.5.2 Active-Structure Control System (CWB)
1189
32.5.3 GNU i-Protocol (XSB)
1190
32.6 Conclusions
1191
References
1192
Index
1197