TY - UNPB
T1 - Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
AU - Munive, Jonathan Julián Huerta y
AU - Foster, Simon
AU - Gleirscher, Mario
AU - Struth, Georg
AU - Laursen, Christian Pardillo
AU - Hickman, Thomas
N1 - Submitted to the Journal of Automated Reasoning
PY - 2024/1/22
Y1 - 2024/1/22
N2 - We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic foundations of the framework's formalisation in the Isabelle/HOL proof assistant. A user-friendly language specification based on a robust state model makes our framework flexible and adaptable to various engineering workflows. New additions to the framework increase both its expressivity and proof automation. Specifically, formalisations related to forward diamond correctness specifications, certification of unique solutions to ordinary differential equations (ODEs) as flows, and invariant reasoning for systems of ODEs contribute to the framework's scalability and usability. Various examples and an evaluation validate the effectiveness of our framework.
AB - We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic foundations of the framework's formalisation in the Isabelle/HOL proof assistant. A user-friendly language specification based on a robust state model makes our framework flexible and adaptable to various engineering workflows. New additions to the framework increase both its expressivity and proof automation. Specifically, formalisations related to forward diamond correctness specifications, certification of unique solutions to ordinary differential equations (ODEs) as flows, and invariant reasoning for systems of ODEs contribute to the framework's scalability and usability. Various examples and an evaluation validate the effectiveness of our framework.
KW - cs.LO
KW - cs.MS
M3 - Preprint
BT - Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
ER -