How to stop time stopping

Bowman, Howard and Gomez, Rodolfo (2006) How to stop time stopping. Formal Aspects of Computing, 18 (4). pp. 459-493. ISSN 0934-5043. (Full text available)

Download (437kB) Preview


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
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Computational Intelligence Group
Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:03 UTC
Last Modified: 12 May 2014 13:40 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year