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.

翻译：微分动态逻辑（dL）是一种形式化框架，用于对混成系统（即同时呈现连续与离散行为的动态系统）进行规约与推理。此类系统广泛存在于诸多安全关键及任务关键型应用中。本文提出了在原型验证系统（PVS）中对dL的形式化实现，涵盖混成程序的语义及dL的证明演算。该形式化将dL嵌入至PVS逻辑中，由此生成的dL版本不仅其证明演算得到形式验证，而且可直接在PVS内部用于混成程序的验证。该嵌入方法被称为Plaidypvs（面向混成程序验证与规约的dL可保障实现），它支持标准的dL风格证明，并进一步利用PVS的能力实现对整类混成程序的推理。同时，该嵌入方法允许用户导入PVS中已有的成熟定义与数学理论。