Cover -- Communicating Embedded Systems -- Title Page -- Copyright Page -- Table of Contents -- Preface -- Chapter 1. Models for Real-Time Embedded Systems -- 1.1. Introduction -- 1.1.1. Model-checking and control problems -- 1.1.2. Timed models -- 1.2. Notations, languages and timed transition systems -- 1.3. Timed models -- 1.3.1. Timed Automata -- 1.3.2. Time Petri nets -- 1.3.2.1. T-time Petri nets -- 1.3.2.2. Timed-arc petri nets -- 1.3.3. Compared expressiveness of several classes of timed models -- 1.3.3.1. Bisimulation and expressiveness of timed models -- 1.3.3.2. Compared expressiveness of different classes of TPN -- 1.3.3.3. Compared expressiveness of TA, TPN, and TAPN -- 1.4. Models with stopwatches -- 1.4.1. Formal models for scheduling aspects -- 1.4.1.1. Automata and scheduling -- 1.4.1.2. Time Petri nets and scheduling -- 1.4.2. Stopwatch automata -- 1.4.3. Scheduling time Petri nets -- 1.4.4. Decidability results for stopwatch models -- 1.5. Conclusion -- 1.6. Bibliography -- Chapter 2. Timed Model-Checking -- 2.1. Introduction -- 2.2. Timed models -- 2.2.1. Timed transition system -- 2.2.2. Timed automata -- 2.2.3. Other models -- 2.3. Timed logics -- 2.3.1. Temporal logics CTL and LTL -- 2.3.2. Timed extensions -- 2.3.2.1. Timed CTL -- 2.3.2.2. Timed LTL -- 2.4. Timed model-checking -- 2.4.1. Model-checking LTL and CTL (untimed case) -- 2.4.2. Region automaton -- 2.4.3. Model-checking TCTL -- 2.4.4. Model-checking MTL -- 2.4.5. Efficient model-checking -- 2.4.6. Model-checking in practice -- 2.5. Conclusion -- 2.6. Bibliography -- Chapter 3. Control of Timed Systems -- 3.1. Introduction -- 3.1.1. Verification of timed systems -- 3.1.2. The controller synthesis problem -- 3.1.3. From control to game -- 3.1.4. Game objectives -- 3.1.5. Varieties of untimed games -- 3.2. Timed games.

3.2.1. Timed game automata -- 3.2.2. Strategies and course of the game -- 3.2.2.1. The course of a timed game -- 3.2.2.2. Strategies -- 3.3. Computation of winning states and strategies -- 3.3.1. Controllable predecessors -- 3.3.2. Symbolic operators -- 3.3.3. Symbolic computation of winning states -- 3.3.4. Synthesis of winning strategies -- 3.4. Zeno strategies -- 3.5. Implementability -- 3.5.1. Hybrid automata -- 3.5.2. On the existence of non-implementable continuous controllers -- 3.5.3. Recent results and open problems -- 3.6. Specification of control objectives -- 3.7. Optimal control -- 3.7.1. TA with costs -- 3.7.2. Optimal cost in timed games -- 3.7.3. Computation of the optimal cost -- 3.7.4. Recent results and open problems -- 3.8. Efficient algorithms for controller synthesis -- 3.8.1. On-the-fly algorithms -- 3.8.2. Recent results and open problems -- 3.9. Partial observation -- 3.10. Changing game rules… -- 3.11. Bibliography -- Chapter 4. Fault Diagnosis of Timed Systems -- 4.1. Introduction -- 4.2. Notations -- 4.2.1. Timed words and timed languages -- 4.2.2. Timed automata -- 4.2.3. Region graph of a TA -- 4.2.4. Product of TA -- 4.2.5. Timed automata with faults -- 4.3. Fault diagnosis problems -- 4.3.1. Diagnoser -- 4.3.2. The problems -- 4.3.3. Necessary and sufficient condition for diagnosability -- 4.4. Fault diagnosis for discrete event systems -- 4.4.1. Discrete event systems for fault diagnosis -- 4.4.2. Checking Δ-diagnosability and diagnosability -- 4.4.2.1. Checking Δ-diagnosability -- 4.4.2.2. Checking diagnosability -- 4.4.3. Computation of the maximum delay -- 4.4.4. Synthesis of a diagnoser -- 4.5. Fault diagnosis for timed systems -- 4.5.1. Checking Δ-diagnosability -- 4.5.2. Checking diagnosability -- 4.5.3. Computation of the maximal delay -- 4.5.4. Synthesis of a diagnoser.

