Group refinement plugin
Group refinement
Motivation
According to the Event B refinement laws, new behaviour is introduced by adding new events to a refinement machine. Such new behaviour may correspond to a detalised description of some abstract behaviour especially when a previously atomic state transition has to be explained as a chain of state transitions. To satisfy the refinement relation, new events are only allowed to update new variables. New variables of a machine denote the part of a system state that is not mapped into the state of the abstract system, that is, they characterise a hidden state of a refined system. Since new events cannot be directly related to the abstract behaviour it is necessary to have a housekeeping event that would link the behaviour expressed on the hidden state with the refined abstract behaviour. Since a housekeeping event assigns to abstract variables that are to be ignored at the implementation stage it is clear that a housekeeping event does not contribute to the specification of the system behaviour. In fact, one should see not as a part of a concrete specification but rather an artefact of the refinement relation proof. Confusingly, Event-B does not make a distinction between abstract variables and events retained solely for the needs of the refinement proof and those preserved as an integral part of an overall specification in the incremental development process.
The group refinement plugin modifies the set of refinement laws within a scope of a single refinement step to remove the need for a housekeeping event. It also simplifies the concrete behaviour specification by allowing a user to forgo the variables and invariants necessary to link abstract and concrete behaviour. The intention is not to replace or remove any of the existing refinement laws but rather augment them with a new set of laws to make the overall refinement process more flexible.
One case where one would have to rely on a housekeeping event is the introduction of a loop. In this case, a housekeeping event forces to a modeller to provide a condition summarising the cumulative loop effect which is likely to be more amenable to analysis that a straightforward next-state relation closure.
