Shared variable decomposition. Developing an event model by successive refinements usually starts with very few events (sometimes even a single event) and with a very few state xxxx- xxxxx. On the contrary, it usually ends up with a last refinement step dealing with many events and many variables. This is because one of the most im- portant mechanisms of the Event-B approach consists in introducing new events during refinement steps. The refinement mechanism is also used at the same time to significantly enlarge the number of state variables. At some point, we might have so many events and so many state xxxx- xxxxx that the refinement process might become quite heavy. And we may also figure out that the refinement steps we are trying to undertake are not involving no longer the totality of our system (as was the case at the begin- ning of the development), only a few variables and events are concerned, the others playing a passive role only. The idea of model decomposition is thus clearly very attractive: it con- sists of cutting a large event system into smaller pieces which can be handled more comfortably than the whole. More precisely, each piece should be able to be refined independently of the others. But, of course, the constraint that must be satisfied by this decomposition is that such independently refined pieces could always (in principle) be easily re-composed. This re-composition process should then result in a system which could have been obtained di- rectly without the decomposition, which thus appears to be just a kind of “divide-and-conquer” artefact. But this is clearly not the only interesting methodological outcome of decomposition. It also allows us to build up the architecture of our future system by dividing it into independent components with well defined rela- tionships. Decomposing an event model M is defined as follows:
1. M is split into several sub-models, say N , . . . , P.
2. The events of M are partitioned and the elements of this partition form the events of the sub-models.
3. The variables of model M are also distributed among the sub-models.
4. These sub-models are then refined several times independently yielding eventually NR, . . . , PR.
5. These refined models might be put together to form a re-composed model MR.
6. The re-composed model MR must be guaranteed to be a refinement of It is important to notice here that Point 5 above (the recomposition) will never be performed in practice. One has only to figure out that it can be done and that the re...
Shared variable decomposition. The idea of decomposition is to split a large model into smaller sub-models which can be handled more comfortably than the whole: one should be able to refine these sub- models independently. More precisely, if one starts from an initial (large) model, say M, decomposition allows us to separate this model into several sub-models M1 Mi. These sub-models can then be refined independently yielding N1 Ni. The correctness of the decomposition technique guarantees that the model N, obtained by re-composing N1 Ni, is a refinement of the original model M. This process is illustrated in the following diagram: Decomposition M 8< M1 Refinement Re-composition : Mi N = 1 Ni N ;
