Advertisement

Safety property verification of Esterel programs and applications to telecommunications software

  • Lalita Jategaonkar Jagadeesan
  • Carlos Puchol
  • James E. Von Olnhausen
Session 4: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

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.

Keywords

Temporal Logic Linear Temporal Logic Safety Property Verification Technique Carrier Group 
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

  1. 1.
    AGEL workshop manual version 3.0, 1989. Produced by ILOG.Google Scholar
  2. 2.
    R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Proc. ACM Symp. on Principles of Distributed Computing, 1991.Google Scholar
  3. 3.
    R. Alur and T. Henzinger. Time for logic. ACM SIGACT News, 22(3), 1991.Google Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    G. Berry and G. Gonthier. The ESTEREL synchronous programming language: design, semantics, implementation. Science of Computer Programming, 19:87–152, 1992.Google Scholar
  6. 6.
    A. Bouajjani, J.C. Fernandez, and N. Halbwachs. On the verification of safety properties, 1994. Draft.Google Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data-flow programming language LUSTRE. Proceedings of the IEEE, 79:1305–1320, 1991.Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    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.Google Scholar
  11. 11.
    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.Google Scholar
  12. 12.
    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.Google Scholar
  13. 13.
    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.Google Scholar
  14. 14.
    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.Google Scholar
  15. 15.
    O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Conference on Logics of Programs, 1985.Google Scholar
  16. 16.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer-Verlag, 1992.Google Scholar
  17. 17.
    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.Google Scholar
  18. 18.
    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.Google Scholar
  19. 19.
    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.Google Scholar
  20. 20.
    M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. LICS, pages 332–339, 1986.Google Scholar
  21. 21.
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Lalita Jategaonkar Jagadeesan
    • 1
  • Carlos Puchol
    • 2
  • James E. Von Olnhausen
    • 3
  1. 1.Software Production Research Dept.AT&T Bell LaboratoriesNapervilleUSA
  2. 2.Dept. of Computer SciencesThe University of Texas at AustinAustinUSA
  3. 3.Global Software Platform LabAT&T Bell LaboratoriesNapervilleUSA

Personalised recommendations