Advertisement

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.

Keywords

Water Level Hybrid System Atomic Action Program Variable Boolean Expression 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. 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. 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. 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. 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. 8.
    E.A. Emerson. Alternative semantics for temporal logics. Theoretical computer science, 26:121–130, 1983.Google Scholar
  9. 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. 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. 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. 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. 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. 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. 15.
    L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Engineering, 3:125–143, 1977.Google Scholar
  16. 16.
    L. Lamport. The hoare logic of concurrent programs. Acta Informatica, 14, 1980.Google Scholar
  17. 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. 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. 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. 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. 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. 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. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Limor Fix
    • 1
  • Fred B. Schneider
    • 1
  1. 1.Department of Computer ScienceCornell UniversityIthaca

Personalised recommendations