![]()
Chapter 1
Models for Real-Time Embedded Systems 1
1.1. Introduction
The class of real-time embedded systems contains software components that control an application by reacting to stimuli received from a changing environment. Therefore, they are often referred to as reactive systems. The reaction time of these systems must be small enough to cope with the internal dynamics of the controlled or monitored application. They must thus obey the strong timing requirements, and it is crucial to ensure their correctness from both the functional and temporal points of view.
Real-time applications are often regarded as safety critical because their failures may either involve substantial financial losses or endanger human lives. It is also important to detect any error at an early stage to minimize the costs involved in its correction. This issue can be addressed by several approaches. Let us consider the following two approaches: in the first approach, from the application requirements, a model for the application and its expected properties are derived. Then a controller is proposed, using expert knowledge, to restrict the application behavior in order to satisfy the given properties. The next step is to validate the proposed controller using different techniques such as testing, theorem proving, formal verification, etc. If the controller is not acceptable, then it has to be reworked on the basis of the knowledge gained from the reported failures or counter-examples. In the second approach, the controller will be synthesized automatically from the formal model of the application. If such a controller exists, which may not be the case, for example, if the requirements are incoherent, then a method to implement should be derived. Alternatively, if the controller model cannot be implemented, the problem has to be reworked from the beginning.
In this chapter, we will address the formal methods relating to these two approaches and those based on state-transition models. The models presented here deal with instantaneous actions and real-valued variables. The former approach usually models relevant events in the systems such as those relative to the command of the actuators or to the measures of sensors and the latter approach models durations of processes. These models thus describe subclasses of real-time embedded systems.
1.1.1. Model-checking and control problems
The requirements of a computer application are usually given as a natural language document. Therefore, they are subject to the interpretation of the persons who will derive the specification from them, which may result in many errors. Moreover, it is impossible for a conceptor to understand all possible interactions of the components of any reasonably sized application.
Formal methods aim at providing a mathematical framework for a clear, non-ambiguous and precise description of the systems and programs we want to develop. In this framework, the system is described by a labeled transition system or any model abstracting such a systems, e.g. automata, Petri nets, process algebra, etc. The specification may be either described in the same manner or as a property expressed in a suitable logic, such as linear temporal logics (LTL) or tree-based temporal logics (CTL), or even their timed extensions. A classical example of a real-time property is the bounded response property which requires that for the execution of the system, whenever some predicate P0 on the states of the system becomes true, then some other predicate P1 will become true, within n time units.
Among formal methods, model-checking is an automatic procedure that verifies whether a system satisfies a given temporal logic property. It usually works by exploring parts of the set of possible states of the system.
Controller synthesis consists of automatically synthesizing a program (the controller) that leads the interaction mec...
