Communicating Embedded Systems for Computer Sciences

<p>Preface xi<br /> Claude JARD and Olivier H. ROUX</p>
<p>Chapter 1. Models for Real–Time Embedded Systems 1<br /> Didier LIME, Olivier H. ROUX and Ji&iexcl;ri SRBA</p>
<p>1.1. Introduction 1</p>
<p>1.2. Notations, languages and timed transition systems 5</p>
<p>1.3. Timed models 8</p>
<p>1.4. Models with stopwatches 23</p>
<p>1.5. Conclusion 31</p>
<p>1.6. Bibliography 31</p>
<p>Chapter 2. Timed Model–Checking 39<br /> Beatrice BERARD</p>
<p>2.1. Introduction 39</p>
<p>2.2. Timed models 40</p>
<p>2.3. Timed logics 46</p>
<p>2.4. Timed model–checking 51</p>
<p>2.5. Conclusion 61</p>
<p>2.6. Bibliography 61</p>
<p>Chapter 3. Control of Timed Systems 67<br /> Franck CASSEZ and Nicolas MARKEY</p>
<p>3.1. Introduction 67</p>
<p>3.2. Timed games 72</p>
<p>3.3. Computation of winning states and strategies 76</p>
<p>3.4. Zeno strategies 82</p>
<p>3.5. Implementability 82</p>
<p>3.6. Specification of control objectives 85</p>
<p>3.7. Optimal control 87</p>
<p>3.8. Efficient algorithms for controller synthesis 92</p>
<p>3.9. Partial observation 96</p>
<p>3.10. Changing game rules 97</p>
<p>3.11. Bibliography 98</p>
<p>Chapter 4. Fault Diagnosis of Timed Systems 107<br /> Franck CASSEZ and Stavros TRIPAKIS</p>
<p>4.1. Introduction 107</p>
<p>4.2. Notations 109</p>
<p>4.3. Fault diagnosis problems 113</p>
<p>4.4. Fault diagnosis for discrete event systems 115</p>
<p>4.5. Fault diagnosis for timed systems 122</p>
<p>4.6. Other results and open problems 136</p>
<p>4.7. Bibliography 136</p>
<p>Chapter 5. Quantitative Verification of Markov Chains 139<br /> Susanna DONATELLI and Serge HADDAD</p>
<p>5.1. Introduction 139</p>
<p>5.2. Performance evaluation of Markov models 140</p>
<p>5.3. Verification of discrete time Markov chain 148</p>
<p>5.4. Verification of continuous time Markov chain 157</p>
<p>5.5. State of the art in the quantitative evaluation of Markov chains 160</p>
<p>5.6. Bibliography 162</p>
<p>Chapter 6. Tools for Model–Checking Timed Systems 165<br /> Alexandre DAVID, Gerd BEHRMANN, Peter BULYCHEV, Joakim BYG, Thomas CHATAIN, Kim G. LARSEN, Paul PETTERSSON, Jacob Illum RASMUSSEN, Ji&iexcl;ri SRBA,Wang YI, Kenneth Y. JOERGENSEN, Didier LIME,MorganMAGNIN, Olivier H. ROUX and Louis–Marie TRAONOUEZ</p>
<p>6.1. Introduction 165</p>
<p>6.2. UPPAAL 166</p>
<p>6.3. UPPAAL–CORA 182</p>
<p>6.4. UPPAAL–TIGA 185</p>
<p>6.5. TAPAAL 199</p>
<p>6.6. ROMEO: a tool for the analysis of timed extensions of Petri nets 205</p>
<p>6.7. Bibliography 217</p>
<p>Chapter 7. Tools for the Analysis of Hybrid Models 227<br /> Thao DANG, Goran FREHSE, Antoine GIRARD and Colas LE GUERNIC</p>
<p>7.1. Introduction 227</p>
<p>7.2. Hybrid automata and reachability 228</p>
<p>7.3. Linear hybrid automata 232</p>
<p>7.4. Piecewise affine hybrid systems 234</p>
<p>7.5. Hybridization techniques for reachability computations 241</p>
<p>7.6. Bibliography 249</p>
<p>List of Authors 253</p>
<p>Index 259</p>