Sciweavers

Share
ITP
2010

Automated Machine-Checked Hybrid System Safety Proofs

8 years 3 months ago
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...
Herman Geuvers, Adam Koprowski, Dan Synek, Eelis v
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Where ITP
Authors Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen
Comments (0)
books