This paper presents a dynamic logic $d\mathcal{L}_\text{CHP}$ for compositional deductive verification of communicating hybrid programs (CHPs). CHPs go beyond the traditional mixed discrete and continuous dynamics of hybrid systems by adding CSP-style operators for communication and parallelism. A compositional proof calculus is presented that modularly verifies CHPs including their parallel compositions from proofs of their subprograms by assumption-commitment reasoning in dynamic logic. Unlike Hoare-style assumption-commitments, $d\mathcal{L}_\text{CHP}$ supports intuitive symbolic execution via explicit recorder variables for communication primitives. Since $d\mathcal{L}_\text{CHP}$ is a conservative extension of differential dynamic logic $d\mathcal{L}$, it can be used soundly along with the $d\mathcal{L}$ proof calculus and $d\mathcal{L}$'s complete axiomatization for differential equation invariants.
翻译:本文提出了一个动态逻辑 $d\ mathcal{L<unk> text{CHP} 用于对交流混合程序( CHPs) 进行构件扣减核查。 CHPs 超越了传统的混合离散和连续的混合系统动态, 添加了通信和平行的 CSP 式操作员 。 提供了一种构成证明的计算法, 模块化地校验了CHPs, 包括通过动态逻辑假设- 承诺推理对其子方案证明的平行构成。 不同于 Hoare 风格的假设- 承诺, $d\ mathcal{L_ text{CHP}$ 支持通过明确的记录器变量对通信原始进行直观的象征性执行。 由于 $d\ mathcal{L_ text{CHP} $ 是差异性动态逻辑的保守延伸 $d\ mathcal{L} $, 它可以与 $d\ mathcal{L} 校准的计算和 $d\ mathcal{L} 美元一起合理使用。</s>