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(Hybrid Communication Services)相继碎片(HCSP)表达的混合系统提供了一个核查工具,该工具允许对HCSP程序进行说明,附有先决条件和先决条件、变数以及普通差异方程式推理的证明规则。核查条件来自Hoare混合逻辑规则的说明。我们设计了标签和突出机制,以区分和直观不同的核查条件。该工具在Python实施,并有一个基于网络的用户界面。我们评估了Simmlink/ Stateflow模型翻译工具和Keymaera X基准工具的有效性。