CHF72.00
Download est disponible immédiatement
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.
Contents:
Parametric Timed Automata.
The Inverse Method for Parametric Timed Automata.
The Inverse Method in Practice: Application to Case
Studies.
Behavioral Cartography of Timed Automata.
Parameter Synthesis for Hybrid Automata.
Application to the Robustness Analysis of Scheduling
Problems.
Conclusion and Perspectives.
About the Authors
É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.
Auteur
Étienne André is Senior lecturer, Informatics Laboratory, Galilee Institute at University of Paris-Nord, Villetaneuse, France / Romain Soulat is Phd at LSV, CNRS & ENS de Cachan, France.
Résumé
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.
Contents:
About the Authors
É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.
Contenu
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. ANDOR 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...