Skip to main content
SpringerLink
Log in

Validation of Synchronous Reactive Systems: From Formal Verification to Automatic Testing

  • Conference paper
  • First Online:
Advances in Computing Science — ASIAN’99 (ASIAN 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1742))

Included in the following conference series:

Abstract

This paper surveys the techniques and tools developped for the validation of reactive systems described in the synchronous data-flow language Lustre [HCRP91]. These techniques are based on the specification of safety properties, by means of synchronous observers. The model checker Lsesar [RHR91] takes a Lustre program, and two observers — respectively describing the expected properties of the program, and the assumptions about the system environment under which these properties are intended to hold —, and performs the verification on a finte state (Boolean) abstraction of the system. Recent work concerns extensions towards simple numerical aspects, which are ignored in the basic tool. Provided with the same kind of observers, the tool Lurette [RWNH98] is able to automatically generate test sequences satisfying the environment assumptions, and to run the test while checking the satisfaction of the specified properties.

This work was partially supported by the ESPRIT-LTR project “SYRF”.

Verimag is a joint laboratory of Université Joseph Fourier, CNRS and INPG associated with IMAG.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Bensalem, P. Caspi, C. Dumas, and C. Parent-Vigouroux. A methodology for proving control programs with Lustre and PVS. In Dependable Computing for Critical Applications, DCCA-7, San Jose. IEEE Computer Society, January 1999.

    Google Scholar 

  2. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Fifth IEEE Symposium on Logic in Computer Science, Philadelphia, 1990.

    Google Scholar 

  3. G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87–152, 1992.

    Article  MATH  Google Scholar 

  4. L. du Bousquet, F. Ouabdesselam, J.-L. Richier, and N. Zuanon. Lutess: testing environment for synchronous software. In Tool support for System Specification Development and Verification. Advances in Computing Science, Springer, 1998.

    Google Scholar 

  5. A. Bouali. Xeve: an Esterel verification environment. In Tenth International Conference on Computer-Aided Verfication, CAV’98, Vancouver (B.C.), June 1998. LNCS 1427, Springer Verlag.

    Chapter  Google Scholar 

  6. O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble. LNCS 407, Springer Verlag, 1989.

    Google Scholar 

  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), 1986.

    Google Scholar 

  8. R. De Simone and A. Ressouche. Compositional semantics of esterel and Verification by compositional reductions. In D. Dill, editor, 6th International Conference on Computer Aided Verification, CAV’94, Stanford, June 1994. LNCS 818, Springer Verlag.

    Google Scholar 

  9. N. Halbwachs. Synchronous programming of reactive systems. Kluwer Academic Pub., 1993.

    Google Scholar 

  10. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 79(9):1305–1320, September 1991.

    Article  Google Scholar 

  11. N. Halbwachs, F. Lagnier, and P. Raymond. Synchronous observers and the Verification of reactive systems. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Third Int. Conf. on Algebraic Methodology and Soft-ware Technology, AMAST’93, Twente, June 1993. Workshops in Computing, Springer Verlag.

    Google Scholar 

  12. N. Halbwachs, Y.E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, August 1997.

    Article  Google Scholar 

  13. L. J. Jagadeesan, C. Puchol, and J. E. Von Olnhausen. Safety property Verification of esterel programs and applications to telecommunication software. In P. Wolper, editor, 7th International Conference on Computer Aided Verification, CAV’95, Liege (Belgium), July 1995. LNCS 939, Springer Verlag.

    Google Scholar 

  14. M. Le Borgne, Bruno Dutertre, Albert Benveniste, and Paul Le Guernic. Dynamical systems over Galois fields. In European Control Conference, pages 2191–2196, Groningen, 1993.

    Google Scholar 

  15. P. LeGuernic, T. Gautier, M. LeBorgne, and C. LeMaire. Programming real time applications with Signal. Proceedings of the IEEE, 79(9):1321–1336, September 1991.

    Article  Google Scholar 

  16. B. Marre. Test data selection for reactive synchronous software. In Dagstuhl-Seminar-Report 223: Test Automation for Reactive Systems-Theory and Practice, September 1998.

    Google Scholar 

  17. M. Müllerburg, L. Holenderski, O. Maffeis, and M. Morley. Systematic testing and formal Verification to validate reactive programs. Software Quality Journal, 4(4):287–307, 1995.

    Article  Google Scholar 

  18. J. P. Queille and J. Sifakis. Specification and Verification of concurrent systems in Cesar. In International Symposium on Programming. LNCS 137, Springer Verlag, April 1982.

    Google Scholar 

  19. C. Ratel, N. Halbwachs, and P. Raymond. Programming and verifying critical systems by means of the synchronous data-flow programming language Lustre. In ACM-SIGSOFT’91 Conference on Software for Critical Systems, New Orleans, December 1991.

    Google Scholar 

  20. P. Raymond, D. Weber, X. Nicollin, and N. Halbwachs. Automatic testing of reactive systems. In 19th IEEE Real-Time Systems Symposium, Madrid, Spain, December 1998.

    Google Scholar 

  21. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program Verification. In Symposium on Logic in Computer Science, June 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Verimag, Grenoble, France

    Nicolas Halbwachs & Pascal Raymond

Authors
  1. Nicolas Halbwachs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pascal Raymond
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Chennai Mathematical Institute, 92 G.N. Chetty Road, T. Nagar, Chennai, 600 017, India

    P. S. Thiagarajan

  2. School of Computing, National University of Singapore, Lower Kent Ridge Road, Singapore, 119260

    Roland Yap

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Halbwachs, N., Raymond, P. (1999). Validation of Synchronous Reactive Systems: From Formal Verification to Automatic Testing. In: Thiagarajan, P.S., Yap, R. (eds) Advances in Computing Science — ASIAN’99. ASIAN 1999. Lecture Notes in Computer Science, vol 1742. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46674-6_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-46674-6_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66856-5

  • Online ISBN: 978-3-540-46674-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation