Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra

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.

A UTP Theory Definitions

In this appendix, we summarise our theory of reactive design contracts. The definitions are all mechanised in accompanying Isabelle/HOL reports [12, 13].

1.1 A.1 Observational Variables

We declare two sets and $\varSigma$ that denote the sets of traces and state spaces, respectively, and operators and . We require that forms a trace algebra [19], which is a form of cancellative monoid. Example models include and . We declare the following observational variables that are used in both our UTP theories:

• – indicate divergence in the prior and present relation;

• – indicate quiescence in the prior and present relation;

• – the initial and final state;

• – the trace of the prior and present relation.

Since the theory is extensible, we also allow further observational variables to be added, which are denoted by the variables r and $r'$.

1.2 A.2 Healthiness Conditions

We first describe the healthiness conditions of reactive relations.

Definition A.1

(Reactive Relation Healthiness Conditions).

healthy relations do not refer to ok or wait and have a well-formed trace associated with them. The latter is ensured by the reactive process healthiness conditions [6, 9, 19], and , which justify the existence of the trace pseudo variable . is closed under relational calculus operators , $\vee$, $\wedge$, and , but not , , , or . We therefore define healthy versions below.

Definition A.2

(Reactive Relation Operators).

We define a reactive complement , reactive implication , and reactive true , which with the other connectives give rise to a Boolean algebra [3]. We also define the reactive skip , which is the unit of , and the reactive weakest precondition operator . The latter is similar to the standard UTP definition of weakest precondition [6], but uses the reactive complement.

We next define the healthiness conditions of reactive contracts.

Definition A.3

(Reactive Designs Healthiness Conditions).

states that if the predecessor is waiting then a reactive design behaves like , the reactive design identity. is analagous to from the theory of designs [6, 9], and introduces divergent behaviour: if the predecessor is divergent ($\lnot ok$), then a reactive design behaves like meaning that the only observation is that the trace is extended. is identical to from the theory of designs [6, 9]. states that is a right unit of sequential composition. composes the reactive healthiness conditions and . We then finally have the healthiness conditions for reactive designs: for “stateful reactive designs”, and for“normal stateful reactive designs”.

Next we define the reactive contract operator.

Definition A.4

(Reactive Contracts).

A reactive contract is a “reactive design” [7, 9]. We construct a UTP design [6] using the design turnstile operator, , and then apply to the resulting construction. The postcondition of the underlying design is split into two cases for $wait'$ and $\lnot wait'$, which indicate whether the observation is quiescent, and correspond to the peri- or postcondition.

Finally, we define the healthiness conditions that specialise our theory to stateful-failure reactive designs.

Definition A.5

(Stateful-Failure Healthiness Conditions).

is similar to , but does not refer to ref in the postcondition. If P is healthy then it cannot refer to ref. If P is healthy then the postcondition cannot refer to $ref'$, but the pericondition can: refusals are only observable when P is quiescent [9, 18].