论文标题
HHLPY：使用Hoare逻辑对混合系统的实际验证
HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
论文作者
论文摘要
我们提出了一种用于验证在HCSP的顺序片段中表达的混合系统的工具（混合通信顺序过程）。该工具允许用前和后结构，不变性和证明有关普通微分方程的推理的规则来注释HCSP程序。根据混合Hoare逻辑规则，从注释中生成验证条件。我们设计了标签和突出显示机制，以区分和可视化不同的验证条件。该工具在Python中实现，并具有基于Web的用户界面。我们评估了该工具对Simulink/stateFlow模型翻译和Keymaera X基准测试的有效性。
We present a tool for verification of hybrid systems expressed in the sequential fragment of HCSP (Hybrid Communicating Sequential Processes). The tool permits annotating HCSP programs with pre- and postconditions, invariants, and proof rules for reasoning about ordinary differential equations. Verification conditions are generated from the annotations following the rules of hybrid Hoare logic. We designed labeling and highlighting mechanisms to distinguish and visualize different verification conditions. The tool is implemented in Python and has a web-based user interface. We evaluated the effectiveness of the tool on translations of Simulink/Stateflow models and on KeYmaera X benchmarks.
