Abstract
Uppaal is a new tool suit for automatic verification of networks of timed automata. In this paper we describe the diagnostic model-checking feature of Uppaal and illustrates its usefulness through the debugging of (a version of) the Philips Audio-Control Protocol. Together with a graphical interface of Uppaal this diagnostic feature allows for a number of errors to be more easily detected and corrected.
This work has been supported by the European Communieties (under CONCUR2 and REACT), NUTEK (Swedish Board for Technical Development) and TFR (Swedish Technical Research Council)
This author would also like to thank the Chinese NSF and the Hong Kong Wang's Foundation for supporting a visit to the Institute of Software, Chinese Academy of Sciences, in 1995.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur and D. Dill. Automata for Modelling Real-Time Systems. Theoretical Computer Science, 126(2):183–236, April 1994.
Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal—a Tool Suite for Automatic Verification of Real-Time Systems. In Proc. of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, Lecture Notes in Computer Science, October 1995.
D. Bosscher, I. Polak, and F. Vaandrager. Verification of an Audio-Control Protocol. In Proc. of FTRTFT'94, volume 863 of Lecture Notes in Computer Science, 1993.
Nicolas Halbwachs. Delay Analysis in Synchronous Programs. Lecture Notes in Computer Science, 697, 1993. In Proc. of CAV'93.
T. A. Henzinger, Z. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking for Real-Time Systems. In Logic in Computer Science, 1992.
Pei-Hsin Ho and Howard Wong-Toi. Automated Analysis of an Audio Control Protocol. In Proc. of CAV'95, volume 939 of Lecture Notes in Computer Science. Springer Verlag, 1995.
H. Hüttel and K. G. Larsen. The use of static constructs in a modal process logic. Lecture Notes in Computer Science, Springer Verlag, 363, 1989.
F. Laroussinie and K.G. Larsen. Compositional Model Checking of Real Time Systems. In Proc. of CONCUR'95, Lecture Notes in Computer Science. Springer Verlag, 1995.
F. Laroussinie and K.G. Larsen. From Timed Automata to Logic — and Back. In Proc. of MFCS'95, Lecture Notes in Computer Sciencie, 1995. Also BRICS report series RS-95-2.
K.G. Larsen, P. Pettersson, and W. Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. To appear in Proc. of the 16th IEEE Real-Time Systems Symposium, December 1995.
Mihalis Yannakakis and David Lee. An efficient algorithm for minimizing real-time transition systems. In Proceedings of CAV'93, volume 697 of Lecture Notes in Computer Science, pages 210–224, 1993.
Wang Yi, Paul Pettersson, and Mats Daniels. Autfomatic Verification of Real-Time Communicating Systems By Constraint-Solving. In Proc. of the 7th International Conference on Formal Description Techniques, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Laxsen, K.G., Pettersson, P., Yi, W. (1996). Diagnostic model-checking for real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds) Hybrid Systems III. HS 1995. Lecture Notes in Computer Science, vol 1066. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0020977
Download citation
DOI: https://doi.org/10.1007/BFb0020977
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61155-4
Online ISBN: 978-3-540-68334-6
eBook Packages: Springer Book Archive