Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Usage-Aware Sequent Calculus for Differential Dynamic Logic

Myra Dotzel, Stefan Mitsch, André Platzer

TL;DR

A novel proof-based technique is presented that detects which constraints in a dL formula are vacuous or over-specified and suggests ways in which these components could be mutated while preserving correctness proofs and general applicability of the technique.

Abstract

Ensuring that safety-critical applications behave as intended is an important yet challenging task. Modeling languages like differential dynamic logic (dL) have proof calculi capable of proving guarantees for such applications. However, dL programmers may unintentionally over-specify assumptions and program statements, which results in overly constrained models that yield weak or vacuous guarantees. In hybrid systems models, such constraints are ubiquitous; they may appear as assumptions, conditions on control switches, and evolution domain constraints in systems of differential equations which makes it nontrivial to systematically detect which ones are over-specified. Existing approaches are limited, either lacking formal correctness guarantees or the granularity to detect all kinds of bugs arising in a given formula. As a remedy, we present a novel proof-based technique that detects which constraints in a dL formula are vacuous or over-specified and suggests ways in which these components could be mutated while preserving correctness proofs. When properties follow entirely from constraints uninfluenced by program statements, this analysis spots outright flaws in models. Otherwise, it helps make models more flexible by identifying specific ways in which they may be generalized. The resulting analysis is thorough, catching bugs at a fine-grained level and proposing mutations that could be applied in combination. We prove soundness and completeness with respect to dL to ensure the correctness of suggested mutations and general applicability of our technique.

A Usage-Aware Sequent Calculus for Differential Dynamic Logic

TL;DR

A novel proof-based technique is presented that detects which constraints in a dL formula are vacuous or over-specified and suggests ways in which these components could be mutated while preserving correctness proofs and general applicability of the technique.

Abstract

Ensuring that safety-critical applications behave as intended is an important yet challenging task. Modeling languages like differential dynamic logic (dL) have proof calculi capable of proving guarantees for such applications. However, dL programmers may unintentionally over-specify assumptions and program statements, which results in overly constrained models that yield weak or vacuous guarantees. In hybrid systems models, such constraints are ubiquitous; they may appear as assumptions, conditions on control switches, and evolution domain constraints in systems of differential equations which makes it nontrivial to systematically detect which ones are over-specified. Existing approaches are limited, either lacking formal correctness guarantees or the granularity to detect all kinds of bugs arising in a given formula. As a remedy, we present a novel proof-based technique that detects which constraints in a dL formula are vacuous or over-specified and suggests ways in which these components could be mutated while preserving correctness proofs. When properties follow entirely from constraints uninfluenced by program statements, this analysis spots outright flaws in models. Otherwise, it helps make models more flexible by identifying specific ways in which they may be generalized. The resulting analysis is thorough, catching bugs at a fine-grained level and proposing mutations that could be applied in combination. We prove soundness and completeness with respect to dL to ensure the correctness of suggested mutations and general applicability of our technique.
Paper Structure (62 sections, 14 theorems, 72 equations, 11 figures)

This paper contains 62 sections, 14 theorems, 72 equations, 11 figures.

Table of Contents

  1. Introduction
  2. Outline.
  3. Background and Motivation
  4. Differential Dynamic Logic (dL)
  5. Parachute Model
  6. Parachute Proof
  7. Key Ideas of Usage-Aware Sequents
  8. Atoms and Labels
  9. Properties.
  10. Mutations
  11. Properties.
  12. Tracking Label Sets
  13. Merge ($\uplus$).
  14. Discard ($\setminus$).
  15. Properties.
  16. ...and 47 more sections

Key Result

lemma 1

If $\color{red}\vec{\mathbf{{\mathbf i}}}{:}\color{black} \Gamma \vdash\mkern-5mu\color{blue}^{\Psi}_{\Sigma}\color{black}\, \color{red}\vec{\mathbf{{\mathbf j}}}{:}\color{black} \Delta$ is valid and the labels in $\color{blue}\Psi\color{black}$ are unique, then for all $\color{blue}\Psi$ each label

Figures (11)

  • Figure 1: Model of parachute dynamics, adopted from ITP2017.
  • Figure 2: Parachute example proof fragment in UAPC (with red, blue, and violet labels) or dL (without). We write $\color{blue}DA(\dots {\mid} \Psi)$ for $\color{blue}DA(i_5,i_6,i_7,i_8,u_1,j,k,l,n,r,s \,{\mid} \Psi)$.
  • Figure 3: Definition of mutation $\mathcal{M}$
  • Figure 4: Definition of merge operator $\uplus$
  • Figure 5: Definition of discard operator $\setminus$
  • ...and 6 more figures

Theorems & Definitions (22)

  • definition 1: Uniqueness
  • definition 2: Freshness
  • definition 3: Mutation structure
  • lemma 1: Well-formed sets
  • definition 4: Fusing
  • lemma 2: Composition of mutations
  • definition 5: $\phi$ function
  • definition 6: Dynamic Analysis
  • theorem 1: Soundness
  • theorem 2: Completeness
  • ...and 12 more