A Usage-Aware Sequent Calculus for Differential Dynamic Logic

TL;DR

This paper introduces a formal, proof-based method for detecting over-specified constraints in differential dynamic logic models, improving model flexibility and correctness in safety-critical hybrid systems.

Contribution

It presents a novel, sound, and complete technique for identifying and suggesting mutations for over-specified constraints in dL formulas, enhancing model robustness.

Findings

Detects vacuous or over-specified constraints in dL models

Proposes mutations to improve model flexibility while preserving correctness

Proves soundness and completeness of the approach

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.