4.5.5. Fault diagnosis with deterministic timed automata -- 4.6. Other results and open problems -- 4.7. Bibliography -- Chapter 5. Quantitative Verification of Markov Chains -- 5.1. Introduction -- 5.2. Performance evaluation of Markov models -- 5.2.1. A stochastic model for discrete events systems -- 5.2.2. Discrete time Markov chains -- 5.2.3. Continuous time Markov chain -- 5.3. Verification of discrete time Markov chain -- 5.3.1. Temporal logics for Markov chains -- 5.3.2. Verification of PCTL formulae -- 5.3.3. Aggregation of Markov chains -- 5.3.4. Verification of PLTL formulae -- 5.3.5. Verification of PCTL* -- 5.4. Verification of continuous time Markov chain -- 5.4.1. Limitations of standard performance indices -- 5.4.2. A temporal logics for continuous time Markov chains -- 5.4.3. Verification algorithm -- 5.5. State of the art in the quantitative evaluation of Markov chains -- 5.6. Bibliography -- Chapter 6. Tools for Model-Checking Timed Systems -- 6.1. Introduction -- 6.2. UPPAAL -- 6.2.1. Timed automata and symbolic exploration -- 6.2.1.1. Example -- 6.2.2. Queries -- 6.2.3. Architecture of the tool -- 6.2.4. Reachability pipeline -- 6.2.5. Liveness pipeline -- 6.2.6. Leadsto pipeline -- 6.2.7. Active clock reduction -- 6.2.8. Space reduction techniques -- 6.2.8.1. Avoid storing all states -- 6.2.8.2. Sharing data -- 6.2.8.3. Minimal graph -- 6.2.8.4. Symmetry reduction -- 6.2.9. Approximation techniques -- 6.2.9.1. Over-approximation: convex-hull -- 6.2.9.2. Under-approximation: bit-state hashing -- 6.2.10. Extensions -- 6.2.10.1. Robust reachability -- 6.2.10.2. Merging DBMs -- 6.2.10.3. Stopwatches -- 6.2.10.4. Supremum values -- 6.2.10.5. Other extensions -- 6.3. UPPAAL-CORA -- 6.3.1. Priced timed automata -- 6.3.2. Example -- 6.4. UPPAAL-TIGA -- 6.4.1. Timed game automata.

6.4.2. Reachability pipeline -- 6.4.3. Time optimality -- 6.4.4. Cooperative strategies -- 6.4.5. Timed games with Büchi objectives -- 6.4.6. Timed games with partial observability -- 6.4.6.1. Algorithm -- 6.4.6.2. Implementation -- 6.4.7. Simulation checking -- 6.4.7.1. Algorithm -- 6.5. TAPAAL -- 6.5.1. Introduction -- 6.5.2. Definition of timed-arc Petri nets used in TAPAAL -- 6.5.3. TAPAAL logic -- 6.5.4. Tool details -- 6.6. ROMÉO: a tool for the analysis of timed extensions of Petri nets -- 6.6.1. Models -- 6.6.1.1. Time Petri nets -- 6.6.1.2. Petri Nets with stopwatches -- 6.6.1.3. Parametric Petri nets with stopwatches -- 6.6.2. Global architecture -- 6.6.3. Systems modeling -- 6.6.4. Verification of properties -- 6.6.4.1. On-line model checking -- 6.6.4.2. Off-line model checking -- 6.6.5. Using ROMÉO in an example -- 6.7. Bibliography -- Chapter 7. Tools for the Analysis of Hybrid Models -- 7.1. Introduction -- 7.2. Hybrid automata and reachability -- 7.3. Linear hybrid automata -- 7.4. Piecewise affine hybrid systems -- 7.4.1. Time discretization -- 7.4.1.1. Autonomous dynamics -- 7.4.1.2. Dynamics with inputs -- 7.4.2. Scaling up reachability computations -- 7.4.2.1. Reachability using zonotopes -- 7.4.2.2. Efficient implementation for LTI systems -- 7.4.2.3. Dealing with the discrete transitions -- 7.5. Hybridization techniques for reachability computations -- 7.5.1. Approximation with linear hybrid automata -- 7.5.2. Hybridization of nonlinear continuous system -- 7.5.2.1. Properties of the approximate reachable set -- 7.5.2.2. Approximation by hybrid systems with piecewise affine dynamics -- 7.5.3. Hybridization and refinement -- 7.6. Bibliography -- List of Authors -- Index.