Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra

TL;DR

This paper introduces an algebraic verification approach for reactive programs with large or infinite state spaces, using reactive relations, novel operators, and Kleene algebra, supported by mechanization in Isabelle/UTP.

Contribution

It presents a new algebraic framework and operators for verifying reactive programs, including iterative ones, with formal soundness guarantees and automation support.

Findings

Successfully verified a reactive buffer example.

Mechanized the verification in Isabelle/UTP for soundness.

Provided a practical algebraic verification strategy for reactive systems.

Abstract

Reactive programs are ubiquitous in modern applications, and so verification is highly desirable. We present a verification strategy for reactive programs with a large or infinite state space utilising algebraic laws for reactive relations. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program's denotational semantics, 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 strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, which provides soundness guarantees, and practical verification support.