André / Soulat The Inverse Method
1. Auflage 2013
ISBN: 978-1-118-56940-5
Verlag: John Wiley & Sons
Format: PDF
Kopierschutz: Adobe DRM (»Systemvoraussetzungen)
Parametric Verification of Real-time Unbedded Systems
E-Book, Englisch, 176 Seiten, E-Book
ISBN: 978-1-118-56940-5
Verlag: John Wiley & Sons
Format: PDF
Kopierschutz: Adobe DRM (»Systemvoraussetzungen)
This book introduces state-of-the-art verification techniquesfor real-time embedded systems, based on the inverse method forparametric timed automata. It reviews popular formalisms for thespecification and verification of timed concurrent systems and, inparticular, timed automata as well as several extensions such astimed automata equipped with stopwatches, linear hybrid automataand affine hybrid automata.
The inverse method is introduced, and its benefits for guaranteeingrobustness in real-time systems are shown. Then, it is shown how aniteration of the inverse method can solve the good parametersproblem for parametric timed automata by computing a behavioralcartography of the system. Different extensions are proposedparticularly for hybrid systems and applications to schedulingproblems using timed automata with stopwatches. Various examples,both from the literature and industry, illustrate the techniquesthroughout the book.
Various parametric verifications are performed, in particular ofabstractions of a memory circuit sold by the chipset manufacturerST-Microelectronics, as well as of the prospective flight controlsystem of the next generation of spacecraft designed by ASTRIUMSpace Transportation.
Contents:
1. Parametric Timed Automata.
2. The Inverse Method for Parametric Timed Automata.
3. The Inverse Method in Practice: Application to CaseStudies.
4. Behavioral Cartography of Timed Automata.
5. Parameter Synthesis for Hybrid Automata.
6. Application to the Robustness Analysis of SchedulingProblems.
7. Conclusion and Perspectives.
About the Authors
Étienne André is Associate Professor in theLaboratoire d'Informatique de Paris Nord, in the Universityof Paris 13 (Sorbonne Paris Cité) in France. His currentresearch interests focus on the verification of real-timesystems.
Romain Soulat is currently completing his PhD at the LSV laboratoryat ENS-Cachan in France, focusing on the modeling and verificationof hybrid temporal systems.
