HHLPy: Practical Verification of Hybrid Systems using Hoare Logic

arxiv(2023)

引用 2|浏览6
暂无评分
摘要
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.
更多
查看译文
关键词
hybrid systems,hoare logic,practical verification
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络