\textsf{HHLPy}: practical verification of hybrid systems using Hoare logic

DOI10.1007/978-3-031-27481-7_11MaRDI QIDQ6174532zbMATH OpenFDO

Authors Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan

Publication date 17 August 2023

Published in Formal Methods (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2210.17163

zbMATH Keywords

formal verificationHoare logichybrid systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
• Differential dynamic logic for hybrid systems
• scientific article; zbMATH DE number 1905118
• Hybrid Systems: Computation and Control

Cites work

• A complete uniform substitution calculus for differential dynamic logic
• A denotational semantics of simulink with higher-order UTP
• Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
• Bellerophon: tactical theorem proving for hybrid systems
• Dafny: an automatic program verifier for functional correctness
• Differential dynamic logic for hybrid systems
• Differential equation invariance axiomatization
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
• Formal verification of Simulink/Stateflow diagrams
• Formal Verification of Simulink/Stateflow Diagrams
• Guarded commands, nondeterminacy and formal derivation of programs
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Logical foundations of cyber-physical systems
• Notions of computation and monads
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• Verifying hybrid systems with modal Kleene algebra
• Why3 -- where programs meet provers

Cited in

(4)

• Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
• Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
• IsaVODEs: Interactive verification of cyber-physical systems at scale
• Embedding differential dynamic logic in PVS

This page was built for publication: \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174532)