We aim to
develop and implement efficient algorithms to enhance the functionality of
model-checkers for timed automata networks (Alur
& Dill, 1994) (Henzinger, Nicollin, Sifakis, & Yovine, 1994), to
offer better support for the prevention and detection of anomalous behaviours
(namely, Zeno runs and timelocks), and more expressive requirements languages.
More specifically, we propose to develop a number of front-end tools for the
widely-used model-checker Uppaal (Behrmann, David, & Larsen, 2004).
Zeno runs and timelocks. Zeno runs denote infinite
executions with finite accumulated delay, and typically occur in cycles in the
model that do not enforce minimum delays between consecutive iterations.
Timelocks are states where all subsequent executions occur with finite
accumulated delay, and typically occur due to mismatched synchronisation of
urgent actions. In general, models with Zeno runs or timelocks cannot be
reliably verified, as such behaviours may prevent the model-checker from
exploring the complete state space. Although, both the absence of Zeno runs and
the absence of timelocks can be expressed by suitable liveness properties,
these properties are difficult to verify (demanding substantial memory and time
to complete) and do not scale up (for instance, the verification of liveness
properties in Uppaal cannot benefit from symmetry reduction).
We propose
alternative methods to check for absence of Zeno runs that do not rely on
liveness properties. This is based on the observation that, often in practice,
the absence of Zeno runs is implied by the existence of suitable clock constraints
and resets in cycles of the model (namely, the strong non-Zenoness property (Tripakis,
1999)), and by the possible synchronisations among cycles (Bowman & Gomez, 2006).
We will also
investigate how to integrate the semantics of Timed Automata with Deadlines
(TAD) (Bornot, Sifakis, & Tripakis, 1998)
(Bowman, 2001) with that of timed safety automata (Henzinger, Nicollin, Sifakis, & Yovine, 1994)
(i.e., time automata with invariants). TAD allow urgent actions to be expressed
more naturally than in timed safety automata, and their semantics prevents the
occurrence of the most common form of timelocks (simple restrictions on clock
constraints ensure that TAD models are time-reactive,
that is, from any state, either actions or delays are possible). Our goal,
then, is to obtain more reliable timed automata models, with a more robust
support for urgent actions, without sacrificing the efficiency of verification
algorithms for timed safety automata.
Expressive requirements languages. We propose an
extention of Uppaal’s requirements language (a subset of TCTL) with a chop-like
operator as found in interval temporal logics such as ITL (Moszkowski, 1986) or Duration Calculus (Chaochen, Hoare, & Ravn, 1991). The chop
operator, which is akin to concatenation in regular expressions, offers a
simple way to denote sequential composition of behaviours, and would bring the
requirements language one step closer to the expressive power of regular
languages. This is important, as it has been recognized that regular logics
facilitate the description of correctness properties (Vardi, 2001), and therefore reduce validation errors and make
verification more reliable.
The project
will explore the so called test automata
as a vehicle to verify chop-based properties in Uppaal. Test automata are timed
automata with a particular structure, derived from a class of correctness
properties that cannot be directly expressed in Uppaal’s requirements language.
Test automata have a distinguished location, such that a model is guaranteed to
satisfy the correctness property if and only if this location is unreachable in
the parallel composition of the model with the test automaton. We will probe the limits of test automata to
characterize formulas with chop; while it is likely that the full power of
regular expressions cannot be preserved, we will able to benefit directly from
Uppaal’s efficient reachability analysis. This research will be inspired in
previous works on the expressiveness of test automata (Aceto, Bouyer, Burgueño, & Larsen, 2003) and on practical
automata-theoretic decision procedures for interval temporal logics (Pandya, 2002) (Gomez & Bowman, 2004).
Rodolfo Gomez
(principal investigator)
Howard Bowman
(advisor)
Kim G. Larsen
(collaborator)
Frits Vaandrager
(collaborator)
Tools
LIDLmd2TA : A tool to verify interval temporal logic
properties on Uppaal networks.
TAD2TA : A tool to translate Timed Automata with Deadlines
(TAD) to Uppaal networks.
ZC : A tool to detect all possible sources of Zeno behaviour
in Uppaal networks.
Publications
A
Compositional Translation of Timed Automata with Deadlines to Uppaal Timed
Automata. R. Gomez. In Proc. of the 7th Int. Conf. on Formal Modelling
and Analysis of Timed Systems (FORMATS'09), 14-16 September, Budapest, Hungary,
LNCS 5813, pages 179-194. Springer, 2009.
Compositional
Detection of Zeno behavior in Timed Automata with Deadlines. R. Gomez.
Technical report 3-09, Computing Laboratory, University of Kent, June 2009.
From LIDL(m)
to Timed Automata. R. Gomez. Technical Report 2-09, Computing Laboratory,
University of Kent, April 2009.
Verification
of Timed Automata with Deadlines in Uppaal. R. Gomez. Technical Report
2-08, Computing Laboratory, University of Kent, June 2008.
Efficient Detection
of Zeno Runs in Timed Automata. R. Gomez and H. Bowman. In J.-F. Raskin and
P.S. Thiagarajan, editors, 5th International Conference FORMATS 2007
(Formal Modelling and Analysis of Timed Systems), volume 4763 of LNCS,
pages 195-210,
Compositional
Detection of Zeno behaviour in Timed Automata. R. Gomez and H. Bowman.
Technical Report 12-06, Computing Laboratory, University of Kent, December
2006.
Aceto, L., Bouyer,
P., Burgueño, A., & Larsen, K. (2003). The power of reachability testing
for timed automata. Theoretical Computer Science , 300 (1-3),
411-475.
Alur,
R., & Dill, D. (1994). A theory of timed automata. Theoretical
Computer Science , 126, 183-235.
Behrmann,
G., David, A., & Larsen, K. G. (2004). A tutorial on Uppaal. Formal
methods for the design of real-time systems (SFM-RT 2004). LNCS 3185,
pp. 200-236. Bertinoro, Italy: Springer.
Bornot,
S., Sifakis, J., & Tripakis, S. (1998). Modelling urgency in timed
systems. Compositionality: The Significant Difference (COMPOS' 97). LNCS
1536, pp. 103-129. Bad Malente, Germany: Springer.
Bowman,
H. (2001). Time and action-lock freedom properties for timed automata. Formal
Techniques for Networked and Distributed Systems (FORTE '01) (pp.
119-134). Cheju Island, Korea: Kluwer Academic Publishers.
Bowman,
H., & Gomez, R. (2006). How to stop time stopping. Formal Aspects of
Computing , 18 (4), 459-493.
Bozga,
M., Graf, S., Ober, I., Ober, I., & Sifakis, J. (2004). The IF toolset. Formal
methods for the design of real-time systems (SFM-RT 2004). LNCS 3185,
pp. 237-267. Bertinoro, Italy: Springer.
Chaochen,
Z., Hoare, C. A., & Ravn, A. P. (1991). A Calculus of Durations. Information
Processing Letters , 40 (5), 269–276.
Gomez,
R., & Bowman, H. (2004). PITL2MONA: Implementing a decision procedure for
Propositional Interval Temporal Logic. Journal of applied non-classical
logics , 14 (1-2), 105-148.
Henzinger,
T., Nicollin, X., Sifakis, J., & Yovine, S. (1994). Symbolic Model
Checking for Real-time Systems. Information and Computation , 111
(2), 193-244.
Moszkowski,
B. (1986). Executing temporal logic programs. Cambridge University
Press.
Pandya,
P. (2002). Interval Duration Logic: Expressiveness and Decidability. Theory
and Practice of Timed Systems (Electronic Notes in Theoretical Computer
Science 65(2)).
Tripakis,
S. (1999). Verifying time progress in timed systems. ARTS'99 , LNCS
1601, pp. 299-314.
Vardi,
M. (2001). Branching time vs Linear time: The final showdown. TACAS'01
, LNCS 2031, pp. 1-22.