Embedding Differential Dynamic Logic in PVS

TL;DR

This paper formalizes differential dynamic logic within PVS, enabling verified reasoning about hybrid systems with continuous and discrete behaviors through an embedded proof calculus.

Contribution

It introduces Plaidypvs, a formal embedding of dL into PVS, allowing for verified hybrid program reasoning and leveraging PVS's existing mathematical theories.

Findings

Formal semantics of hybrid programs in PVS

Verified proof calculus for dL within PVS

Supports reasoning about classes of hybrid systems

Abstract

Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and mission-critical applications. This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and dL's proof calculus. The formalization embeds dL into the PVS logic, resulting in a version of dL whose proof calculus is not only formally verified, but is also available for the verification of hybrid programs within PVS itself. This embedding, called Plaidypvs (Properly Assured Implementation of dL for Hybrid Program Verification and Specification), supports standard dL style proofs, but further leverages the capabilities of PVS to allow reasoning about entire classes of hybrid programs. The embedding also allows the user to import the well-established definitions and mathematical theories available in PVS.