Refining interfaces: the case of the B method

TL;DR

This paper extends the B method's refinement theory to allow signature changes in concrete operations, enhancing practical applicability while maintaining formal guarantees for safety-critical software design.

Contribution

It introduces a method to perform signature modifications within refinement theory, broadening the B method's flexibility without losing its formal correctness guarantees.

Findings

Signature changes are achievable within refinement theory.

The approach preserves the mathematical guarantees of the B method.

Practical application in safety-critical software development is facilitated.

Abstract

Model-driven design of software for safety-critical applications often relies on mathematically grounded techniques such as the B method. Such techniques consist in the successive applications of refinements to derive a concrete implementation from an abstract specification. Refinement theory defines verification conditions to guarantee that such operations preserve the intended behaviour of the abstract specifications. One of these conditions requires however that concrete operations have exactly the same signatures as their abstract counterpart, which is not always a practical requirement. This paper shows how changes of signatures can be achieved while still staying within the bounds of refinement theory. This makes it possible to take advantage of the mathematical guarantees and tool support provided for the current refinement-based techniques, such as the B method.