Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra

Autor:	Ana Cavalcanti, Simon Foster, Jim Woodcock, Kangfeng Ye
Rok vydání:	2018
Předmět:	Kleene algebra Soundness Algebra Algebraic laws Denotational semantics Computer science 020204 information systems Postcondition 0202 electrical engineering electronic engineering information engineering State space 02 engineering and technology State (computer science) Equational theory
Zdroj:	Relational and Algebraic Methods in Computer Science ISBN: 9783030021481 RAMiCS
DOI:	10.1007/978-3-030-02149-8_13
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::6115fffb82bb056e75dd880a1efad4f4 https://doi.org/10.1007/978-3-030-02149-8_13 Zobrazit plný text záznamu