Assertion-Based Analysis of Hybrid Systems with PVS

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.

• Type: Conference
• Year: 2001
• Where: EUROCAST
• Authors: Erika Ábrahám-Mumm, Ulrich Hannemann, Martin Steffen
• Keywords: Deductive Assertional Proof, EUROCAST 2001, Hardware, Hybrid Systems, Theorem Prover Pvs