How to stop time stopping (preliminary version)

Bowman, Howard and Gomez, Rodolfo and Su, Li (2004) How to stop time stopping (preliminary version). Technical report. University of Kent, Canterbury, Kent, CT2 7NF, UK (Full text available)

PDF
Download (288kB)
[img]
Preview

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.

Item Type: Monograph (Technical report)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:02
Last Modified: 12 May 2014 13:56
Resource URI: http://kar.kent.ac.uk/id/eprint/14161 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year