Muutke küpsiste eelistusi

E-raamat: Communicating Embedded Systems for Computer Sciences: Software and Design [Wiley Online]

Edited by (ENS Cachan, France.), Edited by (Nantes University, France)
  • Formaat: 288 pages
  • Sari: ISTE
  • Ilmumisaeg: 06-Nov-2009
  • Kirjastus: ISTE Ltd and John Wiley & Sons Inc
  • ISBN-10: 1118558189
  • ISBN-13: 9781118558188
Teised raamatud teemal:
  • Wiley Online
  • Hind: 174,45 €*
  • * hind, mis tagab piiramatu üheaegsete kasutajate arvuga ligipääsu piiramatuks ajaks
Communicating Embedded Systems for Computer Sciences: Software and DesignSuurem pilt
  • Formaat: 288 pages
  • Sari: ISTE
  • Ilmumisaeg: 06-Nov-2009
  • Kirjastus: ISTE Ltd and John Wiley & Sons Inc
  • ISBN-10: 1118558189
  • ISBN-13: 9781118558188
Teised raamatud teemal:
Wiley Online e-raamatudRohkem infot Wiley Online kohta
Raamatu kodulehekülg: https://onlinelibrary.wiley.com/doi/book/10.1002/9781118558188
This work examines the use of mathematically based formal methods in embedded systems that are linked with other embedded systems, and embedded systems that are connected to other local or remote communication circuit components. It describes elements of current embedded system programs, reviews new research on models and their use, and describes software tools. Chapters cover models for real-time embedded systems, timed model-checking, control and fault diagnosis of timed systems, quantitative verification of Markov chains, tools for model-checking timed systems, and tools for the analysis of hybrid models. Jard is professor at ENS Cachan Campus of Ker-Lann. Roux is assistant professor at Nantes University. Annotation ©2010 Book News, Inc., Portland, OR (booknews.com)

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.

