School of Computing

How to stop time stopping (preliminary version)

Howard Bowman, Rodolfo Gomez, and Li Su

Technical Report 9-04, University of Kent, Computing Laboratory, Canterbury, Kent, CT2 7NF, UK, May 2004.

Abstract

Timed automata are a very successful notation for specifying and verifying real-time systems. One problem of the approach though is that 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. This means, in fact, that the entire system stops. We identify a number of different types of timelocks and argue that each type should be treated differently. We distinguish between time-actionlocks and zeno-timelocks and argue that a constructive approach should be applied to preventing the former of these, while an analytical approach should be used to prevent the latter. In accordance with this position, we present a revision of the interpretation of parallel composition in timed automata in order to prevent time-actionlocks. With respect to zeno-timelocks, we present an analytical method to ensure absence of zeno-timelocks which builds upon the notion of strong non-zenoness introduced by Tripakis. We show how Tripakis' results can be extended, broadening the class of timed automata specifications which can be guaranteed to be free from zeno-timelocks. Moreover, we present a tool that we have developed which implements this syntactic verification on UPPAAL-like timed automata specifications. Also, new syntactic properties, in the spirit of strong non-zenoness, are presented which also ensure zeno-timelock freedom. Finally, we illustrate the use of the tool on a real-life case study, the CSMA/CD protocol.

Download publication 281 kbytes (PDF)

Bibtex Record

@techreport{1915,
author = {Howard Bowman and Rodolfo Gomez and Li Su},
title = {How to stop time stopping (preliminary version)},
month = {May},
year = {2004},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2004/1915},
    publication_type = {techreport},
    submission_id = {7989_1084802696},
    number = {9-04},
    address = {Canterbury, Kent, CT2 7NF, UK},
    institution = {University of Kent, Computing Laboratory},
}

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

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

Last Updated: 21/03/2014