Modeling and Verification of Real-time Systems

Stephan Merz is a researcher at INRIA Lorraine (Nancy, France). He is interested in formal methods for the analysis and construction of reliable software systems, in particular temporal logic, refinement, and the automated and interactive verification of distributed systems. Nicolas Navet is a researcher in Real-Time Systems at INRIA Lorraine (Nancy, France). His research interests include real-time scheduling, probalistic modeling and computational intelligence, with applications to automotive embedded systems and financial engineering.

• Preface 15Stephan MERZ and Nicolas NAVETChapter 1. Time Petri Nets – Analysis Methods and Verification with TINA 19Bernard BERTHOMIEU, Florent PERES and Francois VERNADAT1.1. Introduction 191.2. Time Petri nets 201.2.1. Definition 201.2.2. States and the state reachability relation 201.2.3. Illustration 221.2.4. Some general theorems 231.3. State class graphs preserving markings and LTL properties 241.3.1. State classes 241.3.2. Illustration 251.3.3. Checking the boundedness property on-the-fly 261.3.4. Variations 271.4. State class graphs preserving states and LTL properties 281.4.1. Clock domain 281.4.2. Construction of the SSCG 291.4.3. Variants 301.5. State class graphs preserving states and branching properties 321.6. Computing firing schedules 331.6.1. Schedule systems 331.6.2. Delays (relative dates) versus dates (absolute) 341.6.3. Illustration 351.7. An implementation: the Tina environment 351.8. The verification of SE−LTL formulae in Tina 371.8.1. The temporal logic SE−LTL 371.8.2. Preservation of LTL properties by tina constructions 391.8.3. selt: the SE−LTL checker of Tina 391.9. Some examples of use of selt 421.9.1. John and Fred 421.9.2. The alternating bit protocol 441.10. Conclusion 471.11. Bibliography 48Chapter 2. Validation of Reactive Systems by Means of Verification and Conformance Testing 51Camille CONSTANT, Thierry JERON, Herve MARCHAND and Vlad RUSU2.1. Introduction 512.2. The IOSTS model 542.2.1. Syntax of IOSTS 542.2.2. Semantics of IOSTS 562.3. Basic operations on IOSTS 572.3.1. Parallel product 572.3.2. Suspension 582.3.3. Deterministic IOSTS and determinization 602.4. Verification and conformance testing with IOSTS 602.4.1. Verification 602.4.2. Conformance testing 642.5. Test generation 642.6. Test selection 682.7. Conclusion and related work 702.8. Bibliography 73Chapter 3. An Introduction to Model Checking 77Stephan MERZ3.1. Introduction 773.2. Example: control of an elevator 783.3. Transition systems and invariant checking 793.3.1. Transition systems and their runs 813.3.2. Verification of invariants 823.4. Temporal logic 843.4.1. Linear-time temporal logic 843.4.2. Branching-time temporal logic 873.4.3. ω-automata 893.4.4. Automata and PTL 923.5. Model checking algorithms 943.5.1. Local PTL model checking 953.5.2. Global CTL model checking 973.5.3. Symbolic model checking algorithms 993.6. Some research topics 1033.7. Bibliography 105Chapter 4. Model Checking Timed Automata 111Patricia BOUYER and Francois LAROUSSINIE4.1. Introduction 1114.2. Timed automata 1124.2.1. Some notations 1124.2.2. Timed automata, syntax and semantics 1134.2.3. Parallel composition 1144.3. Decision procedure for checking reachability 1154.4. Other verification problems 1184.4.1. Timed languages 1184.4.2. Branching-time timed logics 1184.4.3. Linear-time timed logics 1204.4.4. Timed modal logics 1214.4.5. Testing automata 1214.4.6. Behavioral equivalences 1214.5. Some extensions of timed automata 1214.5.1. Diagonal clock constraints 1224.5.2. Additive clock constraints 1234.5.3. Internal actions 1244.5.4. Updates of clocks 1254.5.5. Linear hybrid automata 1264.6. Subclasses of timed automata 1274.6.1. Event-recording automata 1274.6.2. One-clock timed automata 1284.6.3. Discrete-time models 1294.7. Algorithms for timed verification 1304.7.1. A symbolic representation for timed automata: the zones 1304.7.2. Backward analysis in timed automata 1314.7.3. Forward analysis of timed automata 1324.7.4. A data structure for timed systems: DBMs 1334.8. The model-checking tool Uppaal 1344.9. Bibliography 135Chapter 5. Specification and Analysis of Asynchronous Systems using CADP 141Radu MATEESCU5.1. Introduction 1415.2. The CADP toolbox 1425.2.1. The LOTOS language 1435.2.2. Labeled transition systems 1435.2.3. Some verification tools 1445.3. Specification of a drilling unit 1475.3.1. Architecture 1505.3.2. Physical devices and local controllers 1525.3.3. Main controller – sequential version 1555.3.4. Main controller – parallel version 1575.3.5. Environment 1585.4. Analysis of the functioning of the drilling unit 1595.4.1. Equivalence checking 1595.4.2. Model checking 1615.5. Conclusion and future work 1645.6. Bibliography 166Chapter 6. Synchronous Program Verification with Lustre/Lesar 171Pascal RAYMOND6.1. Synchronous approach 1716.1.1. Reactive systems 1716.1.2. The synchronous approach 1726.1.3. Synchronous languages 1726.2. The Lustre language 1736.2.1. Principles 1736.2.2. Example: the beacon counter 1746.3. Program verification 1746.3.1. Notion of temporal property 1756.3.2. Safety and liveness 1756.3.3. Beacon counter properties 1756.3.4. State machine 1756.3.5. Explicit automata 1766.3.6. Principles of model checking 1766.3.7. Example of abstraction 1776.3.8. Conservative abstraction and safety 1786.4. Expressing properties 1786.4.1. Model checking: general scheme 1786.4.2. Model checking synchronous program 1796.4.3. Observers 1806.4.4. Examples 1806.4.5. Hypothesis 1806.4.6. Model checking of synchronous programs 1816.5. Algorithms 1826.5.1. Boolean automaton 1826.5.2. Explicit automaton 1826.5.3. The “pre ” and “post ” functions 1836.5.4. Outstanding states 1836.5.5. Principles of the exploration 1846.6. Enumerative algorithm 1846.7. Symbolic methods and binary decision diagrams 1856.7.1. Notations 1856.7.2. Handling predicates 1866.7.3. Representation of the predicates 1866.7.4. Typical interface of aBDD library 1886.7.5. Implementation of BDDs 1886.7.6. Operations on BDDs 1896.7.7. Notes on complexity 1916.7.8. Typed decision diagrams 1926.7.9. Care set and generalized cofactor 1946.8. Forward symbolic exploration 1956.8.1. General scheme 1966.8.2. Detailed implementation 1966.8.3. Symbolic image computing 1986.8.4. Optimized image computing 1986.9. Backward symbolic exploration 2016.9.1. General scheme 2016.9.2. Reverse image computing 2026.9.3. Comparing forward and backward methods 2036.10. Conclusion and related works 2036.11. Demonstrations 2046.12. Bibliography 205Chapter 7. Synchronous Functional Programming with Lucid Synchrone 207Paul CASPI, Gregoire HAMON and Marc POUZET7.1. Introduction 2077.1.1. Programming reactive systems 2077.1.2. Lucid Synchrone 2117.2. Lucid Synchrone 2137.2.1. An ML dataflow language 2137.2.2. Stream functions 2147.2.3. Multi-sampled systems 2167.2.4. Static values 2227.2.5. Higher-order features 2227.2.6. Datatypes and pattern matching 2247.2.7. A programming construct to share the memory 2257.2.8. Signals and signal patterns 2277.2.9. State machines and mixed designs 2297.2.10. Parametrized state machines 2337.2.11. Combining state machines and signals 2347.2.12. Recursion and non-real-time features 2367.2.13. Two classical examples 2367.3. Discussion 2407.3.1. Functional reactive programming and circuit description languages 2407.3.2. Lucid Synchrone as a prototyping language 2417.4. Conclusion 2427.5. Acknowledgment 2437.6. Bibliography 243Chapter 8. Verification of Real-Time Probabilistic Systems 249Marta KWIATKOWSKA, Gethin NORMAN, David PARKER and Jeremy SPROSTON8.1. Introduction 2498.2. Probabilistic timed automata 2508.2.1. Preliminaries 2508.2.2. Syntax of probabilistic timed automata 2528.2.3. Modeling with probabilistic timed automata 2548.2.4. Semantics of probabilistic timed automata 2548.2.5. Probabilistic reachability and invariance 2558.3. Model checking for probabilistic timed automata 2588.3.1. The region graph 2588.3.2. Forward symbolic approach 2618.3.3. Backward symbolic approach 2668.3.4. Digital clocks 2738.4. Case study: the IEEE FireWire root contention protocol 2778.4.1. Overview 2778.4.2. Probabilistic timed automata model 2788.4.3. Model checking statistics .2818.4.4. Performance analysis 2828.5. Conclusion 2858.6. Bibliography 285Chapter 9. Verification of Probabilistic Systems Methods and Tools 289Serge HADDAD and Patrice MOREAUX9.1. Introduction 2899.2. Performance evaluation of Markovian models 2909.2.1. A stochastic model of discrete event systems 2909.2.2. Discrete-time Markov chains 2929.2.3. Continuous-time Markov chains 2949.3. High level stochastic models 2979.3.1. Stochastic Petri nets with general distributions 2979.3.2. GLSPN with exponential distributions . 2999.3.3. Performance indices of SPN 3009.3.4. Overview of models and methods in performance evaluation 3009.3.5. The Great SPN tool 3019.4. Probabilistic verification of Markov chains 3039.4.1. Limits of standard performance indices 3039.4.2. A temporal logic for Markov chains 3039.4.3. Verification algorithms 3059.4.4. Overview of probabilistic verification of Markov chains 3069.4.5. The ETMCC tool 3079.5. Markov decision processes 3089.5.1. Presentation of Markov decision processes 3089.5.2. A temporal logic for Markov decision processes 3099.5.3. Verification algorithms 3099.5.4. Overview of verification of Markov decision processes 3139.5.5. The PRISM tool 3149.6. Bibliography 315Chapter 10. Modeling and Verification of Real-Time Systems using the IF Toolset 319Marius BOZGA, Susanne GRAF, Laurent MOUNIER and Iulian OBER10.1. Introduction 32010.2. Architecture 32210.3. The IF notation 32410.3.1. Functional features 32410.3.2. Non-functional features 32610.3.3. Expressing properties with observers 32810.4. The IF tools 32910.4.1. Core components 32910.4.2. Static analysis 33210.4.3. Validation 33310.4.4. Translating UML to IF 33410.5. An overview on uses of IF in case studies 33610.6. Case study: the Ariane 5 flight program 33710.6.1. Overview of the Ariane 5 flight program 33710.6.2. Verification of functional properties 33910.6.3. Verification of non-functional properties 34310.6.4. Modular verification and abstraction 34410.7. Conclusion 34510.8. Bibliography 347Chapter 11. Architecture Description Languages: An Introduction to the SAE AADL 353Anne-Marie DEPLANCHE and Sebastien FAUCOU11.1. Introduction 35311.2. Main characteristics of the architecture description languages 35611.3. ADLs and real-time systems 35711.3.1. Requirement analysis 35711.3.2. Architectural views 35911.4. Outline of related works 36011.5. The AADL language 36211.5.1. An overview of the AADL 36311.6. Case study 36511.6.1. Requirements 36511.6.2. Architecture design and analysis with AADL 36611.6.3. Designing for reuse: package and refinement 37711.7. Conclusion 38011.8. Bibliography 381List of Authors 385Index 389