Assertion-Based Analysis of Hybrid Systems with PVS

11 years 9 months ago
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.
Erika Ábrahám-Mumm, Ulrich Hannemann
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Authors Erika Ábrahám-Mumm, Ulrich Hannemann, Martin Steffen
Comments (0)