Formal Verification of Stability Properties in Cyber-physical Systems

Matthew Chan, Daniel Ricketts, Sorin Lerner, Gregory Malecha

We increasingly rely on computers to interact with the physical world for us. At the large end, software underlies the control systems of commercial aircraft and power plants, and at the small end it controls medical devices and hobbyist UAVs. The failure of any of these systems can have severe consequences which are often measured in the loss of human lives. Formal verification has proven a promising approach to achieving very strong guarantees in more classic areas of computer science. In this work we present an overview of our experiences formalizing stability properties of cyber-physical systems (CPSs) using the Coq proof assistant.

cyber-physical systems veridrone stability

download

@conference{malecha2015semantic-optimization,
 author = {Matthew Chan and Daniel Ricketts and Sorin Lerner and Gregory Malecha},
 title = {Formal {V}erification of {S}tability {P}roperties of {C}yber-physical {S}ystems},
 conference={CoqPL'16},
 month={Jan}
 year = {2016},
 location = {St. Petersburg, FL, USA},
}