How to stop time stopping

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

PDF
Download (429kB)
[img]
Preview

Abstract

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 > Science Technology and Medical Studies > School of Computing > Computational Intelligence Group
Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:03
Last Modified: 20 Apr 2012 11:42
Resource URI: http://kar.kent.ac.uk/id/eprint/14388 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year