A refinement checking based strategy for component-based systems evolution

TL;DR

This paper introduces a refinement checking strategy for component-based systems using CSP, enabling safe extensions and evolution while preserving concurrency properties, demonstrated through a healthcare robot case study.

Contribution

It presents inheritance and refinement relations for a CSP-based component model supporting constructive design and extensibility verification with the FDR4 tool.

Findings

Refinement relations preserve deadlock freedom during system evolution.

The strategy enables safe extension of component functionality.

Case study demonstrates practical applicability in healthcare robotics.

Abstract

We propose inheritance and refinement relations for a CSP-based component model (BRIC), which supports a constructive design based on composition rules that preserve classical concurrency properties such as deadlock freedom. The proposed relations allow extension of functionality, whilst preserving behavioural properties. A notion of extensibility is defined on top of a behavioural relation called convergence, which distinguishes inputs from outputs and the context where they are communicated, allowing extensions to reuse existing events with different purposes. We mechanise the strategy for extensibility verification using the FDR4 tool, and illustrate our results with an autonomous healthcare robot case study.