Bug in the forward analysis of timed automata
| Abstract: Timed automata are a
widely studied model for real-time systems. Since 8 years, numerous
tools implement this model and are successfully used to verify
real-life examples. In spite of this well-established framework, we
prove the usual forward analysis algorithm is not correct for the
whole class of timed automata. Nevertheless, we also prove that the
algorithm is correct for large subclasses of timed automata which
contain in particular all the timed automata which do not compare two
clocks. This work has been published
as [Bou03]
and
in [Bou04]. |
Forward Analysis for Timed Automata
-
The exact computation of Post* does not terminate: necessity of an
abstraction operator "abs"
-
Several criteria for choosing "abs":
-
[termination] the computation of
(abs o Post)* terminates
-
[soundness] (abs o Post)* is correct w.r.t.
reachability
-
[effectiveness] the computation of
"abs" is easy and efficient (maybe
a subjective criterium)
-
Possible and usual translation for timed automata:
|
|
[effectiveness]
|
|
|
[termination]
|
- zone is included in abs(zone) and abs(zone) is included in the closure of
zone w.r.t. the set of regions associated to the timed
automaton (cf the original article [AD94])
|
[soundness]
|
These three criteria will be denoted as the TA-forward-analysis criteria.
(*) a zone is a set of valuations, defined by
constraints of the form x # c and x-y #c where
x and y are clocks and c is a
constant.
-
The abstraction operator that has been used in numerous tools is the
following extrapolation operator:
abs(Z) = smallest zone containing Z
and defined by k-bounded constraints
where
k is a constant, depending on the automaton. This
abstraction operator is called the k-extrapolation. It obviously meets
the two first conditions of the TA-forward-analysis criteria.
The "buggy" automaton
Consider the following automaton:
If
d is the date the first transition is taken, the valuation
which is reached in
q after having taken
n times the
loop on the right is
v such that:
|
v(x1) = 0
|
v(x3) = 2n+5
|
|
v(x2) = d
|
v(x4) = d+2n+5
|
We can thus represent the reachable zone in
q after
n
loops by the following picture:
Fixing a constant
k, and taking
n such that
2n+2 >
k, the extrapolation of the previous zone can be depicted as:
In particular, if we use the
k-extrapolation, state "Error"
becomes reachable.
| For the previous automaton, there is no constant k
such that the k-extrapolation meets the soundness criterium. |
As a simple corollary, we get that there is no abstraction operator
abs that meets the
TA-forward-analysis criteria.
Notes and some conclusions
The problem comes from the use of diagonal constraints of the type
x-y # c. For diagonal-free timed automata,
i.e. those
automata that only use constraints of the type
x#c, the
k-extrapolation is a correct abstraction for the forward
analysis, where
k is choosen as the maximal constant used in
the
automaton. See
[Bou02]
(the research report corresponding
to
[Bou03])
or
[Bou04]
for a first proof,
or
[BBFL03]
for a second proof).
In the general case, the forward analysis algorithm which uses the
k-extrapolation as an abstraction operator is surprisingly
incorrect. As a side-effect, this implies in addition that there is no
abstraction operator
on zones (
i.e. roughly which meets
the
TA-forward-analysis criteria) which is
correct for a forward analysis. Work is now needed to propose new
correct abstractions...
Recently we have proposed a refinement-based method for verifying
timed automata using diagonal constraints,
see
[BLR05].
This method is going implemented in the
tool
Uppaal
by
Pierre-Alain
Reynier.
Bibliography
|
[AD94]
|
Rajeev Alur and David Dill. A Theory of Timed Automata.
Theoretical Computed Science 126(2), pages 183-225, 1994.
|
|
[BBFL03]
|
Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury and Kim G. Larsen.
Static Guard Analysis in Timed Automata Verification. In
Proc. 9th Int. Conf. Tools and Algorithms for the Construction and
Analysis of Systems (TACAS'2003), vol. 2619 of LNCS, pp. 254--277.
Springer, 2003.
|
|
[BLR05]
|
Patricia Bouyer, François Laroussinie and Pierre-Alain Reynier.
Diagonal Constraints in Timed Automata - Forward Analysis of
Timed Systems. In Proceedings of the 3rd International
Conference on Formal Modelling and Analysis of Timed Systems
(FORMATS'05), Uppsala, Sweden, September-October 2005,
LNCS. Springer. To appear.
|
|
[Bou02]
|
Patricia Bouyer. Timed Automata May Cause Some Troubles.
Research Report LSV-02-9, Laboratoire Spécification et
Vérification, CNRS UMR 8643 & École Normale Supérieure de Cachan,
2002.
|
|
[Bou03]
|
Patricia Bouyer. Untameable Timed Automata! In Proc. 20th
Ann. Symp. Theoretical Aspects of Computer Science (STACS'2003), vol.
2607 of LNCS, pp. 620-631. Springer, 2003.
|
|
[Bou04]
|
Patricia Bouyer. Forward Analysis of Updatable Timed
Automata. Formal Methods in System Design 24(3), pages
281-320, 2004.
|