HHLPy: Practical Verification of Hybrid Systems using Hoare Logic

TL;DR

This paper introduces HHLPy, a Python-based web tool for verifying hybrid systems using Hoare logic, supporting annotations and visualization to facilitate reasoning about differential equations and system properties.

Contribution

The paper presents a practical verification tool for hybrid systems based on hybrid Hoare logic, with visualization features and evaluation on real-world models and benchmarks.

Findings

Effective verification of hybrid systems demonstrated on Simulink/Stateflow models

Visualization aids understanding and debugging of verification conditions

Tool supports reasoning about differential equations in hybrid systems

Abstract

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.