HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
Xiangyu Jin, Bohua Zhan, Shuling Wang and Naijun Zhan
我们提出了一个名为 HHLPar 的工具,用于验证以混合通信顺序过程 (HCSP) 建模的混合系统。 HHLPar建立在HCSP的混合嘶吱逻辑之上,该逻辑学能够推理微分方程的连续时间特性,以及并行HCSP过程的通信和并行组成,并具有参数化痕量计及其同步。 该逻辑在Isabelle/HOL中是正式的,并且被证明是合理的,这构成了HHLPar进行的验证的可信赖的基础。 HHLPar在Python中实现了混合嗤疮逻辑,并支持自动验证:一方面,它提供了符号分解HCSP过程的功能,为单独的顺序过程生成规范,然后通过同步编写它们,以获得整个并行HCSP过程的最终规范;另一方面,它与外部求解器集成,用于处理微分方程和真实算术属性。 我们已经对简化的巡航控制系统进行了实验,以验证该工具的性能。
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 trus...