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.