Inverse Method

Parametric Verification of Real-time Unbedded Systems

Inbunden, Engelska, 2013

1 938 kr

Beställningsvara. Skickas inom 5-8 vardagar. Fri frakt över 249 kr.

Beskrivning

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.

Produktinformation

Utgivningsdatum:2013-01-18
Mått:160 x 241 x 20 mm
Vikt:439 g
Format:Inbunden
Språk:Engelska
Antal sidor:176
Förlag:ISTE Ltd and John Wiley & Sons Inc
ISBN:9781848214477

Utforska kategorier

Mer om författaren

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

Innehållsförteckning

PREFACE ixACKNOWLEDGMENTS xiINTRODUCTION xiiiI.1. Motivation xivI.1.1. An example of asynchronous circuit xivI.2. The good parameters problem xvI.3. Content and organization of the book xviI.3.1. Content xviI.3.2. Organization of the book xviiI.3.3. Acknowledgments xviiiCHAPTER 1. PARAMETRIC TIMED AUTOMATA 11.1. Constraints on clocks and parameters 11.1.1. Clocks 11.1.2. Parameters 21.1.3. Constraints 21.2. Labeled transition systems 41.3. Timed automata 41.3.1. Syntax 51.3.2. Semantics 71.4. Parametric timed automata 101.4.1. Syntax 111.4.2. Semantics 141.5. Related work 191.5.1. Representation of time 191.5.2. Timed automata 201.5.3. Time Petri nets 211.5.4. Hybrid systems 22CHAPTER 2. THE INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA 232.1. The inverse problem 242.1.1. A motivating example 242.1.2. The problem 262.2. The inverse method algorithm 272.2.1. Principle 272.2.2. A toy example 282.2.3. Remarks on the algorithm 282.2.4. Results 322.2.5. Discussion 402.3. Variants of the inverse method 402.3.1. Algorithm with state inclusion in the fixpoint 412.3.2. Algorithm with union of the constraints 422.3.3. Algorithm with simple return 442.3.4. Combination: inclusion in fixpoint and union 452.3.5. Combination: inclusion in fixpoint and direct return 462.3.6. Summary of the algorithms 462.4. Related work 492.4.1. History of the inverse method 492.4.2. Time-abstract bisimulation 502.4.3. Formal techniques of verification 502.4.4. Problems related to the inverse problem 512.4.5. Parameter synthesis for parametric timed automata 53CHAPTER 3. THE INVERSE METHOD IN PRACTICE: APPLICATION TO CASE STUDIES 553.1. IMITATOR 563.1.1. History 563.1.2. Architecture and features 563.2. Flip-flop 573.3. SR-Latch 583.3.1. Parameter synthesis 593.4. AND–OR 603.5. IEEE 1394 Root Contention Protocol 623.5.1. Description of the model 623.5.2. Synthesis of constraints 643.6. Bounded Retransmission Protocol 643.7. CSMA/CD protocol 653.8. The SPSMALL memory 673.8.1. Description 673.8.2. A short history 713.8.3. Manually abstracted model 723.8.4. Automatically generated model 753.9. Networked automation system 773.9.1. Description of the model 773.9.2. Definition of a zone of good behavior 783.9.3. Comparison with other methods 793.10. Tools related to IMITATOR 79CHAPTER 4. BEHAVIORAL CARTOGRAPHY OF TIMED AUTOMATA 814.1. The behavioral cartography algorithm 824.2. Properties 834.2.1. Acyclic parametric timed automata 834.2.2. General case 844.3. Case studies 844.3.1. Implementation 854.3.2. SR latch 864.3.3. Flip-flop 914.3.4. The root contention protocol 954.3.5. SPSMALL memory 954.4. Related work 101CHAPTER 5. PARAMETER SYNTHESIS FOR HYBRID AUTOMATA 1035.1. Hybrid automata with parameters 1055.1.1. Basic definitions 1055.1.2. Symbolic semantics of linear hybrid automata 1085.2. Algorithms for hybrid automata 1095.2.1. The inverse method for hybrid automata 1095.2.2. Behavioral cartography of hybrid automata 1115.2.3. Enhancement of the method for affine dynamics 1145.3. Implementation 1165.4. Discussion 1175.5. Related work 118CHAPTER 6. APPLICATION TO THE ROBUSTNESS ANALYSIS OF SCHEDULING PROBLEMS 1216.1. Preliminaries 1216.1.1. Scheduling problems 1216.1.2. Timed automata augmented with stopwatches 1226.2. Scheduling analysis using the inverse method 1236.2.1. Modeling schedulability with timed automata 1236.2.2. Robustness analysis using the inverse method 1246.2.3. Schedulability zone synthesis 1246.3. Application to scheduling problems 1266.3.1. Jobs with deadlines 1266.3.2. Schedulability zone synthesis 1266.3.3. Next generation spacecraft flight control system 1276.4. Discussion 1306.5. Related work 131CHAPTER 7. CONCLUSION AND PERSPECTIVES 1337.1. Trace-based inverse method and partial orders 1347.2. Preservation of temporal logics 1347.3. Application to other formalisms 135BIBLIOGRAPHY 137INDEX 149