A refinement checking based strategy for component-based systems evolution
This work addresses incremental improvements in formal verification for component-based systems, specifically targeting developers in concurrency and robotics domains.
The authors tackled the problem of verifying behavioral properties during component-based system evolution by proposing inheritance and refinement relations for a CSP-based model, resulting in a mechanized strategy using FDR4 that preserves properties like deadlock freedom, as demonstrated in an autonomous healthcare robot case study.
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.