Communicating Embedded Systems

Software and Design

Inbunden, Engelska, 2009

AvClaude Jard,Olivier H. Roux,France.) Jard, Claude (ENS Cachan,France) Roux, Olivier H. (Nantes University,Olivier H Roux

2 369 kr

Tillfälligt slut

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.

Produktinformation

Utgivningsdatum2009-11-06
Mått158 x 236 x 23 mm
Vikt522 g
FormatInbunden
SpråkEngelska
Antal sidor288
FörlagISTE Ltd and John Wiley & Sons Inc
ISBN9781848211438

Tillhör följande kategorier

Elektronik och kommunikationer inom Naturvetenskap och teknik

Preface xiClaude JARD and Olivier H. ROUXChapter 1. Models for Real-Time Embedded Systems 1Didier LIME, Olivier H. ROUX and Ji¡ri SRBA1.1. Introduction 11.2. Notations, languages and timed transition systems 51.3. Timed models 81.4. Models with stopwatches 231.5. Conclusion 311.6. Bibliography 31Chapter 2. Timed Model-Checking 39Beatrice BERARD2.1. Introduction 392.2. Timed models 402.3. Timed logics 462.4. Timed model-checking 512.5. Conclusion 612.6. Bibliography 61Chapter 3. Control of Timed Systems 67Franck CASSEZ and Nicolas MARKEY3.1. Introduction 673.2. Timed games 723.3. Computation of winning states and strategies 763.4. Zeno strategies 823.5. Implementability 823.6. Specification of control objectives 853.7. Optimal control 873.8. Efficient algorithms for controller synthesis 923.9. Partial observation 963.10. Changing game rules 973.11. Bibliography 98Chapter 4. Fault Diagnosis of Timed Systems 107Franck CASSEZ and Stavros TRIPAKIS4.1. Introduction 1074.2. Notations 1094.3. Fault diagnosis problems 1134.4. Fault diagnosis for discrete event systems 1154.5. Fault diagnosis for timed systems 1224.6. Other results and open problems 1364.7. Bibliography 136Chapter 5. Quantitative Verification of Markov Chains 139Susanna DONATELLI and Serge HADDAD5.1. Introduction 1395.2. Performance evaluation of Markov models 1405.3. Verification of discrete time Markov chain 1485.4. Verification of continuous time Markov chain 1575.5. State of the art in the quantitative evaluation of Markov chains 1605.6. Bibliography 162Chapter 6. Tools for Model-Checking Timed Systems 165Alexandre DAVID, Gerd BEHRMANN, Peter BULYCHEV, Joakim BYG, Thomas CHATAIN, Kim G. LARSEN, Paul PETTERSSON, Jacob Illum RASMUSSEN, Ji¡ri SRBA,Wang YI, Kenneth Y. JOERGENSEN, Didier LIME,MorganMAGNIN, Olivier H. ROUX and Louis-Marie TRAONOUEZ6.1. Introduction 1656.2. UPPAAL 1666.3. UPPAAL-CORA 1826.4. UPPAAL-TIGA 1856.5. TAPAAL 1996.6. ROMEO: a tool for the analysis of timed extensions of Petri nets 2056.7. Bibliography 217Chapter 7. Tools for the Analysis of Hybrid Models 227Thao DANG, Goran FREHSE, Antoine GIRARD and Colas LE GUERNIC7.1. Introduction 2277.2. Hybrid automata and reachability 2287.3. Linear hybrid automata 2327.4. Piecewise affine hybrid systems 2347.5. Hybridization techniques for reachability computations 2417.6. Bibliography 249List of Authors 253Index 259