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. Besides, we discuss how to simplify proofs using the logic by providing a simplified assertion language and a set of sound and complete rules for differential invariants for ODEs. Finally, we implement a proof assistant for the 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的连续相对完备性，以及通过离散化任意逼近连续行为的离散相对完备性。此外，通过提供简化断言语言和一组完备的ODE微分不变量推理规则，我们探讨了如何利用该逻辑简化证明。最后，我们在Isabelle/HOL中实现了该逻辑的证明助手，并应用于两个案例的验证，以展示本逻辑的能力与可扩展性。