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. Concretely, I will first show how ODE safety can be proved using local ODE liveness proofs. Conversely, I will then show how ODE liveness can be deduced through a series of ODE safety proofs.
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.