O'Reilly logo

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

Communicating Embedded Systems: Software and Design

Communicating Embedded Systems: Software and Design

by Olivier H. Roux, Claude Jard
Publisher: John Wiley & Sons
Release Date: December 2009
ISBN: 9781118600092
View table of contents
Start reading

Book Description

The increased complexity of embedded systems coupled with quick design cycles to accommodate faster time-to-market requires increased system design productivity that involves both model-based design and tool-supported methodologies.

Formal methods are mathematically-based techniques and provide a clean framework in which to express requirements and models of the systems, taking into account discrete, stochastic and continuous (timed or hybrid) parameters with increasingly efficient tools.

This book deals with these formal methods applied to communicating embedded systems by presenting the related industrial challenges and the issues of modeling, model-checking, diagnosis and control synthesis, and by describing the main associated automated tools.

Table of Contents

  1. Cover
  2. Title Page
  3. Copyright
  4. Preface
  5. Chapter 1: Models for Real-Time Embedded Systems
    1. 1.1. Introduction
      1. 1.1.1. Model-checking and control problems
      2. 1.1.2. Timed models
    2. 1.2. Notations, languages and timed transition systems
    3. 1.3. Timed models
      1. 1.3.1. Timed Automata
      2. 1.3.2. Time Petri nets
        1. 1.3.2.1. T-time Petri nets
          1. 1.3.2.1.1. Definitions
          2. 1.3.2.1.2. Decidability of classical problems
        2. 1.3.2.2. Timed-arc petri nets
          1. 1.3.2.2.1. Decidability of classical problems
      3. 1.3.3. Compared expressiveness of several classes of timed models
        1. 1.3.3.1. Bisimulation and expressiveness of timed models
        2. 1.3.3.2. Compared expressiveness of different classes of TPN .
        3. 1.3.3.3. Compared expressiveness of TA, TPN, and TAPN
          1. 1.3.3.3.1. From TA/NTA to TPN
          2. 1.3.3.3.2. From TPN to TA/NTA
          3. 1.3.3.3.3. From TA/NTA to TAPN and backwards
          4. 1.3.3.3.4. From TPN to TAPN and Backwards
    4. 1.4. Models with stopwatches
      1. 1.4.1. Formal models for scheduling aspects
        1. 1.4.1.1. Automata and scheduling
        2. 1.4.1.2. Time Petri nets and scheduling
      2. 1.4.2. Stopwatch automata
      3. 1.4.3. Scheduling time Petri nets
      4. 1.4.4. Decidability results for stopwatch models
    5. 1.5. Conclusion
    6. 1.6. Bibliography
  6. Chapter 2: Timed Model-Checking
    1. 2.1. Introduction
    2. 2.2. Timed models
      1. 2.2.1. Timed transition system
      2. 2.2.2. Timed automata
      3. 2.2.3. Other models
    3. 2.3. Timed logics
      1. 2.3.1. Temporal logics CTL and LTL
      2. 2.3.2. Timed extensions
        1. 2.3.2.1. Timed CTL
        2. 2.3.2.2. Timed LTL
    4. 2.4. Timed model-checking
      1. 2.4.1. Model-checking LTL and CTL (untimed case)
      2. 2.4.2. Region automaton
      3. 2.4.3. Model-checking TCTL
      4. 2.4.4. Model-checking MTL
      5. 2.4.5. Efficient model-checking
      6. 2.4.6. Model-checking in practice
    5. 2.5. Conclusion
    6. 2.6. Bibliography
  7. Chapter 3: Control of Timed Systems
    1. 3.1. Introduction
      1. 3.1.1. Verification of timed systems
      2. 3.1.2. The controller synthesis problem
      3. 3.1.3. From control to game
      4. 3.1.4. Game objectives
      5. 3.1.5. Varieties of untimed games
    2. 3.2. Timed games
      1. 3.2.1. Timed game automata
      2. 3.2.2. Strategies and course of the game
        1. 3.2.2.1. The course of a timed game
        2. 3.2.2.2. Strategies
    3. 3.3. Computation of winning states and strategies
      1. 3.3.1. Controllable predecessors
      2. 3.3.2. Symbolic operators
      3. 3.3.3. Symbolic computation of winning states
      4. 3.3.4. Synthesis of winning strategies
    4. 3.4. Zeno strategies
    5. 3.5. Implementability
      1. 3.5.1. Hybrid automata
      2. 3.5.2. On the existence of non-implementable continuous controllers
      3. 3.5.3. Recent results and open problems
    6. 3.6. Specification of control objectives
    7. 3.7. Optimal control
      1. 3.7.1. TA with costs
      2. 3.7.2. Optimal cost in timed games
      3. 3.7.3. Computation of the optimal cost
      4. 3.7.4. Recent results and open problems
    8. 3.8. Efficient algorithms for controller synthesis
      1. 3.8.1. On-the-fly algorithms
      2. 3.8.2. Recent results and open problems
    9. 3.9. Partial observation
    10. 3.10. Changing game rules
    11. 3.11. Bibliography
  8. Chapter 4: Fault Diagnosis of Timed Systems
    1. 4.1. Introduction
    2. 4.2. Notations
      1. 4.2.1. Timed words and timed languages
      2. 4.2.2. Timed automata
      3. 4.2.3. Region graph of a TA
      4. 4.2.4. Product of TA
      5. 4.2.5. Timed automata with faults
    3. 4.3. Fault diagnosis problems
      1. 4.3.1. Diagnoser
      2. 4.3.2. The problems
      3. 4.3.3. Necessary and sufficient condition for diagnosability
    4. 4.4. Fault diagnosis for discrete event systems
      1. 4.4.1. Discrete event systems for fault diagnosis
      2. 4.4.2. Checking Δ-diagnosability and diagnosability
        1. 4.4.2.1. Checking Δ-diagnosability
        2. 4.4.2.2. Checking diagnosability
      3. 4.4.3. Computation of the maximum delay
      4. 4.4.4. Synthesis of a diagnoser
    5. 4.5. Fault diagnosis for timed systems
      1. 4.5.1. Checking Δ-diagnosability
      2. 4.5.2. Checking diagnosability
      3. 4.5.3. Computation of the maximal delay
      4. 4.5.4. Synthesis of a diagnoser
      5. 4.5.5. Fault diagnosis with deterministic timed automata
    6. 4.6. Other results and open problems
    7. 4.7. Bibliography
  9. Chapter 5: Quantitative Verification of Markov Chains
    1. 5.1. Introduction
    2. 5.2. Performance evaluation of Markov models
      1. 5.2.1. A stochastic model for discrete events systems
      2. 5.2.2. Discrete time Markov chains
      3. 5.2.3. Continuous time Markov chain
    3. 5.3. Verification of discrete time Markov chain
      1. 5.3.1. Temporal logics for Markov chains
      2. 5.3.2. Verification of PCTL formulae
      3. 5.3.3. Aggregation of Markov chains
      4. 5.3.4. Verification of PLTL formulae
      5. 5.3.5. Verification of PCTL*
    4. 5.4. Verification of continuous time Markov chain
      1. 5.4.1. Limitations of standard performance indices
      2. 5.4.2. A temporal logics for continuous time Markov chains
      3. 5.4.3. Verification algorithm
    5. 5.5. State of the art in the quantitative evaluation of Markov chains
    6. 5.6. Bibliography
  10. Chapter 6: Tools for Model-Checking Timed Systems
    1. 6.1. Introduction
    2. 6.2. Uppaal
      1. 6.2.1. Timed automata and symbolic exploration
        1. 6.2.1.1. Example
      2. 6.2.2. Queries
      3. 6.2.3. Architecture of the tool
      4. 6.2.4. Reachability pipeline
      5. 6.2.5. Liveness pipeline
      6. 6.2.6. Leadsto pipeline
      7. 6.2.7. Active clock reduction
      8. 6.2.8. Space reduction techniques
        1. 6.2.8.1. Avoid storing all states
        2. 6.2.8.2. Sharing data
        3. 6.2.8.3. Minimal graph
        4. 6.2.8.4. Symmetry reduction
      9. 6.2.9. Approximation techniques
        1. 6.2.9.1. Over-approximation: convex-hull
        2. 6.2.9.2. Under-approximation: bit-state hashing
      10. 6.2.10. Extensions
        1. 6.2.10.1. Robust reachability
        2. 6.2.10.2. Merging DBMs
        3. 6.2.10.3. Stopwatches
        4. 6.2.10.4. Supremum values
        5. 6.2.10.5. Other extensions
    3. 6.3. Uppaal-CORA
      1. 6.3.1. Priced timed automata
      2. 6.3.2. Example
    4. 6.4. Uppaal-TIGA
      1. 6.4.1. Timed game automata
      2. 6.4.2. Reachability pipeline
      3. 6.4.3. Time optimality
      4. 6.4.4. Cooperative strategies
      5. 6.4.5. Timed games with Büchi objectives
      6. 6.4.6. Timed games with partial observability
        1. 6.4.6.1. Algorithm
        2. 6.4.6.2. Implementation
      7. 6.4.7. Simulation checking
        1. 6.4.7.1. Algorithm
    5. 6.5. TAPAAL
      1. 6.5.1. Introduction
      2. 6.5.2. Definition of timed-arc Petri nets used in TAPAAL
      3. 6.5.3. TAPAAL logic
      4. 6.5.4. Tool details
    6. 6.6. Roméo: a tool for the analysis of timed extensions of Petri nets
      1. 6.6.1. Models
        1. 6.6.1.1. Time Petri nets
        2. 6.6.1.2. Petri Nets with stopwatches
        3. 6.6.1.3. Parametric Petri nets with stopwatches
      2. 6.6.2. Global architecture
      3. 6.6.3. Systems modeling
      4. 6.6.4. Verification of properties
        1. 6.6.4.1. On-line model checking
          1. 6.6.4.1.1. Model-checking of a subset of TCTL on Petri nets with stopwatches
          2. 6.6.4.1.2. Parametric model-checking of Petri nets with stopwatches
        2. 6.6.4.2. Off-line model checking
          1. 6.6.4.2.1. Verification based on observers
          2. 6.6.4.2.2. Verification based on translations into other models
      5. 6.6.5. Using Roméo in an example
    7. 6.7. Bibliography
  11. Chapter 7: Tools for the Analysis of Hybrid Models
    1. 7.1. Introduction
    2. 7.2. Hybrid automata and reachability
    3. 7.3. Linear hybrid automata
    4. 7.4. Piecewise affine hybrid systems
      1. 7.4.1. Time discretization
        1. 7.4.1.1. Autonomous dynamics
        2. 7.4.1.2. Dynamics with inputs
      2. 7.4.2. Scaling up reachability computations
        1. 7.4.2.1. Reachability using zonotopes
        2. 7.4.2.2. Efficient implementation for LTI systems
        3. 7.4.2.3. Dealing with the discrete transitions
    5. 7.5. Hybridization techniques for reachability computations
      1. 7.5.1. Approximation with linear hybrid automata
      2. 7.5.2. Hybridization of nonlinear continuous system
        1. 7.5.2.1. Properties of the approximate reachable set
        2. 7.5.2.2. Approximation by hybrid systems with piecewise affine dynamics
      3. 7.5.3. Hybridization and refinement
    6. 7.6. Bibliography
  12. List of Authors
  13. Index