A Usage-Aware Sequent Calculus for Differential Dynamic Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909337731989504 |
|---|---|
| author | Dotzel, Myra Mitsch, Stefan Platzer, André |
| author_facet | Dotzel, Myra Mitsch, Stefan Platzer, André |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2309_01180 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | A Usage-Aware Sequent Calculus for Differential Dynamic Logic Dotzel, Myra Mitsch, Stefan Platzer, André Formal Languages and Automata Theory 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. |
| title | A Usage-Aware Sequent Calculus for Differential Dynamic Logic |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2309.01180 |