Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE.
The benefits of using a synchronous data-flow language for programming critical real-time systems are investigated. These benefits concern ergonomy (since the dataflow approach meets traditional description tools used in this domain) and ability to support formal design and verification methods. It is shown, using a simple example, how the language LUSTRE and its associated verification tool LESAR, can be used to design a program, to specify its critical properties, and to verify these properties. As the language LUSTRE and its uses have already been discussed in several papers, emphasis is put on program verification.
Introduction
It is useless to repeat why real-time programs are among those in which errors can have the most
dramatic consequences. Thus, these programs constitute a domain where there is a special need
of rigorous design methods. We advocate a "language approach" to this problem, arguing that
the programming language used has a direct influence in the quality of the software, from several
points of view:
(i) The language should allow a natural description of the problem to be solved. In particular,
it should be close to the traditional tools used in its application field.
(ii) The language should be formally sound, in order to support formal verification methods.
(iii) The language should be simple enough to minimize the risk of misunderstanding about
program meanings.
These were our main goals in designing the language Lustre [11, 18]. To meet the criterion (i),
we started from the traditional description tools used in the design of process control systems:
At a higher level, these tools consist of mathematical formalisms (differential equations, boolean
while at a lower level, people often use data-flow nets (block-diagrams, analog
schemas, switch or gate networks, These two classes of tools are closely related: For instance,
This work was partially supported by ESPRIT Basic Research Action "SPEC" and by a contract from Merlin
Gerin
differential equations, finite difference equations, boolean equations can be straightforwardly
translated, respectively, into analog schemas, block-diagrams and gate networks. At least the
class of high level tools also meets our criterion (ii), since they are derived from the mathematical
language. Other authors (e.g., [23, 2]) claimed that such declarative formalisms are simpler and
cleaner than usual imperative languages, where assignments, side-effects, aliasing, parameter
passing mechanisms, are unnatural phenomena which are difficult to understand and manage.
We agree with this claim, and therefore consider that these declarative formalisms constitute a
good basis for designing a programming language meeting the criterion (iii).
Lustre is a synchronous data-flow language, initially inspired from Lucid. As in Lucid, any
Lustre variable or expression is considered to represent the sequence of values it takes during
the whole execution of the program, and Lustre operators are considered to operate globally
over these sequences. The synchronous nature of the language consists in assuming that all the
variables and expressions in a program take the n-th value of their respective sequences at the
same time. More concretely, a program is intended to have a cyclic behavior, an execution cycle
consisting in computing the n-th value of each variable or expression. Basically, a program is a set
of equations. When we write an equation "X=E", where X is a variable and E is an expression, we
mean that the sequences of values associated with X and E are identical (it is an actual equation,
in the mathematical sense), or equivalently, that at any cycle of the program, X and E take the
same value.
Time and synchrony
The "real time" capabilities of the language are derived from this synchronous interpretation,
like in other synchronous languages [6, 8, 13, 21, 24]: We consider the following logical notion
of time: As soon as we can specify the order or simultaneity relations between events occurring
both inside and outside the program, we can express time constraints about the behavior of the
program. For instance, a constraint like
"any occurrence of a dangerous situation must be followed by the emission of an alarm
within a delay of 2 seconds"
will be expressed as
"after any occurrence of the event dangerous situation there must be an occurrence
of the event alarm before the 2nd next occurrence of the event second"
This example shows that, in synchronous programming, the "real", physical time is considered
as an external event (here second), which has no privileged nature. This is the multiform time
point of view: Time may be counted in "seconds" as well as in "meters", since there is no
conceptual difference between the two following requirements:
the train must stop within 10 seconds and the train must stop within 100 meters
In a synchronous language, these constraints are expressed in similar ways, in contrast with
languages like ADA, where "real" time is handled by special statements.
In Lustre, an event will be modeled by a boolean variable, whose value is true whenever
the event occurs.
The synchronous interpretation is an abstract point of view which consider the program reaction
time to be negligible with respect to the reaction time of its environment. The advantages of
this abstraction have been pointed out [5, 4, 3] concerning the semantics cleanness and the fact
that it reconciles concurrency and determinism. In particular [4] argues that synchronous languages
are particularly well-suited for programming reactive kernels of real-time systems, while
complex systems generally require the combination of asynchronous and synchronous modules.
We do not claim, therefore, that synchronous languages are general purpose languages, but rather
specialized tools to design such kernels.
One may wonder about the realism of the synchronous hypothesis, since it assumes that
the machine instantly reacts to input events. In fact, it only assumes that the reaction time
is short enough to accurately distinguish and order the incoming events. In practice, it can be
checked by measuring the maximum reaction time of the program. Synchronous languages can
be implemented in a particularly efficient and measurable way, following a technique developed
for Esterel [6]. Two versions of Lustre compilers have been written [11, 20], which use this
technique. The object code is structured as a finite automaton, a transition of which corresponds
to a reaction of the program 1 . The code corresponding to such a transition is linear (loop-free),
and its maximal execution time can be accurately bounded, on a given machine. Therefore, the
validity of the synchrony hypothesis can be checked, and it is the only "real-time" issue in the
synchronous approach. All the design and verification we will perform rely on that checking.
In Section 2, we briefly present the language, whose use is illustrated in Section 3 on a small
example adapted from an actual subway device.
Specification and verification
The remainder of the paper is devoted to program verification. As said before, the synchronous
approach limits the "timing" verification to checking the validity of the synchrony hypothesis.
So, the kind of verification we have in mind is similar to standard verification on transition
systems. It has nothing to do with methods and models (like, e.g., [16, 26]) taking into account
the program execution time - which is always assumed to be zero in the synchronous model.
Moreover, our goal is not to prove the correctness of a program with respect to some complete
specifications, but rather to express and verify some critical properties. For instance, in
an aircraft flight control system, an error in the speed computation can have only slight conse-
quences, whereas it is critical that the undercarriage be locked when landing. Our claim is that
these critical properties are usually simple, and can be verified by means of available automatic
techniques. The main reason for this claim is that experience shows that most of these properties
are "safety" properties which state that a given situation should never occur, or that a given
statement should always hold, in contrast with "liveness" properties which state that a given
situation should eventually occur in the future 2 . For instance, a relevant question is not that a
train will eventually stop, but that it never crosses a red light. This is an important remark as
proof techniques for safety properties are known to be much simpler than for liveness properties:
ffl Safety properties can be checked on program abstractions: Intuitively, one can simplify
a given program P into an abstract program P 0 , having "more behaviors" than P . If P 0
satisfies a safety property, so does P . This abstraction technique is valuable all the more
as experience shows that the considered critical properties seldom depend on numerical
This compiling technique is specific to synchronous languages, since, in an asynchronous language, the non
deterministic interleaving of asynchronous actions would involve immediately a combinatorial explosion of the
automaton size.
As a matter of fact, liveness properties are often introduced to "abstract" response time constraints, which
must be taken fully into account in a real-time system.
relations and computations, but more often on logical dependencies over events. So their
proof can often be handled on finite state abstractions of programs.
ffl Safety properties can be checked on program states, rather than on execution paths. In the
approach we will propose, any verification problem amounts at proving that some program
never outputs the value false. In the finite state case, such a verification can be done by a
simple traversal of the state graph, without keeping track of any path in that graph. Very
efficient methods [22] have been proposed for such a traversal.
ffl Safety properties can be modularly verified: With any process composition operator ?, one
can easily associate an operator ? such that, for any two processes P 1 and P 2 , respectively
satisfying safety properties OE 1 and OE 2 , their composition
verification problem can be decomposed into simpler ones.
So, our ambition is rather modest - since we restrict ourselves to checking safety properties on
finite state (abstractions of) programs - with the hope of getting efficient tools tackling many
real-life cases.
In view of this discussion, we propose a method for specifying and checking simple safety
properties about Lustre programs. In Section 4, we show that we can take advantage of the
declarative nature of Lustre, to express the properties in the same language: It has been
shown [7] that any safety property about a program can be expressed by the invariance of
some boolean Lustre expression. This is due to the fact that Lustre can be viewed as an
executable temporal logic. Concerning ergonomics, there is an obvious advantage of using a full
programming language instead of a temporal logic. In particular, the user can define its own
temporal operators 3 , thus reducing the complexity of property expression.
Moreover, Lustre provides a means of expressing assumptions about the program environ-
ment. This is an essential feature, since the interaction of a real-time program with its environment
is particularly important. In general, the properties of a real-time program are intended to
hold only under some assumptions about the behavior of its environment, and these assumptions
can be quite complex. So, the verification process deals with three entities: The program, the
property (expressed by an invariant) and the assumptions under which the property is intended
to hold (also expressed by an invariant).
Sections 5 and 6 illustrates the proposed approach on our example. The verification (Sec-
tion 7) is performed on a finite state abstraction of the program, which models only the behavior
of boolean variables. A verification tool, called Lesar, is available, which can apply two verification
techniques:
ffl the former is an exhaustive enumeration of the states of the (abstraction of the) program,
similar to standard model checking [12, 27].
ffl the later is a symbolic construction of the set of states which satisfy the property, analogous
to "symbolic model checking" [10, 14, 15].
These techniques will be applied to the example introduced in Section 3.
Finally, Section 8 outlines a method for modular verification: taking advantage of the fact
that the program and its properties are expressed in the same language, we can use the proved
properties of a subprogram in the verification of a full program. This technique can reduce the
complexity of the verification.
3 This is a more powerful mechanism than the macro-notation offered by some specification languages [12, 29].
2 The language Lustre
We do not give here a detailed presentation of the language Lustre, which can be found elsewhere
[11, 18]. We only recall the elements which are necessary for understanding the paper.
A Lustre program specifies a relation between input and output variables. Any variable or
expression is intended to be a function of time. Time is assimilated to the set of natural numbers.
Variables are defined by means of equations (one and only one equation for each variable which
is not an input): As said before, an equation "X=E", where E is a Lustre expression, specifies
that the variable X is always equal to E.
Expressions are made of variable identifiers, constants (considered as constant functions),
usual arithmetic, boolean and conditional operators (considered as pointwisely applying to func-
tions) and only two specific operators: the "previous" operator and the "followed-by" operator:
ffl If E is an expression denoting the function -n:e(n), then "pre(E)" is an expression denoting
the function
-n:
nil if
where nil is an undefined value.
are two expressions of the same type, respectively denoting the functions -n:e(n)
and -n:f(n), then "E -? F" is an expression denoting the function
-n:
In addition to equations, a Lustre program can contain assertions, of the form "assert E",
where E is any boolean expression. This means that E is assumed to be always true during
the execution of the program. For instance, "assert not(ON and OFF)" expresses that the
input events ON and OFF never occur at the same time. Assertions were introduced in order to
express some known properties of the environment, for optimization purposes. They will play
an important role in program verification.
A Lustre program is structured into nodes : a node is a subprogram specifying a relation
between its input and output parameters. This relation is expressed by an unordered set of
equations and assertions, possibly involving local variables. Once declared, a node may be
functionally used in any expression, as a basic operator.
For instance the following declaration defines a node, of general usage, which returns true
whenever its boolean parameter raises from false to true:
node edge(X: bool) returns (EDGE: bool);
let
not pre(X);
tel
Now, the expression edge(not C) is true whenever the variable C has a falling edge.
3 Example of program
Let us introduce an example adapted from a subway device. At each end of a subway line, a
special "U-turn" section allows trains to switch from one track to the other, and to go back in
the opposite direction (see Fig. 1). A U-turn section is composed of three tracks A, B, C, and a
switch S. Assuming the entering track is A and the exiting track is C, trains switching from A to
C must first wait for S to connect A with B, then transit on B and wait again for S to connect
with C before going back on C.
Considering that several trains move along the tracks and that the switch is not a safe device,
two kinds of accidents may occur within the section:
ffl if several trains are allowed to access the section together, they may collide.
ffl if the switch is not well positioned, trains will derail.
It is therefore clear that controlling a U-turn section is a highly critical task. Any automatic U-turn
section management system (later on called UMS) must both drive the switch and manage
train movements along the section so as to avoid accidents.
Such a system is typically reactive: upon receipt of information about the switch status and
about the train position inside the section, it should deliver positioning requests to the switch
and access grants to trains. These four kinds of events can be modeled by the following signals:
ffl ack AB and ack BC indicate whether the switch actually connects A with B or B with C.
If none of these signals is active, trains must not take the switch.
ffl on A, on B and on C are three sensors, one on each track of the section. They are active as
long as there is a train on the track they observe.
ffl do AB and do BC are the requests for the switch to connect A with B or B with C.
ffl grant access and grant exit are grants for trains to move along the section. They
correspond to traffic lights. The first one will allow trains to access the section only if it
is empty and if the switch connects A with B. The second one will allow trains to exit B
only if the switch connects B with C.
An overview of the system and its environment is given in Fig. 2. Let us now implement the
UMS in Lustre. In the sequel, it is assumed that initially, there is no train in the section. Let us
define the equations for the switch positioning requests. The switch will be requested to connect
A with B each time the section is empty and to connect B with C each time a train has arrived
on B. These requests will remain active until the switch is in the right position. In Lustre, we
directly get the equations:

Figure

1: A subway U-turn section
ack AB
ack
on B
UMS
on A
on C
grant access grant exit
do
do AB
A

Figure

2: The UMS system and its environment
not ack-AB and empty-section;
not ack-BC and only-on-B;
Here, empty section states that no train is in the section, while only on B states that the only
trains in the section are on B. The equations for these variables are the followings:
or on-B or on-C);
and not(on-A or on-C);
Now, we have to write the equations defining the movement grants. As mentioned before, access
to the section will be granted only if it is empty and if the switch connects A with B. We therefore
get the following equation:
empty-section and ack-AB;
Trains will be granted to exit the section when the switch connects B with C and when the only
trains in the section are on B. So, we get:
We finally get the whole Lustre program for the UMS system, shown by Fig. 3. This simple
example intends to show that Lustre is well-suited for programming such systems, as all
the equations written in the program are straightforwardly deduced from the informal specifications
of the U-turn section. The fact that equations can be written in any order encourages
a progressive translation of the specifications: each requirement is expressed in turn, possibly
involving the introduction of auxiliary variables. Notice that introducing an auxiliary variable
(like empty section), for naming an expression, has no influence on the program semantics, but
can increase its readability.
node UMS(on A,on B,on C,ack AB,ack BC: bool)
returns (grant access,grant exit, do AB,do BC: bool);
var empty section, only on B: bool;
let
grant access = empty section and ack AB;
grant only on B and ack BC;
do not ack AB and empty section;
do not ack BC and only on B;
empty section = not(on A or on B or on C);
only on B = on B and not(on A or on C);
tel

Figure

3: The Lustre program for the UMS system
Expressing critical properties
Let us now consider the expression of the critical properties of a program. Many formalisms have
been proposed for that, most of them being inspired either from temporal logics or from process
algebras. However, in order to reduce the user's effort, we have been looking for a formalism
being as close as possible to the programming language. So, we propose to express a property
as the invariance of some boolean Lustre expression. Having to express a property P about
a program \Pi, we will write a boolean expression B such that P is satisfied if and only if B is
always true during any execution of \Pi. It has been shown elsewhere [7] that Lustre can be
viewed as a subset of linear temporal logic [25], and that any safety property can be expressed
in that way. From our experience, the critical properties required for a real-time system almost
always fall into this class: as a matter of fact, nobody cares whether an alarm eventually follows
a dangerous situation, but rather whether it occurs within a given delay!
Let us show how some useful non trivial temporal operators can be expressed as Lustre
nodes. Consider the following property:
"Any occurrence of a critical situation causes an alarm, which must be sustained
within a five seconds delay"
Such a property relates three events: the occurrence of the critical situation, the alarm, and the
deadline. A general pattern for this property is the following one:
"Any occurrence of the event A must cause the condition B to be true until the next
occurrence of the event C"
However, this formulation is not directly translatable into Lustre as it refers to what happens
in the future following an A occurrence, while Lustre only allows references to the past
with respect to the current instant. That is why we first translate it into the equivalent past
"Any time A has occurred in the past, either B has been continuously true, or C has
occurred at least once, since the last occurrence of A"
Let us define a node, taking three boolean input parameters A, B, C, and returning a boolean
output X such that X is always true if and only if the property holds:
node always-from-to(B,A,C: bool) returns (X: bool);
let
tel
The equation defining X uses four auxiliary nodes:
ffl The nodes implies implements the ordinary logical implication:
node implies(A, B: bool) returns (AimpliesB: bool);
let
not A or B;
tel
ffl The node after returns the value false until the first time its input is true. Then it returns
true for ever:
node after(A: bool) returns (afterA: bool);
let
tel
ffl The node always since has two inputs and returns true if and only if its first input has
been continuously true since the last time its second input was true:
node always-since(B,A: bool) returns (alwaysBsinceA: bool);
let
else if after(A) then B and pre(alwaysBsinceA)
else true;
tel
ffl Finally, the node once since has two inputs and returns true if and only if its first input
has been at least once true since the last time its second input was true:
node once-since(C,A: bool) returns (onceCsinceA: bool);
let
else if after(A) then C or pre(onceCsinceA)
else true;
tel
These nodes will be used in our example. Of course, other operators could be defined in the
same way (see [19]).
5 Critical properties of the example
Let us express in Lustre the set of safety properties required from our U-turn management
system. As mentioned before, this system must always avoid the occurrence of two dangerous
situations.
The first one concerns train collisions. We have to check that a train may enter the section
only if this one is empty. In Lustre, this property will be expressed by the invariance of a
boolean variable no collision, defined as follows:
From the equation defining grant access, this property is obviously true. So, assuming that no
train enters the section by track C, it is possible to consider by now that no more than one train
is in the section at any time.
We only have to check now that a train entering the section by track A will always leave it
by track C, and that no derailment is possible. This leads to verify how the switch is driven.
First, it is clear that the switch positioning requests should never be both active at the same
time. This is simply expressed by the invariance of the following Lustre expression:
The switch should also connect A to B from the instant when a train is allowed to enter the
section until it has arrived on track B. This leads to the following property:
Similarly, the switch should always connect B to C from the instant when a train is allowed to
leave the section until it has actually left it:
Notice that if the above property is true, a train cannot leave the section by track A.
Finally, the global property to prove is expressed by the following Lustre equation:
no-collision and exclusive-req and no-derail-AB and no-derail-BC;
6 Modeling the environment
The next step in the verification process should consist in running the verification tool and check
whether the safety properties above are preserved by the UMS. However, at that point, an important
and crucial task is to provide a description of how the environment of the system behaves.
Actually, the environment obeys some rules which restrict its possible behaviors. For instance,
in a U-turn section, trains are assumed to stop when traffic lights are red. The verification tool
would certainly not achieve checking the system without being aware of such an information.
It is therefore necessary to define some assumptions about the behavior of the environment. In
Lustre, this is done using the assertion mechanism. As said before, Lustre assertions express
that some boolean expressions can be assumed to be always true.
Let us describe in that way some important features of the U-turn section environment. We
can make the following assumptions about the
ffl the switch cannot both connect A with B and B with C:
assert not(ack-AB and ack-BC);
ffl Once in a given position, the switch remains stable unless it is requested to move to the
opposite position:
assert always-from-to(ack-AB,ack-AB,do-BC)
and always-from-to(ack-BC,ack-BC,do-AB);
About train movements inside the section, we make the following assumptions:
ffl Initially, there is no train in the section.
assert empty-section -? true;
(Remember that "empty section -? true" is equal to "empty section" at the initial
instant, and then is true forever; so the above assertion only restricts the initial value of
"empty section")
Trains obey traffic lights. So, if a train enters or leaves the section, then the corresponding
traffic light was green at the instant before. Therefore, we get (using the node edge defined
in Section 2):
assert true -? implies(edge(not empty-section), pre grant-access);
assert true -? implies(edge(on-C), pre grant-exit);
ffl When a train leaves A, it is on B. When a train leaves B, it is either on A or on C.
assert implies(edge(not on-A),on-B);
assert implies(edge(not on-B), on-A or on-C);
This example and our experience show that specifying the environment behavior of a program
requires important efforts. Such a work undoubtly adds some complexity to the verification
task. However, giving such a precise specification of the assumptions made on the environment
behavior is certainly a useful task in designing a critical system. Moreover, notice that these
assumptions can be dynamically checked, during the execution of the program (a compiler option
produces the corresponding code). They can be used also in a testing phase, for choosing valid
testcases.
7 Program verification
We consider now the verification problem. Given a program \Pi, a property P expressed by a
boolean expression B which must be invariantly true under some assumptions expressed by an
assertion A, we can build a new program \Pi 0 by putting together \Pi, the computation of B and
the assertion assert A, considering the result of B to be the only output of \Pi 0 (see Fig. 4). The
problem thus reduces to proving that the only boolean output of \Pi 0 is always true during any
execution of the program which permanently satisfies the assertion assert A.
assert A
ok

Figure

4: Building a verification program
The verification is performed on a finite state abstraction of the program. Any numerical
computation is deliberately ignored, and boolean expressions depending on numerical variables
(e.g., comparisons) are considered non deterministic. However, assertions can be used again to
restrict this non determinism: For instance, if tests on conditions "X!Y", "Y!Z" and "X!Z" appear
in the program, the assertion "implies(X!Y and Y!Z, X!Z)" will prevent the prover to consider
absurd cases corresponding to "X!Y!Z" and "X-Z".
So, we consider a purely boolean, non deterministic program \Pi 00 , which approximates \Pi 0 in
the sense that "it has more behaviors": Any execution trace of \Pi 0 is also an execution trace of \Pi 00 .
Therefore, if the output of \Pi 00 is always true so is the output of \Pi 0 (Notice that, if the property
depends on the values of numerical variables, our tool may fail in proving it). Now, since \Pi 00
only contains boolean variables, it represents a finite state machine, on which any verification
problem is decidable: proving that its output is always true amounts to enumerate its finite set
of states, checking that, in each state - belonging to a path starting from the initial state and
on which the assertions are always true - and for each input vector, the output evaluates to
true. Two "verification engines" have been implemented and integrated into a verification tool,
called
ffl The first one explicitly enumerates the reachable states, as done by standard "model check-
ers" [12, 27]. The main limitation of such an approach is obviously the number of states
that can be considered. The present version of the tool deals with programs of about
1,000,000 states in reasonable time (less than 1 hour).
ffl The second engine proceeds symbolically: starting from a boolean formula F 0 , characterizing
the set of states where the output is true (in Lustre this formula is the expression
of the property), it iteratively computes a sequence F 1
characterizes the set of states, belonging to F i and necessarily leading (in one execution
step) into F i . As soon as the initial state doesn't satisfy F i , one can conclude that the
property is not satisfied, since there exists an execution path leading to a state where the
output is false. Otherwise, since the state space is finite, the sequence of formulas converges
after a finite number of steps to a formula F which characterizes the set of states
from which it is not possible to reach a state violating the property. Our tool performs
computations over formulas using binary decision diagrams ("BDDs" [9]), a compact
canonical encoding of boolean formulas. This approach is sometimes called "symbolic
model checking" [10, 14, 15].
The two approaches are complementary: in some cases, the enumerative method is cheaper
than the symbolic one, and conversely. The main limitation of the enumerative method is the
number of reachable states which must be considered, whereas the symbolic method is limited by
the complexity of boolean formulas (the size of the BDDs encoding it). Now, the complexity of
node UMS verif(on A,on B,on C, ack AB,ack BC: bool)
returns(property: bool);
var
grant access,grant exit: bool;
do AB,do BC: bool;
no collision,exclusive req: bool;
no derail AB,no derail BC: bool;
empty section, only on B: bool;
let
empty section = not(on A or on B or on C);
only on B = on B and not(on A or on C);
assert not(ack AB and ack BC);
assert always from to(ack AB,ack AB,do BC)
and always from to(ack BC,ack BC,do AB);
assert empty section -? true;
assert true -? implies(edge(not empty section), pre grant access);
assert true -? implies(edge(on C), pre grant exit);
assert implies(edge(not on A),on B);
assert implies(edge(not on B), on A or on C);
(grant access,grant exit,do AB,do
UMS(on A,on B,on C,ack AB,ack BC);
no
exclusive do BC);
no derail always from to(ack AB, grant access, only on B);
no derail always from to(ack BC, grant exit, empty section);
no collision and exclusive req and no derail AB
and no derail BC;
tel

Figure

5: The verification program
a boolean formula is not related with the number of states it characterizes: The formula "true"
can represent billions states!.
The program provided to Lesar for dealing with our example is listed in Fig. 5. The times
(in sec., on SUN4) needed for proving its properties (separately and globally) using each method
are gathered in the table below:
Property States Enum Symb
no collision 27 0.7 0.3
exclusive req 27 0.7 0.4
no derail AB 37 1.0 0.5
no derail
property 54 1.2 1.3
Of course, the example is so simple that these results are hardly meaningful. However, we
have treated more significant programs: In particular, the experience driven in [17] deals with
a real nuclear plant control system; all the critical properties required of this system have been
expressed (so, they were all safety properties) and verified using Lesar, in spite of the fact that
this example involves a lot of real-valued variables. As a matter of fact, these variables only
appeared in the properties by means of threshold comparisons, which have been handled using
assertions.
8 Modular verification
The fact that program and properties are expressed in the same language, together with the
assertion mechanism provide also a method for modular verification: Informally, given a program
\Pi compound of n subprograms once each \Pi i has been proved to satisfy a
safety property P i one can prove that \Pi satisfies a safety property P by proving
that the combination of the P i implies P . More formally, if we note "\Pi the fact that the
program \Pi satisfies the safety property P , and if jj denotes the parallel composition, we have
This can be done in Lustre in the following way: Let \Pi be a program using some node \Pi 0
(Fig. 6.a). Assume that \Pi 0 has been proved to satisfy a property P 0 , expressed by the invariance
(a) (b)

Figure

Modular verification
A

Figure

7: A full subway track
of the boolean expression B. Now, for proving that \Pi satisfies a property P , one can consider \Pi
as a part of the environment of \Pi, replacing it by the assertion that B is always true (Fig. 6.b).
Formally, if we note "2B" the property that B is always true,
Of course, the property P 0 (which must be found by intuition) may be too weak to allow the
proof of P , but such a decomposition may drastically reduce the complexity of the verification.
For instance, the proved properties of the UMS system could be used for verifying the control
of a whole subway track (Fig. 7): Informally, let LINEAR TRACKX be a Lustre program controlling
a single track X , and UMSX;Y be the controller of a UMS with input track X and output
track Y , the structure of the whole program would be
LINEAR TRACKA jj UMS A;C jj LINEAR TRACKC jj UMS C;A
Instead of considering this whole program, one could try to verify the following (hopefully)
simpler one
where BX;Y denotes the boolean expression which has been proved to be invariantly true in the
program UMSX;Y .
Moreover, this approach has been extended in [19] to allow the inductive verification of regular
networks of identical processes. Modular verification also allows the verification of partially
developed programs: Using the same approach in a slightly different way, you can verify the
properties of a program \Pi before writing a sub-program \Pi 0 , using a specification of \Pi 0 .
9 Conclusion and future work
We have tried to highlight the advantages of using a synchronous data-flow language in designing
a real-time program. These advantages are twofold: On one hand, such a language meets
traditional tools used in this field, and on the other hand, since it can be viewed as an executable
temporal logic, it allows the expression of specifications and the smooth merging of programs
and properties.
The synchronous hypothesis relegates "real-time" problems to the evaluation of program
reaction time. Under this hypothesis, a program can be modeled by standard transition systems.
As a consequence, our approach to program verification is quite standard, and even rather
restricted, since it only deals with checking safety properties on finite state program abstractions.
These restrictions have been introduced in order to tackle real-life problems, and we have argued
that they meet many practical cases. Notice that, in contrast with many verification tools which
deal with models of programs, our tools apply directly to programs themselves, thus meeting
G. Berry's ``WYPIWYE'' principle [4]: What you prove is what you execute! There is no manual
transformation between the program which is verified and the code which is executed.
Of course, both programming and verification rely on the synchronous hypothesis. This
hypothesis must be checked in fine for the results to be valid. However, this checking only
consists in evaluating the maximum execution time of linear pieces of code (the reactions), and
is therefore easy.
This work will be pursued, at least in two directions:
ffl The restriction to boolean abstractions is a strong limitation. Dealing with some properties
about bounded integers would certainly be worthwhile. In particular, integer variables are
often used in Lustre to count delays. Up to now, our tools are not aware that a delay of
3 seconds is shorter that one of 10 seconds! Recent works on timed graph analysis [1, 16]
could be adapted for that.
ffl A lot of work remains to be done around modular verification and program synthesis.
In the approach proposed in x8, the specification of a subprogram must be provided by
intuition. It would be appealing to synthesize automatically this specification, using our
verification tool: Assume a program \Pi, calling a sub-program \Pi 0 , is required to
satisfy a property P , i.e., the invariance of some boolean expression B. We can first remove
\Pi 0 from \Pi, considering it as an unknown part of \Pi's environment. If the resulting program
satisfies P , then \Pi 0 has nothing to do with P . Otherwise, the symbolic verifier exhibits
a formula F which characterizes the set of states of the program in which B is false. The
role of \Pi 0 is then to avoid these states. The idea is to extract from F a specification of
\Pi 0 . Moreover, since in our approach, specifications are programs, one can wonder if it is
possible to synthesize \Pi 0 from this specification.



--R

Model checking of real-time systems
Lucid, the data-flow programming language
The synchronous approach to reactive and real-time systems
Real time programming: Special purpose or general purpose languages.
Synchronous programming of reactive systems
The Esterel synchronous programming language: Design
On the verification of safety properties.
The Esterel language.

Symbolic model check- ing: 10 20 states and beyond
Lustre: a declarative language for programming synchronous systems.
Automatic verification of finite-state concurrent systems using temporal logic specifications
A language for compositional specification and verification of finite state hardware controllers.
Verification of synchronous sequential machines based on symbolic execution.
Verifying temporal properties of sequential machines without building their state diagrams.
Timing assumptions and verification of finite state concurrent systems.
V'erification de propri'et'es de programmes flots de donn'ees synchrones.
The synchronous dataflow programming language Lustre.
An experience in proving regular networks of processes by modular model checking.
Generating efficient code from data-flow pro- grams
A visual approach to complex systems.
On limits and possibilities of automated protocols analysis.
The semantics of a simple language for parallel programming.
Programming real time applications with Signal.
The glory of the past.
Automated verification of timed transition systems.
Specification and verification of concurrent systems in Cesar.
Programming and verifying critical systems by means of the synchronous data-flow programming language Lustre
Verification in xesar of the sliding window protocol.
--TR
LUCID, the dataflow programming language
Automatic verification of finite-state concurrent systems using temporal logic specifications
Graph-based algorithms for Boolean function manipulation
Statecharts: A visual formalism for complex systems
LUSTRE: a declarative language for real-time programming
Synchronous programming of reactive systems: an introduction to ESTEREL
Timing assumptions and verification of finite-state concurrent systems
Verification of synchronous sequential machines based on symbolic execution
Programming and verifying critical systems by means of the synchronous data-flow language LUSTRE
On Limits and Possibilities of Automated Protocol Analysis
Verification in XESAR of the Sliding Window Protocol
Automated Verification of Timed Transition Models
Specification and verification of concurrent systems in CESAR
Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams
The Glory of the Past

--CTR
Bruno d'Ausbourg, Synthtiser I'intention d'un pilote pour Dfinir de nou-veaux quipements de bord, Proceedings of the 14th French-speaking conference on Human-computer interaction (Confrence Francophone sur l'Interaction Homme-Machine), p.145-152, November 26-29, 2002, Poitiers, France
Paul Amblard , Fabienne Lagnier , Michel Levy, Introduction to formal processor verification at logic level: a case study, Proceedings of the 2004 workshop on Computer architecture education: held in conjunction with the 31st International Symposium on Computer Architecture, June 19, 2004, Munich, Germany
Vered Gafni, Robots: a real-time systems architectural style, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.57-74, Nov. 1999
Dominique L'Her , Philippe Le Parc , Lionel Marc, Proving sequential function chart programs using timed automata, Theoretical Computer Science, v.267 n.1-2, p.141-155, 09/26/2001
Abdesselam Lakehal , Ioannis Parissis, Automated Measure of Structural Coverage for LUSTRE Programs: a Case Study, Proceedings of the Second International Workshop on Automation of Software Test, p.12, May 20-26, 2007
Tarvo Raudvere , Ingo Sander , Axel Jantsch, A synchronization algorithm for local temporal refinements in perfectly synchronous models with nested feedback loops, Proceedings of the 17th great lakes symposium on Great lakes symposium on VLSI, March 11-13, 2007, Stresa-Lago Maggiore, Italy
Y. Ait-Ameur , G. Bel , F. Boniol , S. Pairault , V. Wiels, Robustness analysis of avionics embedded systems, ACM SIGPLAN Notices, v.38 n.7, July
Tarvo Raudvere , Ingo Sander , Ashish Kumar Singh , Axel Jantsch, Verification of design decisions in ForSyDe, Proceedings of the 1st IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis, October 01-03, 2003, Newport Beach, CA, USA
Ioannis Parissis , Farid Ouabdesselam, Specification-based testing of synchronous software, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.127-134, Nov. 1996
Florence Maraninchi , Yann Rmond, Mode-automata: a new domain-specific construct for the development of safe critical systems, Science of Computer Programming, v.46 n.3, p.219-254, March
K. Altisen , F. Maraninchi , D. Stauch, Aspect-oriented programming for reactive systems: Larissa, a proposal in the synchronous framework, Science of Computer Programming, v.63 n.3, p.297-320, 15 December 2006
Ralph D. Jeffords , Constance L. Heitmeyer, A strategy for efficiently verifying requirements, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September
Axel Poign , Matthew Morley , Olivier Maffes , Leszek Holenderski , Reinhard Budde, The Synchronous Approach to Designing Reactive Systems, Formal Methods in System Design, v.12 n.2, p.163-187, March 1, 1998
Hahnsang Kim , Thierry Turletti , Amar Bouali, EPspectra: a formal toolkit for developing DSP software applications, Theory and Practice of Logic Programming, v.6 n.4, p.451-481, July 2006
Bruno d'Ausbourg , Christel Seguin , Guy Durrieu , Pierre Roch, Helping the automated validation process of user interfaces systems, Proceedings of the 20th international conference on Software engineering, p.219-228, April 19-25, 1998, Kyoto, Japan
Ludovic Samper , Florence Maraninchi , Laurent Mounier , Louis Mandel, GLONEMO: global and accurate formal models for the analysis of ad-hoc sensor networks, Proceedings of the first international conference on Integrated internet ad hoc and sensor networks, May 30-31, 2006, Nice, France
Mary Sheeran , Gunnar Stlmarck, A Tutorial on Stlmarcks Proof Procedure for PropositionalLogic, Formal Methods in System Design, v.16 n.1, p.23-58, Jan 1,2000
Angelo Gargantini , Angelo Morzenti, Automated deductive requirements analysis of critical systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.10 n.3, p.255-307, July 2001
Paul Caspi , Alain Girault , Daniel Pilaud, Automatic Distribution of Reactive Systems for Asynchronous Networks of Processors, IEEE Transactions on Software Engineering, v.25 n.3, p.416-427, May 1999
U. Buy , R. H. Sloan, Automatic Real-Time Analysis of Reactive Systems with the PARTS Toolset, Automated Software Engineering, v.8 n.3-4, p.227-273, August 2001
Alberto Coen-Porisini , Carlo Ghezzi , Richard A. Kemmerer, Specification of realtime systems using ASTRAL, IEEE Transactions on Software Engineering, v.23 n.9, p.572-598, September 1997
parallel languages;dataflow approach;real-time systems;formal design;program verification;critical real-time systems;verification tool LESAR;verification methods;parallel programming;synchronous data-flow language;traditional description tools;ergonomy;data-flow language LUSTRE;critical properties