Automated verification of reactive and concurrent programs by calculation

TY - JOUR

T1 - Automated verification of reactive and concurrent programs by calculation

AU - Foster, Simon

AU - Ye, Kangfeng

AU - Cavalcanti, Ana

AU - Woodcock, Jim

N1 - This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy.

PY - 2021/4/14

Y1 - 2021/4/14

N2 - Reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber-physical systems and autonomous robots. In this paper, we present an algebraic verification strategy for concurrent reactive programs, with a large or infinite state space. 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, based on Kleene algebra, and for parallel composition. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, our implementation of Hoare and He's Unifying Theories of Programming (UTP) framework, to provide soundness guarantees and practical verification support.

AB - Reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber-physical systems and autonomous robots. In this paper, we present an algebraic verification strategy for concurrent reactive programs, with a large or infinite state space. 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, based on Kleene algebra, and for parallel composition. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, our implementation of Hoare and He's Unifying Theories of Programming (UTP) framework, to provide soundness guarantees and practical verification support.

KW - cs.LO

KW - cs.PL

UR - http://www.scopus.com/inward/record.url?scp=85104292228&partnerID=8YFLogxK

U2 - 10.1016/j.jlamp.2021.100681

DO - 10.1016/j.jlamp.2021.100681

M3 - Article

SN - 2352-2208

VL - 121

JO - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

M1 - 100681

ER -