Communicating Embedded Systems for Computer Science

Informationen zum Autor 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. Klappentext 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. Zusammenfassung 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. Inhaltsverzeichnis Preface xi Claude JARD and Olivier H. ROUX Chapter 1. Models for Real-Time Embedded Systems 1 Didier LIME! Olivier H. ROUX and Ji!ri SRBA 1.1. Introduction 1 1.2. Notations! languages and timed transition systems 5 1.3. Timed models 8 1.4. Models with stopwatches 23 1.5. Conclusion 31 1.6. Bibliography 31 Chapter 2. Timed Model-Checking 39 Beatrice BERARD 2.1. Introduction 39 2.2. Timed models 40 2.3. Timed logics 46 2.4. Timed model-checking 51 2.5. Conclusion 61 2.6. Bibliography 61 Chapter 3. Control of Timed Systems 67 Franck CASSEZ and Nicolas MARKEY 3.1. Introduction 67 3.2. Timed games 72 3.3. Computation of winning states and strategies 76 3.4. Zeno strategies 82 3.5. Implementability 82 3.6. Specification of control objectives 85 3.7. Optimal control 87 3.8. Efficient algorithms for controller synthesis 92 3.9. Partial observation 96 3.10. Changing game rules 97 3.11. Bibliography 98 Chapter 4. Fault Diagnosis of Timed Systems 107 Franck CASSEZ and Stavros TRIPAKIS 4.1. Introduction 107 4.2. Notations 109 4.3. Fault diagnosis problems 113 4.4. Fault diagnosis for discrete event systems 115 4.5. Fault diagnosis for timed systems 122 4.6. Other results and open problems 136 4.7. Bibliography 136 Chapter 5. Quantitative Verification of Markov Chains 139 Susanna DONATELLI and Serge HADDAD 5.1. Introduction 139 5.2. Performance evaluation of Markov models 140 5.3. Verification of discrete time Markov chain 148 5.4. Verification of continuous time Markov chain 157 5.5. State of the art in the quantitative evaluation of Markov chains 160 5.6. Bibliography 162 Chapter 6. Tools for Model-Checking Timed Systems 165 Alexandre 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 TRAONOUEZ 6.1. Introduction 165 6.2. UPPAAL 166 6.3. UPPAAL-CORA 182 6.4. UPPAAL-TIGA 185 6.5. ...

List of contents

Preface xi
Claude JARD and Olivier H. ROUX

Chapter 1. Models for Real-Time Embedded Systems 1
Didier LIME, Olivier H. ROUX and Ji¡ri SRBA

1.1. Introduction 1

1.2. Notations, languages and timed transition systems 5

1.3. Timed models 8

1.4. Models with stopwatches 23

1.5. Conclusion 31

1.6. Bibliography 31

Chapter 2. Timed Model-Checking 39
Beatrice BERARD

2.1. Introduction 39

2.2. Timed models 40

2.3. Timed logics 46

2.4. Timed model-checking 51

2.5. Conclusion 61

2.6. Bibliography 61

Chapter 3. Control of Timed Systems 67
Franck CASSEZ and Nicolas MARKEY

3.1. Introduction 67

3.2. Timed games 72

3.3. Computation of winning states and strategies 76

3.4. Zeno strategies 82

3.5. Implementability 82

3.6. Specification of control objectives 85

3.7. Optimal control 87

3.8. Efficient algorithms for controller synthesis 92

3.9. Partial observation 96

3.10. Changing game rules 97

3.11. Bibliography 98

Chapter 4. Fault Diagnosis of Timed Systems 107
Franck CASSEZ and Stavros TRIPAKIS

4.1. Introduction 107

4.2. Notations 109

4.3. Fault diagnosis problems 113

4.4. Fault diagnosis for discrete event systems 115

4.5. Fault diagnosis for timed systems 122

4.6. Other results and open problems 136

4.7. Bibliography 136

Chapter 5. Quantitative Verification of Markov Chains 139
Susanna DONATELLI and Serge HADDAD

5.1. Introduction 139

5.2. Performance evaluation of Markov models 140

5.3. Verification of discrete time Markov chain 148

5.4. Verification of continuous time Markov chain 157

5.5. State of the art in the quantitative evaluation of Markov chains 160

5.6. Bibliography 162

Chapter 6. Tools for Model-Checking Timed Systems 165
Alexandre 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 TRAONOUEZ

6.1. Introduction 165

6.2. UPPAAL 166

6.3. UPPAAL-CORA 182

6.4. UPPAAL-TIGA 185

6.5. TAPAAL 199

6.6. ROMEO: a tool for the analysis of timed extensions of Petri nets 205

6.7. Bibliography 217

Chapter 7. Tools for the Analysis of Hybrid Models 227
Thao DANG, Goran FREHSE, Antoine GIRARD and Colas LE GUERNIC

7.1. Introduction 227

7.2. Hybrid automata and reachability 228

7.3. Linear hybrid automata 232

7.4. Piecewise affine hybrid systems 234

7.5. Hybridization techniques for reachability computations 241

7.6. Bibliography 249

List of Authors 253

Index 259

About the author

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.

Summary

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.

Product details

• Authors: JARD, C Jard, Claud Jard, Claude Jard, Claude/ Roux Jard, Olivier Roux
• Assisted by: Claude Jard (Editor), Olivier Roux (Editor), Olivier H. Roux (Editor)
• Publisher: Wiley, John and Sons Ltd
• Languages: English
• Product format: Hardback
• Released: 30.12.2009
• EAN: 9781848211438
• ISBN: 978-1-84821-143-8
• Series: ISTE
• Subjects: Natural sciences, medicine, IT, technology > IT, data processing > IT; Informatik, computer science, Programmierung u. Software-Entwicklung, Programming & Software Development, Eingebettetes System