Preface xi
Claude Jard
Olivier H. Roux
Models for Real-Time Embedded Systems
1(38)
Didier Lime
Olivier H. Roux
Jiri Srba
Introduction
1(4)
Model-checking and control problems
2(1)
Timed models
3(2)
Notations, languages and timed transition systems
5(3)
Timed models
8(15)
Timed Automata
8(2)
Time Petri nets
10(2)
T-time Petri nets
12(3)
Timed-arc petri nets
15(4)
Compared expressiveness of several classes of timed models
19(1)
Bisimulation and expressiveness of timed models
19(1)
Compared expressiveness of different classes of TPN
20(1)
Compared expressiveness of TA, TPN, and TAPN
21(2)
Models with stopwatches
23(8)
Formal models for scheduling aspects
23(1)
Automata and scheduling
23(1)
Time Petri nets and scheduling
24(1)
Stopwatch automata
25(1)
Scheduling time Petri nets
26(5)
Decidability results for stopwatch models
31(1)
Conclusion
31(1)
Bibliography
31(8)
Timed Model-Checking
39(28)
Beatrice Berard
Introduction
39(1)
Timed models
40(6)
Timed transition system
40(1)
Timed automata
41(3)
Other models
44(2)
Timed logics
46(5)
Temporal logics CTL and LTL
46(2)
Timed extensions
48(1)
Timed CTL
48(2)
Timed LTL
50(1)
Timed model-checking
51(10)
Model-checking LTL and CTL (untimed case)
51(2)
Region automaton
53(3)
Model-checking TCTL
56(2)
Model-checking MTL
58(1)
Efficient model-checking
59(1)
Model-checking in practice
60(1)
Conclusion
61(1)
Bibliography
61(6)
Control of Timed Systems
67(40)
Franck Cassez
Nicolas Markey
Introduction
67(5)
Verification of timed systems
67(1)
The controller synthesis problem
68(1)
From control to game
69(1)
Game objectives
70(1)
Varieties of untimed games
71(1)
Timed games
72(4)
Timed game automata
72(1)
Strategies and course of the game
73(1)
The course of a timed game
73(1)
Strategies
74(2)
Computation of winning states and strategies
76(6)
Controllable predecessors
77(2)
Symbolic operators
79(1)
Symbolic computation of winning states
79(1)
Synthesis of winning strategies
80(2)
Zeno strategies
82(1)
Implementability
82(3)
Hybrid automata
83(1)
On the existence of non-implementable continuous controllers
84(1)
Recent results and open problems
85(1)
Specification of control objectives
85(2)
Optimal control
87(5)
TA with costs
87(2)
Optimal cost in timed games
89(1)
Computation of the optimal cost
90(2)
Recent results and open problems
92(1)
Efficient algorithms for controller synthesis
92(4)
On-the-fly algorithms
93(2)
Recent results and open problems
95(1)
Partial observation
96(1)
Changing game rules
97(1)
Bibliography
98(9)
Fault Diagnosis of Timed Systems
107(32)
Franck Cassez
Stavros Tripakis
Introduction
107(2)
Notations
109(4)
Timed words and timed languages
109(1)
Timed automata
110(1)
Region graph of a TA
111(1)
Product of TA
111(1)
Timed automata with faults
112(1)
Fault diagnosis problems
113(2)
Diagnoser
113(1)
The problems
114(1)
Necessary and sufficient condition for diagnosability
115(1)
Fault diagnosis for discrete event systems
115(7)
Discrete event systems for fault diagnosis
115(1)
Checking δ-diagnosability and diagnosability
116(1)
Checking δ-diagnosability
116(1)
Checking diagnosability
117(3)
Computation of the maximum delay
120(1)
Synthesis of a diagnoser
121(1)
Fault diagnosis for timed systems
122(14)
Checking δ-diagnosability
122(1)
Checking diagnosability
123(2)
Computation of the maximal delay
125(1)
Synthesis of a diagnoser
126(1)
Fault diagnosis with deterministic timed automata
127(9)
Other results and open problems
136(1)
Bibliography
136(3)
Quantitative Verification of Markov Chains
139(26)
Susanna Donatelli
Serge Haddad
Introduction
139(1)
Performance evaluation of Markov models
140(8)
A stochastic model for discrete events systems
140(3)
Discrete time Markov chains
143(3)
Continuous time Markov chain
146(2)
Verification of discrete time Markov chain
148(9)
Temporal logics for Markov chains
148(1)
Verification of PCTL formulae
149(2)
Aggregation of Markov chains
151(3)
Verification of PLTL formulae
154(3)
Verification of PCTL
157(1)
Verification of continuous time Markov chain
157(3)
Limitations of standard performance indices
157(1)
A temporal logics for continuous time Markov chains
158(1)
Verification algorithm
159(1)
State of the art in the quantitative evaluation of Markov chains
160(2)
Bibliography
162(3)
Tools for Model-Checking Timed Systems
165(62)
Alexandre David
Gerd Behrmann
Peter Bulychev
Joakim Byg
Thomas Chatin
Kim G. Larsen
Paul Pettersson
Jacob Illum Rasmussen
Jiri Srba
Wang Yi
Kenneth Y. Joergensen
Didier Lime
Morgan Magnin
Olivier H. Roux
Louis-Marie Traonouez
Introduction
165(1)
Uppaal
166(16)
Timed automata and symbolic exploration
166(3)
Example
169(1)
Queries
170(2)
Architecture of the tool
172(1)
Reachability pipeline
173(2)
Liveness pipeline
175(1)
Leadsto pipeline
176(1)
Active clock reduction
176(1)
Space reduction techniques
177(1)
Avoid storing all states
177(1)
Sharing data
178(1)
Minimal graph
178(1)
Symmetry reduction
179(1)
Approximation techniques
180(1)
Over-approximation: convex-hull
180(1)
Under-approximation: bit-state hashing
180(1)
Extensions
181(1)
Robust reachability
181(1)
Merging DBMs
181(1)
Stopwatches
181(1)
Supremum values
181(1)
Other extensions
181(1)
Uppaal-CORA
182(3)
Priced timed automata
182(2)
Example
184(1)
Uppaal-TIGA
185(14)
Timed game automata
185(2)
Reachability pipeline
187(1)
Time optimality
188(1)
Cooperative strategies
189(1)
Timed games with Buchi objectives
190(2)
Timed games with partial observability
192(2)
Algorithm
194(1)
Implementation
194(2)
Simulation checking
196(1)
Algorithm
197(2)
TAPAAL
199(6)
Introduction
199(1)
Definition of timed-arc Petri nets used in TAPAAL
200(3)
TAPAAL logic
203(1)
Tool details
204(1)
Romeo: a tool for the analysis of timed extensions of Petri nets
205(12)
Models
206(1)
Time Petri nets
206(2)
Petri Nets with stopwatches
208(2)
Parametric Petri nets with stopwatches
210(1)
Global architecture
210(1)
Systems modeling
211(1)
Verification of properties
211(1)
On-line model checking
211(2)
Off-line model checking
213(1)
Using Romeo in an example
214(3)
Bibliography
217(10)
Tools for the Analysis of Hybrid Models
227(26)
Thao Dang
Goran Frehse
Antoine Girard
Colas Le Guernic
Introduction
227(1)
Hybrid automata and reachability
228(4)
Linear hybrid automata
232(2)
Piecewise affine hybrid systems
234(7)
Time discretization
234(1)
Autonomous dynamics
234(2)
Dynamics with inputs
236(1)
Scaling up reachability computations
237(1)
Reachability using zonotopes
237(2)
Efficient implementation for LTI systems
239(1)
Dealing with the discrete transitions
239(2)
Hybridization techniques for reachability computations
241(8)
Approximation with linear hybrid automata
241(2)
Hybridization of nonlinear continuous system
243(1)
Properties of the approximate reachable set
244(1)
Approximation by hybrid systems with piecewise affine dynamics
245(1)
Hybridization and refinement
246(3)
Bibliography
249(4)
List of Authors 253(6)
Index 259
Claude Jard is full professor at ENS Cachan Campus of Ker-Lann. His research works relate to the formal analysis of asynchronous parallel systems.

Olivier H. Roux is an Assistant Professor at Nantes University and his research focusses on validation and verification of embedded systems, real-time and hybrid systems.
Püsilink: https://www.kriso.ee/db/9781118558188_pe.html
Märksõnad: