Formal Specification of reactive systems:
DEVS or Timed Automata?
Frédéric Châne, Norbert Giambiasi, Jean-Luc Paillet,
LSIS, UMR CNRS 6168, Université Aix-Marseille III,
Campus St Jérome
13397- Marseille, FRANCE
Abstract:
This article aims to open the way to research activities, which would result in using the formalism of DEVS for realtime
system design. In this way, we will try to analyze why timed Automata are used in place of DEVS, and, we present
two transformation tools for a real time system designer that will help him to validate by simulation and verify by formal
proof this two kind of models.
I) Introduction
The design of discrete event control systems is a process that needs dedicated formalisms and adapted tools. These
formalisms may differ considerably in their syntax, semantics, and representation. However, the basic concepts of
discrete event models can be found in all these different formalisms. First of all, the input-output variables have discrete
event trajectories and the state variables have piecewise constant trajectories. Certain formalisms impose explicit states
(named), other ones have implicit states (states defined by a set of state variables). The state set can be finite or infinite
according to the formalism chosen and the system to be considered. Finally, the time can be represented implicitly
(untimed formalisms) or by actual values (timed formalisms).
In addition, some formalism seems better adapted in the first phases of the design process whereas aim towards lowlevel
models with a more precise representation of the system dynamics. For example, DEVS formalism is well adapted
to represent timed behavior of real systems. But DEVS (Zeigler 1976; Zeigler 1989; Zeigler, Praehofer and Kim 2000;
Giambiasi, Escude and Ghosh 2000) is not well suited to high-level specifications of discrete event control systems.
This is due to the fact that at the highest levels of specifications, the model can be undeterministic and the occurrence
times of events are not defined precisely.
DEVS defines a method of abstraction of dynamic systems that allows building timed discrete event simulation
models (deterministic models) with a good accuracy. DEVS is a symbolic specification of system semantics and there is
only one way to execute a DEVS model. DEVS Models are deterministic and this can be as an inconvenience for highlevel
specifications of real-time software. In fact, DEVS is well adapted to build models at low levels of abstraction.
Consequently, in the proposed approach we consider that the high-level specification of a control system is
expressed by a timed automaton and the system model to be controlled is a DEVS model. The verification of the highlevel
specification of the control system will be done by the simulation of a coupled DEVS model built from this
specification and the model of the system to be controlled. Within the framework of this methodology, we have
proposed a method to transform a Timed Automaton into a DEVS model (Giambiasi N., Paillet JL., and Châne F. 2003),
in order to allow the description and the simulation of the coupled DEVS of model of the whole system.
In another paper (Châne F., Giambiasi N., and Paillet JL.2004), a transformation from a DEVS Model into a timed
Input/Output automaton has been proposed in order to apply model checking method on DEVS models.
In this paper, first we give a brief recall of the transformation of a Timed Automata into a DEVS model and the
inverse transformation. A complete example illustrates these two transformations and show how simulation and model
checking methods can be used both for DEVS models and timed automata.
Methodology:
Reactive systems (D. Harel and A. Pnueli 1985;A. Pnueli 1986) cover a wild number of applications, in particular,
include several kind of systems like concurrent systems, distributed or real time system. Modeling phase is the most
important phase in the design process of real time systems. According to widely accepted principles of system
engineering, the functional system must be specified as complete, precise and unambiguous as possible (A. Wayne
Wymore, editor1993). A wide range of real time system can be described as a physical system and its control. The
following definition (J.E. Van Aken 1978): « Control is the use of control actions, or interventions, by a control system
to promote the preferred behavior of the system being controlled» well expresses the frontier between the control part of
the system and the physical part of the system. This does not mean that the controller completely defines the behavior of
the entire system.
The previous architecture of two distinct part of a reactive system is the one that we retain for real time high-level
specifications. Two classes of approaches offer a well-suited environment for high-level specifications and validation:
Formal proof methods and simulation based-methods. In the proposed approach, for formal proof, we use Timed
Input/Output Automata formalism (Alur, R. and Dill, D.L, 1978; D'Argenio P.R. , Katoen J.P.,Ruys T., and Tretmans J.
.....