Predicate Transformer Semantics for Hybrid Systems: Verification Components for Isabelle/HOL

TL;DR

This paper introduces a semantic framework for verifying hybrid systems within Isabelle/HOL, enabling reasoning about system evolutions using differential dynamic logic concepts and formal verification components.

Contribution

It provides a novel semantic foundation and formalization for hybrid system verification in Isabelle/HOL, including verification components and example demonstrations.

Findings

Framework supports reasoning about hybrid system evolutions

Formal Isabelle/HOL implementation of the semantics

Verification components demonstrated on simple examples

Abstract

We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or invariant sets for vector fields. We introduce the semantic foundations of this framework and summarise their Isabelle formalisation as well as the resulting verification components. A series of simple examples shows our approach at work.