Abstract
In this paper we study the issue of progress for distributed timed systems modeled as the parallel composition of timed automata. We clarify the requirements of discrete progress (absence of deadlocks) and time progress (absence of deadlocks and timelocks) and give static sufficient conditions for a model of TA to be deadlock- and timelock-free. We also present dynamic techniques for deadlock and timelock detection. The techniques are based on forward symbolic reachability and are on-the-fly, that is, they can return an answer as soon as possible, without necessarily having to construct and store the whole state space.
This work has been done at Verimag. Currently, the author is at UC Berkeley as a post-doctoral scholar.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur, C. Courcoubetis, and D.L. Dill. Model checking in dense real time. Information and Computation, 104(1):2–34, 1993.
[BFK+98]_H. Bowman, G. Faconti, J-P. Katoen, D. Latella, and M. Massink. Automatic verification of a lip synchronisation algorithm using uppaal. In 3rd International Workshop on Formal Methods for Industrial Critical Systems, 1998.
S. Bornot and J. Sifakis. Relating time progress and deadlines in hybrid systems. In International Workshop, HART’97, pages 286–300, Grenoble, France, March 1997. Lecture Notes in Computer Science 1201, Spinger-Verlag.
S. Bornot, J. Sifakis, and S. Tripakis. Modeling urgency in timed systems. In Compositionality, LNCS 1536, 1998. To appear.
C. Daws. Méthodes d’analyse de systèmes temporisés: de la théorie à la pratique. PhD thesis, Institut National Polytechnique de Grenoble, 1998. In french.
D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, pages 197–212. Springer-Verlag, 1989.
C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Tools and Algorithms for the Construction and Analysis of Systems’ 98, Lisbon, Portugal, volume 1384 of LNCS. Springer-Verlag, 1998.
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.
A. Olivero. Modélisation et analyse de systèmes temporisés et hybrides. PhD thesis, Institut National Polytechnique de Grenoble, 1994. In french.
J. Sifakis and S. Yovine. Compositional specification of timed systems. In 13th Annual Symposium on Theoretical Aspects of Computer Science, STACS’96, pages 347–359, Grenoble, France, February 1996. Lecture Notes in Computer Science 1046, Spinger-Verlag.
S. Tripakis. The formal analysis of timed systems in practice. PhD thesis, Université Joseph Fourrier de Grenoble, 1998. To be published.
S. Yovine. Méthodes et outils pour la vérification symbolique de systèmes temporisés. PhD thesis, Institut National Polytechnique de Grenoble, 1993. In french.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tripakis, S. (1999). Verifying Progress in Timed Systems. In: Katoen, JP. (eds) Formal Methods for Real-Time and Probabilistic Systems. ARTS 1999. Lecture Notes in Computer Science, vol 1601. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48778-6_18
Download citation
DOI: https://doi.org/10.1007/3-540-48778-6_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66010-1
Online ISBN: 978-3-540-48778-4
eBook Packages: Springer Book Archive