Towards the Safety Verification of Real-Time Systems with the Coq Proof Assistant
Olga Tveretina · 2009
Abstract. Hybrid systems are systems involving the interaction of discrete and continuous dynamics. Hybrid systems have been used as a mathematical model for many safety critical applications. One of the most important analysis problems of hybrid systems is the reachability problem. Approaches based on predicate abstraction are widely used for the reachability analysis. They are not efficient enough because of introducing additional transitivity along the series of abstract states. In this paper we give an approach to solve this problem for some classes of hybrid systems. A verification example formalized within the Coq proof assistant is provided.