Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra
share
Reactive programs are ubiquitous in modern applications, and thus verification is highly desirable. We present a verification strategy for infinite-state reactive programs utilising algebraic laws for reactive relations. We define bespoke operators that characterise interactions and state-updates, and an associated equational theory. Our theory can be used to calculate denotational semantics of a reactive program, and thereby facilitate automated proof. Of note is our reasoning support for iterative programs with reactive invariants, which is supported by Kleene algebra. We illustrate our proof strategy by verifying an example reactive program. Our laws and strategy are mechanised in Isabelle/UTP, which provides both soundness guarantees, and practical verification support.
READ FULL TEXT