Communicating Embedded Systems: Software and Design

Chapter 2

Timed Model-Checking ¹

2.1. Introduction

Reactive systems are those which handle interactions with the environment. They are frequently used in the area of transportation, communication protocols, or medical instrumentation, and often contain critical parts, where software errors can have heavy consequences. Many examples can be found in the PhD thesis of E. Fleury [FLE 02]. Even if there is a large agreement about the need for correctness of such systems, frequent accidents show that a formal verification step cannot be avoided.

Test generation is certainly the most commonly used technique. It consists of feeding input scenarios to a system and observing the output. The problem is then to guarantee a sufficient coverage of the behavior of the system, which is a difficult task. Other methods like theorem proving or model-checking ensure the completeness of the verification, but they suffer from the so-called “combinatorial explosion problem”, which sets an intrinsic limit on the systems size.

Model-checking (see [CLA 08], [BAI 99] or [SCH 01] for overviews) answers to the following question: given a system and a property; does the property hold in the system? The first step consists of building formal models S and P, respectively, for the system and the property, and subsequently applying a suitable algorithm that automatically solves the problem: does S satisfy P, denoted by ? The formalisms used for the system and the property should be the most expressive, whereas ...