CMU-CS-22-114.pdf (5.1 MB)
Download file

Deductive Verification for Ordinary Differential Equations: Safety, Liveness, and Stability

Download (5.1 MB)
thesis
posted on 12.07.2022, 20:44 authored by Yong Kiam TanYong Kiam Tan

Ordinary differential equations (ODEs) are quintessential models of real-world continuous behavior in the physical and engineering sciences. They also feature prominently in hybrid system models that combine discrete and continuous dynamics, and interactions thereof. Formal verification of ODEs and hybrid systems is of increasing practical importance because the real-world systems they model, such as control systems and cyber-physical systems, are often required to operate in safetyand mission-critical settings—obtaining comprehensive and trustworthy verification results for continuous and hybrid systems gives a strong measure of confidence that the real-world systems they model operate correctly. This thesis studies deductive verification for ordinary dierential equations with a focus on proofs of their i) safety, ii) liveness, and iii) stability properties. These proofs are compositionally extended to obtain proofs of iv) stability for hybrid (switched) systems. The combination of safety, liveness, and stability is crucial for comprehensive correctness of real-world systems: i) safety of a system model ensures that it always stays within a prescribed set of safe states throughout its operation, ii) liveness ensures that the modeled system will eventually reach its speci€ed goal or complete its mission, and iii) & iv) stability ensures that the idealized models are robust to real-world perturbations, which is important for control system designs. The overarching thesis insight is the use of deductive reasoning as a basis for understanding the aforementioned properties and for developing their proofs. Specifically, this thesis uses differential dynamic logic (dL), a logic for deductive verification of hybrid systems, as a trustworthy logical foundation upon which all reasoning principles for safety, liveness, and stability are rigorously derived. The thesis first shows how ODE invariance, a key ingredient in proofs of ODE safety, can be completely axiomatized and reasoned about syntactically in dL. Often, ODE liveness and existence properties are formally proved through reenement-based reasoning in dL, where each reenement step is justified by proving an ODE safety property. Finally, stability properties for ODEs and hybrid systems are specied using dL’s ability to nest safety and liveness modalities with first-order quanti€cation. Proofs of those stability specifications build on ODE safety and liveness (sub-)proofs by compositionally adding dL reasoning for the first-order quantifiers and hybrid systems. Formal dL specifications elucidate the logical relationships between the properties studied in this thesis. Indeed, these relationships are reƒected in the thesis structure outlined above because they yield chapter-by-chapter identification, buildup, and generalization of the deductive building blocks underlying proof methods for the respective properties. The deductive approach enables such generalizations while retaining utmost confidence in the correctness of the resulting proofs because every step is soundly and syntactically justified using dL’s parsimonious axiomatization. The derived proof principles and insights are put into practice by implementing them in the KeYmaera X theorem prover for hybrid systems based on dL. 

History

Date

06/07/2022

Degree Type

Dissertation

Department

Computer Science

Degree Name

  • Doctor of Philosophy (PhD)

Advisor(s)

Andre Platzer