Skip to main content

A tool for the syntactic detection of zeno-timelocks in timed automata

Bowman, Howard, Gomez, Rodolfo, Su, Linying (2005) A tool for the syntactic detection of zeno-timelocks in timed automata. Electronic Notes in Theoretical Computer Science, 139 (1). pp. 25-47. ISSN 1571-0661. (doi:10.1016/j.entcs.2005.09.006) (KAR id:14234)

Language: English
Download (317kB) Preview
[thumbnail of BowmanGS05.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


Timed automata are a very successful notation for specifying and verifying real-time systems, but timelocks can freely arise. These are counter-intuitive situations in which a specifier's description of a component automaton can inadvertently prevent time from passing beyond a certain point, possibly making the entire system stop. In particular, a zeno-timelock represents a situation where infinite computation is performed in a finite period of time. Zeno-timelocks are very hard to detect for real-time model checkers, e.g. UPPAAL and Kronos. We have developed a tool which can take an UPPAAL model as input and return a number of loops which can potentially cause zeno-timelocks. This tool implements an algorithm which refines a static verification approach introduced by Tripakis. We illustrate the use of this tool on a real-life case-study, the CSMA/CD protocol.

Item Type: Article
DOI/Identification number: 10.1016/j.entcs.2005.09.006
Additional information: Proceedings of the 6th AMAST Workshop on Real-time Systems (ARTS 2004)
Uncontrolled keywords: Timed Automata; Zeno-timelocks; UPPAAL
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:02 UTC
Last Modified: 16 Nov 2021 09:52 UTC
Resource URI: (The current URI for this page, for reference purposes)
Bowman, Howard:
  • Depositors only (login required):


Downloads per month over past year