Abstract
Time and action locks can arise freely in timed automata specification. We review techniques for avoiding the occurrence of timelocks, based on the Timed Automata with Deadlines framework. Then we present a notion of parallel composition which preserves action lock freeness, in the sense that, if any component automaton is action lock free, then the composition will also be action lock free.
Chapter PDF
Similar content being viewed by others
References
Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, and Paul Pettersson amd Wang Yi. Uppaal-a tool suite for automatic verification of real-time system. In Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, 1995.
S. Bornot and J. Sifakis. On the composition of hybrid systems. In Hybrid Systems: Computation and Control, LNCS 1386, pages 49–63, 1998.
S. Bornot, J. Sifakis, and S. Tripakis. Modeling urgency in timed systems. In Compositionality, COMPOS’97, LNCS 1536, 1997.
H. Bowman. Modelling timeouts without timelocks. In ARTS’99, Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop, LNCS 1601, pages 335–353. Springer-Verlag, 1999.
H. Bowman. On time and action lock free description of timed systems. Technical Report 16-99, Computing Laboratory, University of Kent at Canterbury, 1999. available at http://www.cs.ukc.ac.uk/people/staff/hb5/pubs.local.
H. Bowman, G. Faconti, J-P. Katoen, D. Latella, and M. Massink. Automatic verification of a lip synchronisation algorithm using UPPAAL. Formal Aspects of Computing, 10(5–6):550–575, August 1998.
C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, Verification and Control, LNCS 1066. Springer-Verlag, 1996.
T. Regan. Multimedia in temporal LOTOS: A lip synchronisation algorithm. In PSTV XIII, 13th Protocol Spec., Testing & Verification. North-Holland, 1993.
S. Tripakis. Verifying progress in timed systems. In ARTS’99, Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop, LNCS 1601. Springer-Verlag, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 IFIP International Federation for Information Processing
About this paper
Cite this paper
Bowman, H. (2001). Time and Action Lock Freedom Properties for Timed Automata. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds) Formal Techniques for Networked and Distributed Systems. FORTE 2001. IFIP International Federation for Information Processing, vol 69. Springer, Boston, MA. https://doi.org/10.1007/0-306-47003-9_8
Download citation
DOI: https://doi.org/10.1007/0-306-47003-9_8
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-7923-7470-1
Online ISBN: 978-0-306-47003-5
eBook Packages: Springer Book Archive