Abstract
We present a technique for automatically verifying linear-time temporal logic safety properties of programs written in Esterel, a formally-defined language for programming reactive systems. In our approach, linear-time temporal logic safety properties are first translated into Esterel programs that model these properties. Using the Esterel compiler, the translations are compiled in parallel with the Esterel program to be verified. A trivial reachability analysis of the output of the compiler then indicates whether or not the safety property is satisfied by the program. We describe two real-world software problems — Esterel versions of two features of the AT&T 5ESS® switching system — and one well-known benchmark problem — the generalized railroad crossing problem — that we have verified using our technique and associated tool set.
The author is currently supported by a Fulbright fellowship. The work described here was performed while the author was visiting AT&T Bell Laboratories.
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
AGEL workshop manual version 3.0, 1989. Produced by ILOG.
R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Proc. ACM Symp. on Principles of Distributed Computing, 1991.
R. Alur and T. Henzinger. Time for logic. ACM SIGACT News, 22(3), 1991.
M. Ardis, John A. Chaves, L. Jagadeesan, P. Mataga, C. Puchol, M. Staskauskas, and J. Von Olnhausen. A framework for evaluating specification methods for reactive systems. In Proc. 17th Intl. Conf. on Software Engineering, April 1995.
G. Berry and G. Gonthier. The ESTEREL synchronous programming language: design, semantics, implementation. Science of Computer Programming, 19:87–152, 1992.
A. Bouajjani, J.C. Fernandez, and N. Halbwachs. On the verification of safety properties, 1994. Draft.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2):244–263, 1986.
N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data-flow programming language LUSTRE. Proceedings of the IEEE, 79:1305–1320, 1991.
N. Halbwachs, F. Lagnier, and C. Ratel. Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE. Transactions on Software Engineering, 18(9):785–793, 1992.
N. Halbwachs, D. Pilaud, F. Ouabdesselam, and A.C. Glory. Specifying, programming and verifying reactive systems, using a synchronous declarative language. In Workshop on Automatic Verification Methods for Finite State Systems, LNCS Vol. 407, 1989.
G. Haugk, F.M. Lax, R.D. Royer, and J.R. Williams. The 5ESS(TM) switching system: Maintenance capabilities. AT&T Tech. Journal, 64(6 part 2): 1385–1416, Jul–Aug 1985.
C. Heitmeyer, R.D. Jeffords, and B. Labaw. A benchmark for comparing different approaches for specifying and verifying real-time systems. In Proc. 10th International Workshop on Real-Time Operating Systems and Software, May 1993.
L.J. Jagadeesan, C. Puchol, and J.E. Von Olnhausen. A formal approach to reactive systems software: A telecommunications application in Esterel. In Proc. Workshop on Industrialstrength Formal Spec. Techniques, April 1995.
O Lichtenstein and A. Pnueli. Checking that finite-state concurrent programs satisfy their linear specifications. In ACM Symposium on Priciples of Programming Languages, pages 97–107, 1985.
O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Conference on Logics of Programs, 1985.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer-Verlag, 1992.
K.E. Martersteck and A.E. Spencer. Introduction to the 5ESS(TM) switching system. AT&T Tech. Journal, 64(6 part 2):1305–1314, Jul–Aug 1985.
D. Pilaud and N. Halbwachs. From a synchronous declarative language to a temporal logic dealing with multi-form time. In Symposium on Formal Techniques in Real-Time and Fault-Tolerant Techniques, LNCS Vol. 331, 1988.
C. Puchol. A solution to the generalized railroad crossing problem in Esterel. Technical Report UTCS-TR95-05, Dept. of Com. Sci., Univ. of Texas at Austin, Feb 1995.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. LICS, pages 332–339, 1986.
P. Wolper, M.Y. Vardi, and A.P. Sistla. Reasoning about infinite computation paths. In IEEE Symposium on Foundations of Computer Science, pages 185–194, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jagadeesan, L.J., Puchol, C., Von Olnhausen, J.E. (1995). Safety property verification of Esterel programs and applications to telecommunications software. In: Wolper, P. (eds) Computer Aided Verification. CAV 1995. Lecture Notes in Computer Science, vol 939. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60045-0_45
Download citation
DOI: https://doi.org/10.1007/3-540-60045-0_45
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60045-9
Online ISBN: 978-3-540-49413-3
eBook Packages: Springer Book Archive