Using Timed Automata for Modeling the Clocks of Distributed Embedded Systems

Introduction

The importance of adopting formal verification techniques in order to assess the correctness of embedded systems is nowadays beyond discussion. Through the use of formal methods, an embedded system can be precisely and unambiguously specified, and the specification can go through a systematic analysis that indicates whether the system behaves according to its requirements or not. This facilitates the early detection of design errors, which could reduce the development costs, and also causes a significant increase in the level of confidence of the system (Baier & Katoen, 2008).

Among the existing formal verification techniques, this chapter primary concerns model checking. Model checking is an automated technique that, given a model of a system and a logical property (a requirement), systematically checks whether this property holds for that model. Moreover, whenever the system does not fulfill the property, model checking provides a counter example (in the form of a trace) which can be extremely useful in order to find flaws in the system design.

Model checking was introduced in the eighties (Clarke & Emerson, 1981; Queille & Sifakis, 1982; Clarke, Emerson & Sistla, 1986) and has since then gained wide acceptance. Many advances have been reported and, as a consequence, several model checking tools (also known as model checkers) have been made available. Nevertheless, the usefulness of model checking still depends on the ability of the system designer to realistically express the behaviour of the system under verification. In fact, in the literature about formal verification it is often pointed out that “model checking is only as good as the model to be checked” (Baier & Katoen, 2008).

For the model checking of real-time systems, timed automata, (Alur & Dill, 1994) is a well established and widely used formalism. A timed automaton is a finite-state machine extended with real-valued variables, called clocks. The main advantage of timed automata is that they incorporate a quantitative notion of time, which makes this technique especially suitable for those systems in which the requirements are characterized by quantitative timing properties, i.e. by time bounds. Note that this is the case for most embedded systems, since they usually have to fulfill real-time requirements that are specified in the form of periods, deadlines, etc.

Nevertheless, the mechanism for time representation in timed automata exhibits a particularity that is sometimes regarded as a limitation to the modeling: it assumes that all the clocks in a model increase at the same rate. In other words, it assumes that only one time base is available in the system. Although such an assumption can be suitable for modeling most single-processor embedded systems, in which actually only one computer clock exists, it is not acceptable for the modeling of many distributed embedded systems. In a distributed embedded system, each node usually works with its own computer clock, and since the computer clocks may not tick at exactly the same rate, the perception of time among the nodes is not consistent. Even when some kind of clock synchronization mechanism is used by the nodes, the drift of the computer clocks cannot be perfectly corrected and thus certain residual degree of inconsistency (the so-called precision) always persists among them.

Due to this, it might seem that the timed automata formalism is not suitable for modeling and verifying distributed embedded systems with such clocks. However, various modeling techniques can actually be used in order to circumvent this limitation and specify different time bases in the timed automata that compose a system model. Descriptions of these techniques can be found in the literature, but since they are scattered in different publications, for instance in (Alur, Torre & Madhusudan, 2005; Daws & Yovine, 1995; Rodriguez-Navas, Proenza & Hansson, 2006), it is unfortunately difficult to have a general perspective of what can be done, and how.