Group refinement

Overview

One of the project industrial partners (Bosch) has identified a recurring refinement pattern that did not fit well the existing laws of refinement. It is a case of atomicity refinement where a previously atomic action (event) is split into a number of steps which combined effect achieves the effect of the abstract atomic event. The Event-B approach is to introduce new variables in a refinement machine and thus have a hidden concrete state on which the steps are defined. There is a further event summarising the effect of the computations accomplished on the hidden state and explicitly relating it to the abstract state. This is the event for which the refinement relation is demonstrated while the events defining the actual computation steps would have no formal link to the abstract event.

When the hidden state does not naturally follow as a part of the modelling process this refinement style leads to a contrived model. There appear auxiliary variables and auxiliary events that play no part in the characterisation of the system behaviour but rather are a codification of the refinement relation to an abstract model. Since such elements accumulate during refinement this has a profound effect on the development of large model.

In addressing this problem, one obvious source of inspiration is the Classical B method where an abstract atomic statement may be refined into an operation which body is made of a sequence of assignments. However, the introduction of the semicolon operator in Event-B is a substantial change affecting most aspects of the method. This would also reintroduce one of the problems of the Classical B that Event-B tries to address: proof scalability. Accumulation of sequential composition through refinement steps may result in unmanageable proof obligations. It is also more difficult to conduct subsequent refinement of events with sequential actions.

Actions Systems exceptionally powerful atomicity refinement technique where one can refine an atomic action into a loop of new actions. The associated proof costs is quite high and there is no evidence that such proofs may be efficiently mechanised.

The challenge was addressed by a method that lets a modeller to select an alternative set of refinement laws whenever the identifier pattern of refinement is encountered. The method and the tool were development by Newcastle University, the pattern of refinement was discovered by the Bosch formal modelling team.

Motivations

This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.

Choices / Decisions

This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.

Available Documentation

This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:

• Requirements.
• Pre-studies (states of the art, proposals, discussions).
• Technical details (specifications).
• Teaching materials (tutorials).
• User's guides.

A distinction shall be made on the one hand between these different categories, and on the other hand between documentation written for developers and documentation written for end-users.

Planning

This paragraph shall give a timeline and current status (as of 28 Jan 2011).