Modular Data Refinement.

Modularity and refinement are two important software engineering concepts. Modularity is essential for maintaining intellectual control over complex systems by breaking them into loosely coupled subsystems. Refinement is a systematic approach that gradually transforms a specification into a working system while ensuring correctness at each step. Unfortunately, modularity and refinement have an uneasy relationship with each other, as the operators used to describe a system model in a modular way are generally nonmonotonic with respect to refinement. In this work we present a useful technique and the necessary conditions to ensure that data refinement is monotonic with respect to conjunction. The essential idea is to represent all system operations using a smaller set of operations (kernel) that do not interfere with each other. It is then possible to refine the entire system by refining just the kernel. We demonstrate this technique with a simple example and refer to a larger case study in which this technique was applied to a model of a real-world application.