Assertion-based Analysis of Hybrid Systems with PVS (Extended Abstract)
Contributor(s)The Pennsylvania State University CiteSeerX Archives
Full recordShow full item record
Abstract31. December 2000 Erika Abraham-Mumm 1 , Ulrich Hannemann 2 , and Martin Steffen 1 1 Institut fur Informatik und praktische Mathematik Christian-Albrechts-Universitat Preuerstrae 1--9, D-24105 Kiel, Deutschland 2 Computing Science Department, University of Nijmegen P.O. Box 9010, NL - 6500 GL Nijmegen, The Netherlands Abstract. Hybrid automata are a well-established mathematical model for discrete systems acting in a continuous environment. We present assertion-based proof methods for hybrid systems for inductive assertional proofs. The model and the proof-methods are rigorously formalized within the PVS theorem-prover. We validate the applicability of the approach on a number of examples. Hybrid systems Combining discrete state-machines with continuous behavior, hybrid systems  have been successfully used to model a large number of applications in areas such as realtime software, embedded systems, and others. Basically, its a state-based formalism augmented by r...