Abstract
Uppaal is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata [12, 9, 4], developed during the past two years. In this paper, we summarize the main features of Uppaal in particular its various extensions developed in 1995 as well as applications to various case-studies, review and provide pointers to the theoretical foundation.
This work has been supported by the European Communities (under CONCUR2 and REACT), NUTEK (Swedish Board for Technical Development) and TFR (Swedish Technical Research Council).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Martin Abadi and Leslie Lamport. An Old-Fashioned Recipe for Real Time. Lecture Notes in Computer Science, 600, 1993.
J.-R. Abrial. Steam-boiler control specification problem. June 1995. International Seminar on Methods for Semantics and Specification.
Johan Bengtsson, David Griffioen, Kåre Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Verification of an Audio Protocol with Bus Collision Using Uppaal. Submitted for publication, 1996.
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, 1994.
C. Daws and S. Yovine. Two examples of verification of multirate timed automata with Kronos. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 66–75, December 1995.
Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. A Users Guide to HyTech. Technical report, Department of Computer Science, Cornell University, 1995.
Mathai Joseph, Alan Burns, Andy Welling, Krithi Ramamritham, Jozef Hooman, Steve Schneider, Zhiming Liu, and Henk Schepers. Real-time Systems Specification, Verification and Analysis. Prentice Hall, 1996.
Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 76–87, December 1995.
Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. In Proc. of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, Lecture Notes in Computer Science, October 1995.
A. Olivero, J. Sifakis, and S. Yovine. Using Abstractions for the Verification of Linear Hybrids Systems. In Proc. of CAV'94, volume 818 of Lecture Notes in Computer Science, 1994.
Wang Yi, Paul Pettersson, and Mats Daniels. Automatic 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
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W. (1996). Uppaal in 1995. In: Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1996. Lecture Notes in Computer Science, vol 1055. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61042-1_66
Download citation
DOI: https://doi.org/10.1007/3-540-61042-1_66
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61042-7
Online ISBN: 978-3-540-49874-2
eBook Packages: Springer Book Archive