LEADER 05887nam 2200769 a 450 001 9910820091003321 005 20230124183943.0 010 $a1-118-55818-9 010 $a1-118-60009-6 010 $a1-118-60012-6 010 $a1-299-18745-5 035 $a(CKB)2550000001005882 035 $a(EBL)1124321 035 $a(SSID)ssj0000832934 035 $a(PQKBManifestationID)11465909 035 $a(PQKBTitleCode)TC0000832934 035 $a(PQKBWorkID)10918982 035 $a(PQKB)10810509 035 $a(Au-PeEL)EBL1124321 035 $a(CaPaEBR)ebr10658441 035 $a(CaONFJC)MIL449995 035 $a(CaSebORM)9781118600092 035 $a(MiAaPQ)EBC1124321 035 $a(OCoLC)828298965 035 $a(OCoLC)857718082 035 $a(OCoLC)ocn857718082 035 $a(EXLCZ)992550000001005882 100 $a20090709d2010 uy 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 10$aCommunicating embedded systems $esoftware and design : formal methods /$fedited by Claude Jard, Olivier H. Roux 205 $a1st edition 210 $aLondon $cISTE ;$aHoboken, N.J. $cWiley$d2010 215 $a1 online resource (275 p.) 225 1 $aISTE 300 $aDescription based upon print version of record. 311 $a1-84821-143-0 320 $aIncludes bibliographical references and index. 327 $aCover; 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 327 $a1.3.3.3. Compared expressiveness of TA, TPN, and TAPN1.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 327 $a2.3.2.2. Timed LTL2.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 327 $a3.2.2.1. The course of a timed game3.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 327 $a3.7.4. Recent results and open problems3.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 327 $a4.4. Fault diagnosis for discrete event systems 330 $aThe 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 410 0$aISTE 606 $aEmbedded computer systems$xProgramming 606 $aEmbedded computer systems$xDesign and construction 606 $aComputer software$xDevelopment 606 $aFormal methods (Computer science) 615 0$aEmbedded computer systems$xProgramming. 615 0$aEmbedded computer systems$xDesign and construction. 615 0$aComputer software$xDevelopment. 615 0$aFormal methods (Computer science) 676 $a621.39/2 701 $aJard$b Claude$01641049 701 $aRoux$b Olivier H$01641050 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910820091003321 996 $aCommunicating embedded systems$93984916 997 $aUNINA