Skip to main content
SpringerLink
Log in

Hybrid verification by exploiting the environment

  • Invited Lectures
  • Conference paper
  • First Online:
Book cover Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1994, ProCoS 1994)

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

Abstract

A method for verifying hybrid systems is given. Such systems involve state components whose values are changed by continuous (physical) processes. The verification method is based on proving that only those executions that satisfy constraints imposed by an environment also satisfy the property of interest. A suitably expressive logic then allows the environment to model state components that are changed by physical processes.

Work supported in part by the Office of Naval Research under contract N00014-91-J-1219, the National Science Foundation under Grant No. CCR-9003440, DARPA/NSF Grant No. CCR-9014363, NASA/DARPA grant NAG-2-893, and AFOSR grant F49620-94-1-0198. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author and do not reflect the views of these agencies.

Limor Fix is also supported, in part, by a Fullbright post-doctoral award.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi and L. Lamport. An old-fashioned recipe for real-time. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Real-time: Theory in Practice, pages 1–17. Lecture Notes in Computer Science Vol. 600, Springer-Verlag, 1992.

    Google Scholar 

  2. R. Alur, C. Courcoubetis, T.A. Henzinger, and P-H. Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 209–229. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.

    Google Scholar 

  3. H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In 16th Annual ACM Aymposium on Theory of Computing, pages 51–63, 1984.

    Google Scholar 

  4. Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1991.

    Google Scholar 

  5. Z. Chaochen, A.P. Ravn, and M.R. Hansen. An extended duration calculus for hybrid real-time systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 36–59. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.

    Google Scholar 

  6. E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proceedings 4th IEEE Symposium on Logic in Computer Science, pages 353–362, 1989.

    Google Scholar 

  7. J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg (eds.). Real-Time: Theory in Practice. Lecture Notes in Computer Science Vol. 600, Springer-Verlag, 1992.

    Google Scholar 

  8. E.A. Emerson. Alternative semantics for temporal logics. Theoretical computer science, 26:121–130, 1983.

    Google Scholar 

  9. L. Fix, N. Francez, and O. Grumberg. Program composition via unification. In 19th International Colloquium On Automata, Languages and Programming, pages 672–684. Lecture Notes in Computer Science Vol. 623, Springer-Verlag, 1992.

    Google Scholar 

  10. L. Fix and F.B. Schneider. Reasoning about programs by exploiting the environment. To appear, 21st International Colloquium On Automata, Languages and Programming.

    Google Scholar 

  11. O. Grumberg and D.E. Long. Model checking and modular verification. In CONCUR'91, 2nd International Conference on Concurrency Theory, pages 250–263. Lecture Notes in Computer Science Vol. 527, Springer-Verlag, 1991.

    Google Scholar 

  12. T.A. Henzinger, Z. Manna, and A. Pnueli. Towards refining temporal specifications into hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 60–76. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.

    Google Scholar 

  13. J. Hooman. A compositional approach to the design of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 121–148. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.

    Google Scholar 

  14. C.B. Jones. Specification and design of (parallel) programs. In R.E.A. Mason, editor, Information Processing'83, pages 321–332. Elsevier Science Publishers, 1983.

    Google Scholar 

  15. L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Engineering, 3:125–143, 1977.

    Google Scholar 

  16. L. Lamport. The hoare logic of concurrent programs. Acta Informatica, 14, 1980.

    Google Scholar 

  17. L. Lamport. Hybrid systems in tla +. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 77–102. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.

    Google Scholar 

  18. O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg, editors, REX Workshop, Real-time: Theory in practice, pages 447–484. Lecture Notes in Computer Science Vol. 600, Springer-Verlag, 1992.

    Google Scholar 

  19. Z. Manna and A. Pnueli. Verifying hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 4–35. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.

    Google Scholar 

  20. K. Marzullo, F.B. Schneider, and N. Budhiraja. Derivation of sequential real-time, process-control programs. In A. Van Tilborg and G. Koob, editors, Foundations of Real-Time Computing, pages 39–54. Kluwer Academic Publishers, 1991.

    Google Scholar 

  21. J. Misra and M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, SE-7(4):417–426, 1981.

    Google Scholar 

  22. X. Nicollin, J. Sifakis, and S. Yovine. From atp to timed graphs and hybrid systems. In J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg, editors, REX Workshop, Real-time: Theory in practice, pages 549–572. Lecture Notes in Computer Science Vol. 600, Springer-Verlag, 1992.

    Google Scholar 

  23. A. Pnueli. In transition from global to modular temporal reasoning about program. In K.R. Apt, editor, Logics and models of concurrent systems, pages 123–144. NATO ASI Series, Vol. F13, Springer-Verlag, 1985.

    Google Scholar 

  24. F.B. Schneider. Designing real-time systems (that really work!). Invited lecture at Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Warwick, England, Sept. 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Cornell University, 14853, Ithaca, New York

    Limor Fix & Fred B. Schneider

Authors
  1. Limor Fix
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fred B. Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Hans Langmaack Willem-Paul de Roever Jan Vytopil

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fix, L., Schneider, F.B. (1994). Hybrid verification by exploiting the environment. In: Langmaack, H., de Roever, WP., Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT ProCoS 1994 1994. Lecture Notes in Computer Science, vol 863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58468-4_157

Download citation

  • DOI: https://doi.org/10.1007/3-540-58468-4_157

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58468-1

  • Online ISBN: 978-3-540-48984-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation