Communicating Embedded Systems: Software and Design

Contents

Preface

Chapter 1. Models for Real-Time Embedded Systems

1.1. Introduction

1.2. Notations, languages and timed transition systems

1.3. Timed models

1.4. Models with stopwatches

1.5. Conclusion

1.6. Bibliography

Chapter 2. Timed Model-Checking

2.1. Introduction

2.2. Timed models

2.3. Timed logics

2.4. Timed model-checking

2.5. Conclusion

2.6. Bibliography

Chapter 3. Control of Timed Systems

3.1. Introduction

3.2. Timed games

3.3. Computation of winning states and strategies

3.4. Zeno strategies

3.5. Implementability

3.6. Specification of control objectives

3.7. Optimal control

3.8. Efficient algorithms for controller synthesis

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.3. Fault diagnosis problems

4.4. Fault diagnosis for discrete event systems

4.5. Fault diagnosis for timed systems

4.6. Other results and open problems

4.7. Bibliography

Chapter 5. Quantitative Verification of Markov Chains

5.1. Introduction

5.2. Performance evaluation of Markov models

5.3. Verification of discrete time Markov chain

5.4. Verification of continuous time Markov chain

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

5.6. Bibliography

Chapter 6. Tools for Model-Checking Timed Systems

6.1. Introduction

6.2. Uppaal

6.3. Uppaal-CORA

6.4. Uppaal-TIGA

6.5. TAPAAL

6.6. Roméo: a tool for the analysis of timed extensions of Petri nets

6.7. Bibliography

Chapter 7. Tools for the ...