Implementing dynamic aggregations of abstract machines in the B method

We previously defined an extension to the B method to be able to dynamically aggregate components. The proposed extension allowed one to build specifications which can create and delete instances of machines at run time, a feature often associated with object oriented languages and not directly supported in the B method. In this paper, we study the refinement of specifications written using this extension. We define a procedure that, given a valid implementation of an abstract machine M, systematically generates an implementation for a machine representing a dynamic aggregation of "instances" of M. Moreover, the generated implementation is guaranteed to be correct by construction. Following the approach initiated in our previous work, the refinement process is defined in a way that is fully compatible with the standard B method.