Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra

TY - GEN

T1 - Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra

AU - Foster, Simon David

AU - Ye, Kangfeng

AU - Cavalcanti, Ana Lucia Caneca

AU - Woodcock, JAMES Charles Paul

N1 - © 2018, Springer Nature Switzerland AG. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.

PY - 2018/11/1

Y1 - 2018/11/1

N2 - 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.

AB - 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.

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

U2 - 10.1007/978-3-030-02149-8_13

DO - 10.1007/978-3-030-02149-8_13

M3 - Conference contribution

SN - 9783030021481

VL - 11194

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 205

EP - 224

BT - Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Proceedings

A2 - Guttmann, Walter

A2 - Desharnais, Jules

A2 - Joosten, Stef

PB - Springer

ER -