HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
Preprint
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.Keywords
All Related Versions
This publication has 11 references indexed in Scilit:
- A denotational semantics of Simulink with higher-order UTPJournal of Logical and Algebraic Methods in Programming, 2022
- Translating a large subset of stateflow to hybrid CSP with code optimizationJournal of Systems Architecture, 2022
- Predicate Transformer Semantics for Hybrid SystemsJournal of Automated Reasoning, 2021
- Learning safe neural network controllers with barrier certificatesFormal Aspects of Computing, 2021
- Differential Equation Invariance AxiomatizationJournal of the ACM, 2020
- Logical Foundations of Cyber-Physical Systems2018
- A Complete Uniform Substitution Calculus for Differential Dynamic LogicJournal of Automated Reasoning, 2016
- Differential Dynamic Logic for Hybrid SystemsJournal of Automated Reasoning, 2008
- A Framework for Worst-Case and Stochastic Safety Verification Using Barrier CertificatesIEEE Transactions on Automatic Control, 2007
- Notions of computation and monadsInformation and Computation, 1991