Data refinement for true concurrency

TL;DR

This paper introduces an interval-based data refinement framework for modeling and verifying true concurrency in systems, accommodating both discrete and continuous behaviors with sound proof rules.

Contribution

It develops a novel interval-based approach to data refinement that captures true concurrency and non-determinism, extending traditional methods to continuous systems.

Findings

Interval-based encoding of forward simulation

Proof of soundness for the forward simulation rule

Rules for compositional proof decomposition

Abstract

The majority of modern systems exhibit sophisticated concurrent behaviour, where several system components modify and observe the system state with fine-grained atomicity. Many systems (e.g., multi-core processors, real-time controllers) also exhibit truly concurrent behaviour, where multiple events can occur simultaneously. This paper presents data refinement defined in terms of an interval-based framework, which includes high-level operators that capture non-deterministic expression evaluation. By modifying the type of an interval, our theory may be specialised to cover data refinement of both discrete and continuous systems. We present an interval-based encoding of forward simulation, then prove that our forward simulation rule is sound with respect to our data refinement definition. A number of rules for decomposing forward simulation proofs over both sequential and parallel composition are developed.