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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
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).
R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:252–235, 1994.
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.
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.
E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
The Coq project. http://pauillac.inria.fr/coq/, 1998.
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.
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.
R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Proc. Symp. In Applied Mathematics, volume 19, pages 19–32, 1967.
M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.
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.
U. Hannemann. Semantic Analysis of Compositional Proof Methods for Concurrency. PhD thesis, Utrecht Universiteit, Oct. 2000.
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.
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.
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.
T. A. Henzinger and V. Rusu. Reachability verification for hybrid automata. In Henzinger and Sastry [18], pages 190–204.
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.
J. Hooman. A compositional approach to the design of hybrid systems. In Grossman et al. [12], pages 121–148.
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.
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.
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.
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.
Z. Manna and H. B. Sipma. Deductive verification of hybrid systems using STeP. In Henzinger and Sastry [18].
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.
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.
L. C. Paulson. The Isabelle reference manual. Technical Report 283, University of Cambridge, Computer Laboratory, 1993.
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.
J. M. Rushby, 2001. available electronically at http://www.csl.sri.com/papers/pvs-bib/
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.
T. Stauner. Properties of hybrid systems-a computer science perspective. Technical Report TUM-I0017, Technische Universität München, Nov. 2000.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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