This book introduces state-of-the-art verification techniques for real-time embedded systems, based on the inverse method for parametric timed automata. It reviews popular formalisms for the specification and verification of timed concurrent systems and, in particular, timed automata as well as several extensions such as timed automata equipped with stopwatches, linear hybrid automata and affine hybrid automata.
The inverse method is introduced, and its benefits for guaranteeing robustness in real-time systems are shown. Then, it is shown how an iteration of the inverse method can solve the good parameters problem for parametric timed automata by computing a behavioral cartography of the system. Different extensions are proposed particularly for hybrid systems and applications to scheduling problems using timed automata with stopwatches. Various examples, both from the literature and industry, illustrate the techniques throughout the book.
Various parametric verifications are performed, in particular of abstractions of a memory circuit sold by the chipset manufacturer ST-Microelectronics, as well as of the prospective flight control system of the next generation of spacecraft designed by ASTRIUM Space Transportation.
Table of Contents:
PREFACE ix
ACKNOWLEDGMENTS xi
INTRODUCTION xiii
I.1. Motivation xiv
I.1.1. An example of asynchronous circuit xiv
I.2. The good parameters problem xv
I.3. Content and organization of the book xvi
I.3.1. Content xvi
I.3.2. Organization of the book xvii
I.3.3. Acknowledgments xviii
CHAPTER 1. PARAMETRIC TIMED AUTOMATA 1
1.1. Constraints on clocks and parameters 1
1.1.1. Clocks 1
1.1.2. Parameters 2
1.1.3. Constraints 2
1.2. Labeled transition systems 4
1.3. Timed automata 4
1.3.1. Syntax 5
1.3.2. Semantics 7
1.4. Parametric timed automata 10
1.4.1. Syntax 11
1.4.2. Semantics 14
1.5. Related work 19
1.5.1. Representation of time 19
1.5.2. Timed automata 20
1.5.3. Time Petri nets 21
1.5.4. Hybrid systems 22
CHAPTER 2. THE INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA 23
2.1. The inverse problem 24
2.1.1. A motivating example 24
2.1.2. The problem 26
2.2. The inverse method algorithm 27
2.2.1. Principle 27
2.2.2. A toy example 28
2.2.3. Remarks on the algorithm 28
2.2.4. Results 32
2.2.5. Discussion 40
2.3. Variants of the inverse method 40
2.3.1. Algorithm with state inclusion in the fixpoint 41
2.3.2. Algorithm with union of the constraints 42
2.3.3. Algorithm with simple return 44
2.3.4. Combination: inclusion in fixpoint and union 45
2.3.5. Combination: inclusion in fixpoint and direct return 46
2.3.6. Summary of the algorithms 46
2.4. Related work 49
2.4.1. History of the inverse method 49
2.4.2. Time-abstract bisimulation 50
2.4.3. Formal techniques of verification 50
2.4.4. Problems related to the inverse problem 51
2.4.5. Parameter synthesis for parametric timed automata 53
CHAPTER 3. THE INVERSE METHOD IN PRACTICE: APPLICATION TO CASE STUDIES 55
3.1. IMITATOR 56
3.1.1. History 56
3.1.2. Architecture and features 56
3.2. Flip-flop 57
3.3. SR-Latch 58
3.3.1. Parameter synthesis 59
3.4. AND–OR 60
3.5. IEEE 1394 Root Contention Protocol 62
3.5.1. Description of the model 62
3.5.2. Synthesis of constraints 64
3.6. Bounded Retransmission Protocol 64
3.7. CSMA/CD protocol 65
3.8. The SPSMALL memory 67
3.8.1. Description 67
3.8.2. A short history 71
3.8.3. Manually abstracted model 72
3.8.4. Automatically generated model 75
3.9. Networked automation system 77
3.9.1. Description of the model 77
3.9.2. Definition of a zone of good behavior 78
3.9.3. Comparison with other methods 79
3.10. Tools related to IMITATOR 79
CHAPTER 4. BEHAVIORAL CARTOGRAPHY OF TIMED AUTOMATA 81
4.1. The behavioral cartography algorithm 82
4.2. Properties 83
4.2.1. Acyclic parametric timed automata 83
4.2.2. General case 84
4.3. Case studies 84
4.3.1. Implementation 85
4.3.2. SR latch 86
4.3.3. Flip-flop 91
4.3.4. The root contention protocol 95
4.3.5. SPSMALL memory 95
4.4. Related work 101
CHAPTER 5. PARAMETER SYNTHESIS FOR HYBRID AUTOMATA 103
5.1. Hybrid automata with parameters 105
5.1.1. Basic definitions 105
5.1.2. Symbolic semantics of linear hybrid automata 108
5.2. Algorithms for hybrid automata 109
5.2.1. The inverse method for hybrid automata 109
5.2.2. Behavioral cartography of hybrid automata 111
5.2.3. Enhancement of the method for affine dynamics 114
5.3. Implementation 116
5.4. Discussion 117
5.5. Related work 118
CHAPTER 6. APPLICATION TO THE ROBUSTNESS ANALYSIS OF SCHEDULING PROBLEMS 121
6.1. Preliminaries 121
6.1.1. Scheduling problems 121
6.1.2. Timed automata augmented with stopwatches 122
6.2. Scheduling analysis using the inverse method 123
6.2.1. Modeling schedulability with timed automata 123
6.2.2. Robustness analysis using the inverse method 124
6.2.3. Schedulability zone synthesis 124
6.3. Application to scheduling problems 126
6.3.1. Jobs with deadlines 126
6.3.2. Schedulability zone synthesis 126
6.3.3. Next generation spacecraft flight control system 127
6.4. Discussion 130
6.5. Related work 131
CHAPTER 7. CONCLUSION AND PERSPECTIVES 133
7.1. Trace-based inverse method and partial orders 134
7.2. Preservation of temporal logics 134
7.3. Application to other formalisms 135
BIBLIOGRAPHY 137
INDEX 149
About the Author :
Étienne André is Associate Professor in the Laboratoire d'Informatique de Paris Nord, in the University of Paris 13 (Sorbonne Paris Cité) in France. His current research interests focus on the verification of real-time systems.
Romain Soulat is currently completing his PhD at the LSV laboratory at ENS-Cachan in France, focusing on the modeling and verification of hybrid temporal systems.
