Skip to main content
SpringerLink
Log in

Assertion-Based Analysis of Hybrid Systems with PVS

  • Conference paper
  • First Online:
Computer Aided Systems Theory — EUROCAST 2001 (EUROCAST 2001)

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

Included in the following conference series:

Abstract

Hybrid systems are a well-established mathematical model for embedded systems. Such systems, which combine discrete and continuous behavior, are increasingly used in safety-critical applications. To guarantee safe functioning, formal verification techniques are crucial. While research in this area concentrates on model checking, deductive techniques attracted less attention. In this paper we use the general purpose theorem prover PVS for the rigorous formalization and analysis of hybrid systems. To allow for machine-assisted proofs, we implement a deductive assertional proof method within PVS. The sound and complete proof system allows modular proofs in that it comprises a proof rule for the parallel composition. Besides hybrid systems and the proof system, a number of examples are formalized within PVS.

The work was supported by the Dutch Technology Foundation STW, project EIF 3959, Formal Design of Industrial Safety-Critical Systems and further by the German Research Council (DFG) within the special program KONDISK under grant LA 1012/5-1.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. E. Ábrahfm-Mumm, U. Hannemann, and M. Steffen. Verification of hybrid systems: Formalization and proof rules in PVS. Technical Report TR-ST-01-1, Lehrstuhl für Software-Technologie, Institut für Informatik und praktische Mathematik, Christian-Albrechts-Universität Kiel, Jan. 2001.

    Google Scholar 

  2. R. Alur, C. Courcoubetis, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995. A preliminary version appeared in the proceedings of 11th. International Conference on Analysis and Optimization of Systems: Discrete Event Systems (LNCI 199).

    Article  MATH  MathSciNet  Google Scholar 

  3. R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:252–235, 1994.

    Article  MathSciNet  Google Scholar 

  4. R. Alur, T. A. Henzinger, and P. Ho. Automatic symbolic verification of embedded systems. In Proc. 14th Annual Real-Time Systems Symposium, pages 2–11. IEEE Computer Society Press, 1993.

    Google Scholar 

  5. M. Archer and C. Heitmeyer. Verifying hybrid systems modeled as timed automata: A case sudy. In O. Maler, editor, Hybrid and Real-Time Systems (HART’97), number 1201 in Lecture Notes in Computer Science, pages 171–185. Springer-Verlag, 1997.

    Chapter  Google Scholar 

  6. E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.

    Google Scholar 

  7. The Coq project. http://pauillac.inria.fr/coq/, 1998.

  8. J. B. de Meer and E. Ábrahám-Mumm. Formal methods for reflective system specification. In J. Grabowski and S. Heymer, editors, Formale Beschreibungstechniken für verteilte Systeme, pages 51–57. Universität Lübeck/Shaker Verlag, Aachen, Juni 2000 2000.

    Google Scholar 

  9. W.-P. de Roever, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, 2001. to appear.

    Google Scholar 

  10. R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Proc. Symp. In Applied Mathematics, volume 19, pages 19–32, 1967.

    Google Scholar 

  11. M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.

    Google Scholar 

  12. R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors. Hybrid Systems, volume 736 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

    Google Scholar 

  13. U. Hannemann. Semantic Analysis of Compositional Proof Methods for Concurrency. PhD thesis, Utrecht Universiteit, Oct. 2000.

    Google Scholar 

  14. T. Henzinger and H. Wong-Toi. Linear phase-portrait approximations for nonlinear hybrid systems. In R. Alur, T. Henzinger, and E. D. Sontag, editors, Hybrid Systems III, volume 1066 of Lecture Notes in Computer Science, pages 377–388, 1996.

    Chapter  Google Scholar 

  15. T. A. Henzinger and P.-H. Ho. Algorithmic analysis of nonlinear hybrid systems. In P. Wolper, editor, CAV’ 95: Computer Aided Verification, volume 939 of Lecture Notes in Computer Science, pages 225–238. Springer-Verlag, 1995.

    Google Scholar 

  16. T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata. In 27th Annual ACM Symposium on Theory of Computing. ACM Press, 1995.

    Google Scholar 

  17. T. A. Henzinger and V. Rusu. Reachability verification for hybrid automata. In Henzinger and Sastry [18], pages 190–204.

    Google Scholar 

  18. T. A. Henzinger and S. Sastry, editors. Proceedings of the First International Workshop on Hybrid Systems: Computation and Control (HSCC’98), volume 1386 of Lecture Notes in Computer Science. Springer, 1998.

    Google Scholar 

  19. J. Hooman. A compositional approach to the design of hybrid systems. In Grossman et al. [12], pages 121–148.

    Google Scholar 

  20. A. Kapur, T. A. Henzinger, Z. Manna, and A. Pnueli. Proving safety properties of hybrid systems. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems 1994, volume 863 of Lecture Notes in Computer Science, Kiel, Germany, September 1994. Springer-Verlag. 3rd International School and Symposium.

    Google Scholar 

  21. Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration graphs: a class of decidable hybrid systems. In Grossman et al. [12], pages 179–208.

    Google Scholar 

  22. S. Kowalewski, P. Herrmann, S. Engell, H. Krumm, H. Treseler, Y. Lakhnech, R. Huuck, and B. Lukoschus. Approaches to the formal verification of hybrid systems. at Automatisierungstechnik. Special Issue: Hybrid Systems II: Analysis, Modeling, and Verification, 49(2):66–74, Feb. 2001.

    Google Scholar 

  23. N. A. Lynch, R. Segala, and F. W. Vaandrager. Hybrid I/O automata revisited. In M. D. D. Benedetto and A. Sangiovanni-Vincentelli, editors, Proceedings of the 4th International Wokrshop on Hybrid Systems: Computation and Control (HSCC 2001), Rome, volume 2034 of Lecture Notes in Computer Science. Springer-Verlag, 2001.

    Google Scholar 

  24. Z. Manna and H. B. Sipma. Deductive verification of hybrid systems using STeP. In Henzinger and Sastry [18].

    Google Scholar 

  25. S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, Automated Deduction (CADE-11), volume 607 of Lecture Notes in Computer Science, pages 748–752. Springer-Verlag, 1992.

    Google Scholar 

  26. S. Owre, N. Shankar, J. M. Rushby, and D.W. J. Stringer-Calvert. PVS Manual (Language Reference, Prover Guide, System Guide). Computer Science Laboratory, SRI International, Menlo Park, CA, Sept. 1999.

    Google Scholar 

  27. L. C. Paulson. The Isabelle reference manual. Technical Report 283, University of Cambridge, Computer Laboratory, 1993.

    Google Scholar 

  28. O. Roux and V. Rusu. Uniformity for the decidability of hybrid automata. In R. Cousot and D. A. Schmidt, editors, Proceedings of SAS’ 96, volume 1145 of Lecture Notes in Computer Science, pages 301–316. Springer-Verlag, 1996.

    Google Scholar 

  29. J. M. Rushby, 2001. available electronically at http://www.csl.sri.com/papers/pvs-bib/

  30. N. Shankar. Lazy compositional verification. In W.-P. de Roever, H. Langmaack, and A. Pnueli, editors, Compositionality: The Significant Difference (Compos’ 97), volume 1536 of Lecture Notes in Computer Science, pages 541–564. Springer, 1998.

    Chapter  Google Scholar 

  31. T. Stauner. Properties of hybrid systems-a computer science perspective. Technical Report TUM-I0017, Technische Universität München, Nov. 2000.

    Google Scholar 

  32. T. Stauner. Hybrid systems’ properties-classification and relation to computer science. In Proceedings of the Eight International Conference on Computer Aided Systems Theory, Formal Methods and Tools for Computer Science (Eurocast’ 01), Lecture Notes in Computer Science. Springer-Verlag, 2001.

    Google Scholar 

  33. J. Vitt and J. Hooman. Assertional specification and verification using PVS of the steam boiler system. In Formal Methods for Industrial Applications: Specifying and Programmin the Steam Boiler Control System, volume 1165 of Lecture Notes in Computer Science, pages 453–472. Springer, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Preußerstraße 1—9, D-24105, Kiel, Deutschland

    Erika Ábrahám-Mumm & Martin Steffen

  2. Computing Science Department, University of Nijmegen, P.O. Box 9010, NL - 6500, GL Nijmegen, The Netherlands

    Ulrich Hannemann

Authors
  1. Erika Ábrahám-Mumm
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ulrich Hannemann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martin Steffen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Universidad de Las Palmas de Gran Canaria, Instituto Universitario de Ciencias y Tecnologías Cibernéticas, Campus de Tafira, 35017, Las Palmas de Gran Canaria, Spain

    Roberto Moreno-Díaz

  2. University of Linz, Research Institute for Symbolic Computation, 232, Schloss Hagenberg, Austria

    Bruno Buchberger

  3. University ofA Coruña, Facultad de Informática, LFCIA, Dpto. of Computer Science, Campus de Elviña, 15071, A Coruña, Spain

    José Luis Freire

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ábrahám-Mumm, E., Hannemann, U., Steffen, M. (2001). Assertion-Based Analysis of Hybrid Systems with PVS. In: Moreno-Díaz, R., Buchberger, B., Luis Freire, J. (eds) Computer Aided Systems Theory — EUROCAST 2001. EUROCAST 2001. Lecture Notes in Computer Science, vol 2178. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45654-6_8

Download citation

  • DOI: https://doi.org/10.1007/3-540-45654-6_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42959-3

  • Online ISBN: 978-3-540-45654-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation