USING DECM TO FORMALLY DESCRIBE THE BEHAVIOUR OF
CONTROLLED SYSTEMS
Jean-Luc Paillet Watcharee Jumpamule Norbert Giambiasi
LSIS, CMI,
39 av. Joliot-Curie
13453 Marseille France
Jean-Luc.Paillet@cmi.univ-mrs.fr
Computer Science Department
Chiang Mai University
50202 Chiang Mai, Thailand
sccsi003@chiangmai.ac.th
LSIS, Polytech
Av. Escadrille Normandie-Niemen
13387 Marseille, France
norbert.giambiasi@lsis.org
Key word. Formal specifications, discrete event systems.
ABSTRACT
We defined an original formalism, DECM,
allowing nonspecialists to formally specify discrete
event control systems, in a natural way. But for
validating the specifications of a control system, we
have to build a coupled model including the control
system and the physical system to be controlled. In this
paper, we show that DECM can be used to represent
both system, in a uniform way, by using auxiliary time
functions. Such a use of DECM is illustrated by a case
study.
1. INTRODUCTION
Our previous works concerned the design of
correct control systems from informal descriptions of the
required behaviours. We defined an original
mathematical model (Paillet and Giambiasi 2002),
DECM (Discrete Event Calculus Model), to represent
the behaviour of timed discrete event systems at a high
level of abstraction. Of course, there is a lot of
formalisms available to model controllers and plants.
Nevertheless, most of these formalisms are based on the
paradigm of state (or « places ») transitions such as, for
example, SpecCharts (Gajski et al., 1994), Petri nets
(Peterson, 1981), CCS (Milner, 1980), or they are
inspired by the timed automata paradigm (Alur and Dill,
1994) as, for example, in various extensions of LOTOS
(Is, 1989). We do not think that these formalisms are the
most suitable for specifying real-time systems at a high
level of abstrraction, in a natural way. The concept of
event is more natural than the concept of state transitions
(Buss, 1996 ; Schruben, 1997 ; Giambiasi et al., 1995).
DECM formalism is based on the concept of event and
the basic objects are defined by means of functions
representing temporal behaviours. Moreover, the
«intensive» (algebraic) DECM formulations of
behaviors are well suited for future studies on possible
formal verifications.
We developed a formal language, based on DECM
concepts, which allows nonspecialist users to formally
specify control systems in terms of causal relationships
between timed events. This language uses algebraic
expressions, “event expressions”, and conditional
clauses, to determine the output events sent out in
reaction to input events received by the system.
Nevertheless, validating the specifications of a control
system requires to combine a description of the control
system and one of the controlled physical system, and to
validate the behaviour of the coupled system. Presently,
we use simulations of "coupled models" (Jumpamule
and al. 2003) to validate the initial specifications of the
control system. Thus, we should use a formal
description of the behaviour of the controlled system as
well. We can suppose that this formal description is
provided by means of a library of components written in
a widely used formalism, such as DEVS (Zeigler 1976).
Nevertheless,
- in the one hand, it is not always the case, especially
for specific or new technology components. We can
have only an informal description of the behavior
- in the other hand, we can want to use a different
formalism (Blanc and al. 2003) from the one used in the
library.
In any case, it is better to have a unified formalism to
describe both of the control and the controlled systems,
as a central core for various validation methods.
DECM was tailored to describe control systems and the
behaviour of these systems is purely logical. A
contrario, in a controlled physical system, output events
occur as delayed reactions to control events. In fact,
when a control event is received by an actuator, a given
physical component executes some task (e.g. a
mechanical movement). When this task is completed, a
specific event is emitted by a sensor.
The cases where erroneous control events are sent to the
controlled system with erroneous timing must be taken
into account during the validation process.
For that purpose, we add new auxiliary functions to
DECM formalism. These new functions are used to
compute the "accumulated" running time necessary to
complete (if possible) the considered work. By using the
concept of updatable timed variable, which generalizes
.....