HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
TL;DR
The paper addresses automated verification of parallel HCSP models describing hybrid systems with communication and synchronization. It builds HHLPar on Hybrid Hoare Logic, extends prior HHLPy to support parallel composition via explicit assertion language and synchronization rules, and formalizes the rules in Isabelle/HOL for soundness. It provides a Python-based implementation that integrates external solvers for ODEs and real arithmetic to automate deduction by symbolically decomposing and composing HCSP processes. The approach is demonstrated on a simplified cruise control case, showing automated verification of safety properties for hybrid, communicating systems and indicating practical impact for safety-critical cyber-physical verification.
Abstract
We present a tool called HHLPar for verifying hybrid systems modelled in Hybrid Communicating Sequential Processes (HCSP). HHLPar is built upon a Hybrid Hoare Logic for HCSP, which is able to reason about continuous-time properties of differential equations, as well as communication and parallel composition of parallel HCSP processes with the help of parameterised trace assertions and their synchronization. The logic was formalised and proved to be sound in Isabelle/HOL, which constitutes a trustworthy foundation for the verification conducted by HHLPar. HHLPar implements the Hybrid Hoare Logic in Python and supports automated verification: On one hand, it provides functions for symbolically decomposing HCSP processes, generating specifications for separate sequential processes and then composing them via synchronization to obtain the final specification for the whole parallel HCSP processes; On the other hand, it is integrated with external solvers for handling differential equations and real arithmetic properties. We have conducted experiments on a simplified cruise control system to validate the performance of the tool.