Communicating Embedded Systems: Software and Design

Chapter 4

Fault Diagnosis of Timed Systems ¹

In this chapter, we review the main results pertaining to the problem of fault diagnosis of timed automata. Timed automata are introduced in Chapters 1 and 2 in this book, and the reader not familiar with this model is invited to read them first.

4.1. Introduction

Many computerized systems (sometimes embedded) supervise/control devices or appliances the failure of which can be life-threatening (airplanes, railways, nuclear plants, medical devices etc.) or extremely expensive (Ariane 5 rocket, telephone networks etc.).

For more than two decades, researchers have tried to develop tools and algorithms to increase the dependability of computerized systems. All verification techniques can be gathered under the generic name of formal methods, the most famous and successful one certainly being model checking [SCH 99], which consists of building a mathematical model of a system S, and then checking that it satisfies a given property ϕ. It is sometimes even possible to synthesize a controller C (see Chapter 3) for S, in order to ensure that the controlled system C(S) satisfies a property ϕ.

The model checking and controller synthesis techniques assume that we can build a complete model of the system (and the controller), and everything is observable (controller synthesis under partial observation can also be solved for some particular properties for timed automata). Also it might be that no controller exists or it is not possible to compute one, ...