Deductive Verification for Ordinary Differential Equations
24/03/2021
Speaker
Yong Kiam Tan (CMU)
Abstract
Cyber-physical systems (CPSs) feature software controllers interacting with real world physics. Correctness for such systems is paramount since they often operate in safety- or mission-critical settings. To verify correctness for a CPS, one first needs to have a model of its real world physics and methods for analyzing that model. In this talk, I will explain how ordinary differential equations (ODEs) models of CPS physics can be analyzed using a logical, deductive approach.
The first strength of this logical approach is enabling highly trustworthy, computer-checkable proofs of correctness properties for ODEs and CPSs. The second strength is its generality and flexibility, which I will exemplify through the deductive analysis of two key correctness properties for ODEs: safety and liveness. Safety of a system means it never reaches an undesirable (unsafe) state, while liveness means it eventually reaches a desirable (goal) state. This duality between safety and liveness is made precise through the lens of logic and it is their logical interplay which enables their analysis.