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.

翻译：本文提出一个用于验证以HCSP（混合通信顺序进程）顺序片段表达的混合系统的工具。该工具允许为HCSP程序标注前置条件、后置条件、不变量以及常微分方程推理的证明规则。验证条件依据混合霍尔逻辑规则从标注中生成。我们设计了标签与高亮机制来区分并可视化不同验证条件。该工具采用Python实现，并配备基于网页的用户界面。我们通过对Simulink/Stateflow模型翻译实例及KeYmaera X基准测试评估了该工具的有效性。