HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
摘要
We introduce HHLPar, a tool for verifying hybrid systems modeled in Hybrid Communicating Sequential Processes (HCSP). HHLPar is based on a Hybrid Hoare Logic for HCSP, which enables reasoning about both the continuous-time properties of differential equations and the communication and parallel composition of HCSP processes. This is achieved through the use of specialized trace assertions and their synchronization. The logic has been formalized and proven sound in Isabelle/HOL, providing a reliable foundation for the verification. HHLPar implements the logic in Python and supports automated verification: On one hand, it provides functions for symbolically decomposing HCSP processes, generating assertions for individual sequential processes, and then composing them via synchronization to obtain the final specification for the entire parallel HCSP process; On the other hand, it is integrated with external solvers for handling differential equations and real arithmetic properties. The resulting assertions are sufficiently expressive to deduce both the state properties at termination and the continuous-time invariants maintained throughout the execution of processes, which are critical for ensuring system safety. Finally, we present the main issues related to the implementation of HHLPar and demonstrate its applicability through a case study involving a simplified cruise control system.