Verifying Progress in Timed Systems
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.
Unable to display preview. Download preview PDF.
- [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.Google Scholar
- [BS97]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.Google Scholar
- [BST98]S. Bornot, J. Sifakis, and S. Tripakis. Modeling urgency in timed systems. In Compositionality, LNCS 1536, 1998. To appear.Google Scholar
- [Daw98]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.Google Scholar
- [DT98]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.Google Scholar
- [Oli94]A. Olivero. Modélisation et analyse de systèmes temporisés et hybrides. PhD thesis, Institut National Polytechnique de Grenoble, 1994. In french.Google Scholar
- [SY96]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.Google Scholar
- [Tri98]S. Tripakis. The formal analysis of timed systems in practice. PhD thesis, Université Joseph Fourrier de Grenoble, 1998. To be published.Google Scholar
- [Yov93]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.Google Scholar