book

Communicating Embedded Systems: Software and Design

by Claude Jard, Olivier H. Roux

December 2009

Intermediate to advanced

288 pages

7h 11m

English

Wiley

Read now

Unlock full access

1.1. Introduction1.1.1. Model-checking and control problems1.1.2. Timed models1.2. Notations, languages and timed transition systems1.3. Timed models1.3.1. Timed Automata1.3.2. Time Petri nets1.3.2.1. T-time Petri nets1.3.2.1.1. Definitions1.3.2.1.2. Decidability of classical problems1.3.2.2. Timed-arc petri nets1.3.2.2.1. Decidability of classical problems1.3.3. Compared expressiveness of several classes of timed models1.3.3.1. Bisimulation and expressiveness of timed models1.3.3.2. Compared expressiveness of different classes of TPN .1.3.3.3. Compared expressiveness of TA, TPN, and TAPN1.3.3.3.1. From TA/NTA to TPN1.3.3.3.2. From TPN to TA/NTA1.3.3.3.3. From TA/NTA to TAPN and backwards1.3.3.3.4. From TPN to TAPN and Backwards1.4. Models with stopwatches1.4.1. Formal models for scheduling aspects1.4.1.1. Automata and scheduling1.4.1.2. Time Petri nets and scheduling1.4.2. Stopwatch automata1.4.3. Scheduling time Petri nets1.4.4. Decidability results for stopwatch models1.5. Conclusion1.6. Bibliography
2.1. Introduction2.2. Timed models2.2.1. Timed transition system2.2.2. Timed automata2.2.3. Other models2.3. Timed logics2.3.1. Temporal logics CTL and LTL2.3.2. Timed extensions2.3.2.1. Timed CTL2.3.2.2. Timed LTL2.4. Timed model-checking2.4.1. Model-checking LTL and CTL (untimed case)2.4.2. Region automaton2.4.3. Model-checking TCTL2.4.4. Model-checking MTL2.4.5. Efficient model-checking2.4.6. Model-checking in practice2.5. Conclusion2.6. Bibliography
3.1. Introduction3.1.1. Verification of timed systems3.1.2. The controller synthesis problem3.1.3. From control to game3.1.4. Game objectives3.1.5. Varieties of untimed games3.2. Timed games3.2.1. Timed game automata3.2.2. Strategies and course of the game3.2.2.1. The course of a timed game3.2.2.2. Strategies3.3. Computation of winning states and strategies3.3.1. Controllable predecessors3.3.2. Symbolic operators3.3.3. Symbolic computation of winning states3.3.4. Synthesis of winning strategies3.4. Zeno strategies3.5. Implementability3.5.1. Hybrid automata3.5.2. On the existence of non-implementable continuous controllers3.5.3. Recent results and open problems3.6. Specification of control objectives3.7. Optimal control3.7.1. TA with costs3.7.2. Optimal cost in timed games3.7.3. Computation of the optimal cost3.7.4. Recent results and open problems3.8. Efficient algorithms for controller synthesis3.8.1. On-the-fly algorithms3.8.2. Recent results and open problems3.9. Partial observation3.10. Changing game rules3.11. Bibliography
4.1. Introduction4.2. Notations4.2.1. Timed words and timed languages4.2.2. Timed automata4.2.3. Region graph of a TA4.2.4. Product of TA4.2.5. Timed automata with faults4.3. Fault diagnosis problems4.3.1. Diagnoser4.3.2. The problems4.3.3. Necessary and sufficient condition for diagnosability4.4. Fault diagnosis for discrete event systems4.4.1. Discrete event systems for fault diagnosis4.4.2. Checking Δ-diagnosability and diagnosability4.4.2.1. Checking Δ-diagnosability4.4.2.2. Checking diagnosability4.4.3. Computation of the maximum delay4.4.4. Synthesis of a diagnoser4.5. Fault diagnosis for timed systems4.5.1. Checking Δ-diagnosability4.5.2. Checking diagnosability4.5.3. Computation of the maximal delay4.5.4. Synthesis of a diagnoser4.5.5. Fault diagnosis with deterministic timed automata4.6. Other results and open problems4.7. Bibliography
5.1. Introduction5.2. Performance evaluation of Markov models5.2.1. A stochastic model for discrete events systems5.2.2. Discrete time Markov chains5.2.3. Continuous time Markov chain5.3. Verification of discrete time Markov chain5.3.1. Temporal logics for Markov chains5.3.2. Verification of PCTL formulae5.3.3. Aggregation of Markov chains5.3.4. Verification of PLTL formulae5.3.5. Verification of PCTL*5.4. Verification of continuous time Markov chain5.4.1. Limitations of standard performance indices5.4.2. A temporal logics for continuous time Markov chains5.4.3. Verification algorithm5.5. State of the art in the quantitative evaluation of Markov chains5.6. Bibliography
6.1. Introduction6.2. Uppaal6.2.1. Timed automata and symbolic exploration6.2.1.1. Example6.2.2. Queries6.2.3. Architecture of the tool6.2.4. Reachability pipeline6.2.5. Liveness pipeline6.2.6. Leadsto pipeline6.2.7. Active clock reduction6.2.8. Space reduction techniques6.2.8.1. Avoid storing all states6.2.8.2. Sharing data6.2.8.3. Minimal graph6.2.8.4. Symmetry reduction6.2.9. Approximation techniques6.2.9.1. Over-approximation: convex-hull6.2.9.2. Under-approximation: bit-state hashing6.2.10. Extensions6.2.10.1. Robust reachability6.2.10.2. Merging DBMs6.2.10.3. Stopwatches6.2.10.4. Supremum values6.2.10.5. Other extensions6.3. Uppaal-CORA6.3.1. Priced timed automata6.3.2. Example6.4. Uppaal-TIGA6.4.1. Timed game automata6.4.2. Reachability pipeline6.4.3. Time optimality6.4.4. Cooperative strategies6.4.5. Timed games with Büchi objectives6.4.6. Timed games with partial observability6.4.6.1. Algorithm6.4.6.2. Implementation6.4.7. Simulation checking6.4.7.1. Algorithm6.5. TAPAAL6.5.1. Introduction6.5.2. Definition of timed-arc Petri nets used in TAPAAL6.5.3. TAPAAL logic6.5.4. Tool details6.6. Roméo: a tool for the analysis of timed extensions of Petri nets6.6.1. Models6.6.1.1. Time Petri nets6.6.1.2. Petri Nets with stopwatches6.6.1.3. Parametric Petri nets with stopwatches6.6.2. Global architecture6.6.3. Systems modeling6.6.4. Verification of properties6.6.4.1. On-line model checking6.6.4.1.1. Model-checking of a subset of TCTL on Petri nets with stopwatches6.6.4.1.2. Parametric model-checking of Petri nets with stopwatches6.6.4.2. Off-line model checking6.6.4.2.1. Verification based on observers6.6.4.2.2. Verification based on translations into other models6.6.5. Using Roméo in an example6.7. Bibliography

