Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalability, where a powerful specification logic for HSs is the cornerstone. Often, HSs are naturally modelled by concurrent processes that communicate with each other. However, existing specification logics cannot easily handle such models. In this paper, we present a specification logic and proof system for Hybrid Communicating Sequential Processes (HCSP), that extends CSP with ordinary differential equations (ODE) and interrupts to model interactions between continuous and discrete evolution. Because it includes a rich set of algebraic operators, complicated hybrid systems can be easily modelled in an algebra-like compositional way in HCSP. Our logic can be seen as a generalization and simplification of existing hybrid Hoare logics (HHL) based on duration calculus (DC), as well as a conservative extension of existing Hoare logics for concurrent programs. Its assertion logic is the first-order theory of differential equations (FOD), together with assertions about traces recording communications, readiness, and continuous evolution. We prove continuous relative completeness of the logic w.r.t. FOD, as well as discrete relative completeness in the sense that continuous behaviour can be arbitrarily approximated by discretization. Finally, we implement the above logic in Isabelle/HOL, and apply it to verify two case studies to illustrate the power and scalability of our logic.

翻译：近年来，混合系统（HS）的演绎验证因其强大的能力和可扩展性而日益受到关注，其中针对混合系统的强大规约逻辑是基石。混合系统通常自然地建模为相互通信的并发进程。然而，现有的规约逻辑难以处理此类模型。本文提出了一种用于混合通信顺序进程（HCSP）的规约逻辑与证明系统，该系统通过扩展CSP，引入常微分方程（ODE）和中断机制，以建模连续演化与离散演化之间的交互。由于HCSP包含丰富的代数运算符，复杂的混合系统可以以类似代数的组合方式轻松建模。我们的逻辑可视为基于时段演算（DC）的现有混合霍尔逻辑（HHL）的广义化与简化，同时也是现有并发程序霍尔逻辑的保守扩展。其断言逻辑为一阶微分方程理论（FOD），并结合了记录通信、就绪状态和连续演化的迹断言。我们证明了该逻辑相对于FOD的连续相对完备性，以及在离散化可任意逼近连续行为意义上的离散相对完备性。最后，我们在Isabelle/HOL中实现了上述逻辑，并将其应用于两个案例研究的验证，以展示我们逻辑的能力与可扩展性。