The Inverse Method - Parametric Verification of Real-time Unbedded Systems

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:
 
1. Parametric Timed Automata.
2. The Inverse Method for Parametric Timed Automata.
3. The Inverse Method in Practice: Application to Case Studies.
4. Behavioral Cartography of Timed Automata.
5. Parameter Synthesis for Hybrid Automata.
6. Application to the Robustness Analysis of Scheduling Problems.
7. 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.

List 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 semanti

About the author

É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.

Summary

This practical guide arms scientists, researchers, and industrial engineers with state-of-the-art verification techniques for real time embedded systems based on the inverse method for parametric timed automata. The authors begin with an introduction to the inverse method, demonstrating how to use it to guarantee robustness in real-time systems.

Product details

• Authors: Etienne André, Etienne Andr?, Etienne Andre, Etienn André, Etienne André, Romain Soulat
• Publisher: Wiley & Sons
• Languages: English
• Product format: Hardback
• Released: 16.01.2014
• EAN: 9781848214477
• ISBN: 978-1-84821-447-7
• No. of pages: 168
• Dimensions: 162 mm x 231 mm x 32 mm
• Weight: 872 g
• Series: ISTE Focus; Focus Series; Focus Computer Engineering and; ISTE Focus; Focus Computer Engineering and
• Subjects: Natural sciences, medicine, IT, technology > Technology > Electronics, electrical engineering, communications engineering; COMPUTERS / Computer Science, Computers - General Information