Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL

TL;DR

IsaVODEs delivers a scalable, Isabelle/HOL–based framework for deductive verification of cyber-physical systems by embedding a hybrid modelling language with lens-based stores and nondeterministic state-transformer semantics. It extends differential dynamic logic reasoning with forward boxes and forward diamonds, local reasoning via frames, and automatic proof tactics for differentiation, Lipschitz continuity, and flows, augmented by CAS integrations (Wolfram Engine, SageMath). The approach enables modular verification of ODEs and hybrid programs, supported by new Darboux rules, differential ghosts, and framed Fréchet derivatives to automate invariant reasoning. Extensive evaluation on ARCH22 benchmarks demonstrates competitive automation, substantial proof automation, and practical applicability to pilot-case scenarios like flight dynamics and rocket reachability, while highlighting remaining arithmetic bottlenecks and integration opportunities with CAS tools. Overall, IsaVODEs advances practical, extensible formal verification for CPS by combining rigorous semantic foundations, automation, and CAS-assisted symbolic reasoning within a general-purpose ITP framework.

Abstract

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.

Figures (2)

• Figure 1: Diagrams illustrating the flight dynamics example
• Figure 2: Depiction of the rocket behaviour assuming $m_0>k$

Theorems & Definitions (12)

• Example 1
• Example 2
• Example 3
• Example 4
• Example 5
• Example 6
• Example 7
• Example 8
• Example 9
• Example 10