School of Computing

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

H. Bowman, R. Gomez, and L. Su

In Proceedings of the 6th AMAST Workshop on Real-Time Systems, pages 182-196, Stirling, Scotland, July 2004. Elsevier To be published in ENTCS.

Abstract

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.

Download publication 216 kbytes

Bibtex Record

@inproceedings{1934,
author = {H. Bowman and R. Gomez and L. Su},
title = {A tool for the syntactic detection of zeno-timelocks in timed automata},
month = {July},
year = {2004},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {To be published in ENTCS},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2004/1934},
    booktitle = {Proceedings of the 6th AMAST Workshop on Real-Time Systems},
    submission_id = {21671_1088080062},
    address = {Stirling, Scotland},
    refereed = {yes},
    publisher = {Elsevier},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014