Abstract
The efficient representation and manipulation of time information is key to any successful implementation of a verification tool. We extend the syntax and semantics of the higher level specification language Promela to include constructs and statements based on the model of timed Büchi automata [2]. We implement these extensions on top of the verification tool Spin.
Partially supported by the BRA ESPRIT project REACT.
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
R. Alur. Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Stanford University, 1991.
R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 414–425, Philadelphia, June 1990.
R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An implementation of three algorithms for timing verification based on automata emptiness. In RTSS 1992, proceedings, 1992.
R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. Minimization of timed transition systems. In CONCUR 1992, proceedings. Lecture Notes in Computer Science, Springer-Verlag, 1992.
C. Courcoubetis, D. Dill, M. Chatzaki, and P. Tzounakis. Verification with real-time COSPAN. In Proceedings of the Fourth Workshop on Computer-Aided Verification, Lecture Notes in Computer Science. Springer-Verlag, 1992.
D. Dill. Timing assumptions and verification of finite-state concurrent systems. In Proc. Workshop on Computer Aided Verification, CAV89, Grenoble, June 1989. Lecture Notes in Computer Science, Springer-Verlag.
Dolev, Klawe, and Rodeh. An O(n log n) unidirectional distributed algorithm for extrema finding in a circle. J. of Algs, 3:245–260, 1982.
G.J. Holzmann. Design and Validation of Protocols. Prentice-Hall, 1990.
G.J. Holzmann. Basic spin manual. Technical report, AT&T, Bell Laboratories, 1994.
G.J. Holzmann. What's new in spin. Technical report, AT&T, Bell Laboratories, 1995.
G.J. Holzmann and Doron A. Peled. An improvement in formal verification. In Proceedings of the 7th International Conference on Formal Description Techniques, FORTE94, Berne, Switcherland, October 1994.
M. Katevenis, S. Sidiropoulos, and C. Courcoubetis. Weighted round-robin cell multiplexing in a general purpose ATM switch chip. IEEE JSAC, 9(8):1265–1279, 1991.
J. Katzenelson and B. Kurshan. S/r: A language for specifying protocols and other coordinating processes. In Proc. 5th Ann. Int'l Phoenix Conf. Comput. Commun., IEEE, 1986.
N. Lambrogeorgos. Verification of real-time systems: a case study of discrete and dense time models, 1993. Available only in greek.
L. Lamport. A fast mutual exclusion algorithm. ACM Transactions on Computer Systems, 5(1):1–11, 1987.
Doron A. Peled. Combining partial order reductions with on-the-fly model checking. In Proceedings of the 6th International Conference on Comptuter Aided Verification, CAV94, Stanford, California, june 1994.
S. Sidiropoulos. A general purpose ATM switch. architecture and feasibility study, 1991.
P. Tzounakis. Verification of real time systems: The extension of COSPAN in dense time, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tripakis, S., Courcoubetis, C. (1996). Extending promela and spin for real time. 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_53
Download citation
DOI: https://doi.org/10.1007/3-540-61042-1_53
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