HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes

TL;DR

HHLPar is an automated verification tool for hybrid systems modeled in HCSP, combining symbolic decomposition, external solvers, and formal logic to verify properties of parallel hybrid processes.

Contribution

It introduces a sound Hybrid Hoare Logic formalized in Isabelle/HOL and implements it in Python for automated verification of parallel hybrid systems.

Findings

Successfully verified a simplified cruise control system

Demonstrated effective symbolic decomposition and solver integration

Validated the soundness and practicality of HHLPar

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.