Journal
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
Volume 121, Issue -, Pages -Publisher
ELSEVIER SCIENCE INC
DOI: 10.1016/j.jlamp.2021.100681
Keywords
-
Categories
Funding
- CyPhyAssure project, EPSRC grant [EP/S001190/1]
- RoboCalc project, EPSRC [EP/M025756/1]
- Royal Academy of Engineering
- EPSRC [EP/M025756/1] Funding Source: UKRI
Ask authors/readers for more resources
This paper presents an algebraic verification strategy for concurrent reactive programs with a large or infinite state space, involving novel operators and an associated equation theory. The method can calculate denotational semantics of reactive programs, facilitate automated proof, and support iterative programs and parallel composition..
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. (C) 2021 Elsevier Inc. All rights reserved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available