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.

翻译：本文提出了一种名为HHLPar的工具，用于验证基于混合通信顺序进程（HCSP）建模的混合系统。HHLPar建立在面向HCSP的混合霍尔逻辑之上，该逻辑能够借助参数化迹断言及其同步机制，对微分方程的连续时间属性以及并行HCSP进程间的通信与并行组合进行推理。该逻辑已在Isabelle/HOL中形式化并证明为可靠，为HHLPar执行的验证提供了可信基础。HHLPar使用Python实现了混合霍尔逻辑，并支持自动化验证：一方面，它提供符号化分解HCSP进程的功能，为独立的顺序进程生成规约，再通过同步组合得到整个并行HCSP进程的最终规约；另一方面，它集成了外部求解器以处理微分方程和实数算术属性。我们通过对简化巡航控制系统的实验验证了该工具的性能。