7.1. Introduction7.2. Hybrid automata and reachability7.3. Linear hybrid automata7.4. Piecewise affine hybrid systems7.4.1. Time discretization7.4.1.1. Autonomous dynamics7.4.1.2. Dynamics with inputs7.4.2. Scaling up reachability computations7.4.2.1. Reachability using zonotopes7.4.2.2. Efficient implementation for LTI systems7.4.2.3. Dealing with the discrete transitions7.5. Hybridization techniques for reachability computations7.5.1. Approximation with linear hybrid automata7.5.2. Hybridization of nonlinear continuous system7.5.2.1. Properties of the approximate reachable set7.5.2.2. Approximation by hybrid systems with piecewise affine dynamics7.5.3. Hybridization and refinement7.6. Bibliography

Content preview from Communicating Embedded Systems: Software and Design

Chapter 2 Timed Model-Checking ¹

2.1. Introduction

Reactive systems are those which handle interactions with the environment. They are frequently used in the area of transportation, communication protocols, or medical instrumentation, and often contain critical parts, where software errors can have heavy consequences. Many examples can be found in the PhD thesis of E. Fleury [FLE 02]. Even if there is a large agreement about the need for correctness of such systems, frequent accidents show that a formal verification step cannot be avoided.

Test generation is certainly the most commonly used technique. It consists of feeding input scenarios to a system and observing the output. The problem is then to guarantee a sufficient coverage of the behavior of the system, which is a difficult task. Other methods like theorem proving or model-checking ensure the completeness of the verification, but they suffer from the so-called “combinatorial explosion problem”, which sets an intrinsic limit on the systems size.

Model-checking (see [CLA 08], [BAI 99] or [SCH 01] for overviews) answers to the following question: given a system and a property; does the property hold in the system? The first step consists of building formal models S and P, respectively, for the system and the property, and subsequently applying a suitable algorithm that automatically solves the problem: does S satisfy P, denoted by ? The formalisms used for the system and the property should be the most expressive, whereas ...