Skip to main content

How to stop time stopping

Bowman, Howard, Gomez, Rodolfo (2006) How to stop time stopping. Formal Aspects of Computing, 18 (4). pp. 459-493. ISSN 0934-5043. (doi:10.1007/s00165-006-0010-7) (KAR id:14388)

Language: English
Click to download this file (462kB) Preview
[thumbnail of main.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


Zeno-timelocks constitute a challenge for the formal verification of timed automata: they are difficult to detect, and the verification of most properties (e.g., safety) is only correct for timelock-free models. Some time ago, Tripakis proposed a syntactic check on the structure of timed automata: If a certain condition (called strong non-zenoness) is met by all the loops in a given automaton, then zeno-timelocks are guaranteed not to occur. Checking for strong non-zenoness is efficient, and compositional (if all components in a network of automata are strongly non-zeno, then the network is free from zeno-timelocks). Strong non-zenoness, however, is sufficient-only: There exist non-zeno specifications which are not strongly non-zeno. A TCTL formula is known that represents a sufficient-and-necessary condition for non-zenoness; unfortunately, this formula requires a demanding model-checking algorithm, and not all model-checkers are able to express it. In addition, this algorithm provides only limited diagnostic information. Here we propose a number of alternative solutions. First, we show that the compositional application of strong non-zenoness can be weakened: Some networks can be guaranteed to be free from Zeno-timelocks, even if not every component is strongly non-zeno. Secondly, we present new syntactic, sufficient-only conditions that complement strong non-zenoness. Finally, we describe a sufficient-and-necessary condition that only requires a simple form of reachability analysis. Furthermore, our conditions identify the cause of zeno-timelocks directly on the model, in the form of unsafe loops. We also comment on a tool that we have developed, which implements the syntactic checks on Uppaal models. The tool is also able to derive, from those unsafe loops in a given automaton (in general, an Uppaal model representing a product automaton of a given network), the reachability formulas that characterise the occurrence of zeno-timelocks. A modified version of the CSMA/CD protocol is used as a case-study.

Item Type: Article
DOI/Identification number: 10.1007/s00165-006-0010-7
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:03 UTC
Last Modified: 09 Mar 2023 11:29 UTC
Resource URI: (The current URI for this page, for reference purposes)
Bowman, Howard:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.