Automated Machine-Checked Hybrid System Safety Proofs

mentation of the Abstraction Method In Coq Eelis van der Weegen Institute for Computing and Information Sciences Raboud University Nijmegen This technical report documents our development of a hybrid afety prover, implemented in Coq using the abstraction method introduced by Alur in [1]. The development includes: a formalization of the structure of hybrid systems; a systematic approach and generic set rt utilities for the construction of an abstract system (consisting of decidable “overestimators” of abstract transitions and initiality) faithpresenting a (concrete) hybrid system; a translation of abstract to graphs enabling decision of abstract state reachability using a certified graph reachability algorithm; a proof of an example hybrid system (taken from [1]) generated using this tool stack. The development critically relies on the computable real number implementation part of the C-CoRN library of formalized constructive mathematics. 1 1 This research was supported by the BRIC...

• Type: Journal
• Year: 2010
• Where: ITP
• Authors: Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen
• Keywords: Abstraction Method, Hybrid Afety Prover, Hybrid System, ITP 2010, Mathematics