The Refinement Calculus of Reactive Systems

TL;DR

The paper introduces RCRS, a formal framework for modeling, specifying, and verifying reactive systems compositionally, supporting safety, liveness, and non-deterministic behaviors with tool support.

Contribution

It presents a new compositional formalism for reactive systems using property transformers, with symbolic reasoning techniques and a formal Isabelle implementation.

Findings

RCRS can model both safety and liveness properties.

Supports non-deterministic and non-input-receptive systems.

Includes a formal Isabelle proof assistant implementation.

Abstract

The Refinement Calculus of Reactive Systems (RCRS) is a compositional formal framework for modeling and reasoning about reactive systems. RCRS provides a language which allows to describe atomic components as symbolic transition systems or QLTL formulas, and composite components formed using three primitive composition operators: serial, parallel, and feedback. The semantics of the language is given in terms of monotonic property transformers, an extension to reactive systems of monotonic predicate transformers, which have been used to give compositional semantics to sequential programs. RCRS allows to specify both safety and liveness properties. It also allows to model input-output systems which are both non-deterministic and non-input-receptive (i.e., which may reject some inputs at some points in time), and can thus be seen as a behavioral type system. RCRS provides a set of techniques for symbolic computer-aided reasoning, including compositional static analysis and verification. RCRS comes with a publicly available implementation which includes a complete formalization of the RCRS theory in the Isabelle proof assistant.