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 event defining the actual computation steps 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.

, i.e., when the abstract variable should be logically retained

This first paragraph shall identify the involved partners and give an overview of the contribution. In particular, it shall provide answers to the following questions:

• What are the common denominations?
• Is it a new feature or an improvement?
• What is the main purpose?
• Who was in charge?
• Who was involved?

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).