1 Aarhus University School of Engineering - Software Engineering, Aarhus University School of Engineering, Science and Technology, Aarhus University2 Heinrich Heine Universität Düsseldorf3 Department of Engineering - Software Engineering, Department of Engineering, Science and Technology, Aarhus University4 Department of Engineering - Software Engineering, Department of Engineering, Science and Technology, Aarhus University
When modelling concurrent or distributed systems in Event-B, we often obtain models where the structure of the connected components is specified by constants. Their behaviour is specified by the non-deterministic choice of event parameters for events that operate on shared variables. From a certain point on in a development we would rather develop components separately. The other -behaviourally identical- components should not concern us when we are focusing on one of them. We have to ask the following question: How can we systematically extract "real" components from such a model? These components may still refer to shared variables. Events of these components should not refer to the constants specifying the structure. The non-deterministic choice between these components should not be via parameters. We say the components are reified. We need to address how the reified components get reflected into the original model. This reflection should indicate the constraints on how to connect the components.