A Generalized Hybrid Hoare Logic
Naijun Zhan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Dimitar Guelev
TL;DR
This work delivers a generalized Hoare logic for Hybrid CSP (HCSP) that unifies concurrent communication and continuous evolution through a trace-based semantics. It introduces a comprehensive assertion logic built on first-order differential equations (FOD) with generalized traces, and proves both continuous and discrete relative completeness, while maintaining compositional reasoning about parallelism. The logic is implemented in Isabelle/HOL and validated on two case studies (a lunar lander controller and a parallel scheduler), demonstrating scalability and practical applicability to complex safety-critical hybrid systems. By generalizing beyond duration calculus and enabling explicit trace-based synchronization, the approach offers a scalable, modular framework for verifying safety properties of HSs in a concurrent setting. The work lays a foundation for future extensions to livelock analysis and total correctness within a robust formal framework.
Abstract
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.