Towards Verification of Hybrid Systems in a Foundational Proof Assistant

Daniel Ricketts, Gregory Malecha, Mario M. Alvarez, Vignesh Gowda and Sorin Lerner

Unsafe behavior of hybrid systems can have disastrous consequences, motivating the need for formal verification of the software running on these systems. Foundational verification in a proof assistant such as Coq is a promising technique that can provide extremely strong, foundational, guarantees about software systems. In this paper, we show how to apply this technique to hybrid systems. We define a TLA-inspired formalism in Coq for reasoning about hybrid systems and use it to verify two quadcopter modules: the first limits the quadcopter’s velocity and the second limits its altitude. We ran both of these modules on an actual quadcopter, and they worked as intended. We also discuss lessons learned from our experience foundationally verifying hybrid systems.

cyber-physical systems verification

download

@inproceedings{ricketts2015towards,
  author={Ricketts, Daniel and Malecha, Gregory and Alvarez, Mario M. and Gowda, Vignesh and Lerner, Sorin}, 
  booktitle={Formal Methods and Models for Codesign (MEMOCODE), 2015 ACM/IEEE International Conference on}, 
  title={Towards verification of hybrid systems in a foundational proof assistant}, 
  year={2015},
  pages={248-257},
  keywords={Cognition;Computer architecture;Differential equations;Safety;Sensors;Software;Upper bound}, 
  doi={10.1109/MEMCOD.2015.7340492},
  month={Sept}
}