Group refinement: Difference between revisions
imported>Alexili New page: === 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 atomic... |
imported>Alexili No edit summary |
||
| (5 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
=== Overview === | === Overview === | ||
Group refinement plug-in is a tool realising an alternative set of Event-B refinement laws in the Rodin platform. It lets a modeller to switch to differing style of event atomicity refinement for the scope of a single refinement steps. For a certain case of atomicity refinement the alternative laws result in a more natural and compact model with fewer and simpler proof obligations. | |||
The method and the tool were development by Newcastle University. | |||
=== Motivations === | |||
One of the project industrial partners 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 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 a large model. | |||
=== Choices / Decisions === | |||
, | 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 has an atomicity refinement technique where one can refine an atomic action into a loop of new actions. This is general eough to address the problem but, seemingly, the associated proof cost is prohibitively high and there is no evidence that such proofs may be efficiently mechanised. | |||
The challenge was addressed by offering a method that lets a modeller to select an alternative set of refinement laws whenever the identified pattern of refinement is encountered. The new refinement laws are based on a different interpretation of a model: split refinement (a case of event refinement when an abstract event is refined into two or more concrete alternatives) is understood as a refinement into a composite event made of the concrete events arranged in some way. One simple arrangement case is when the concrete events are understood to execute sequentially. Then the refinement relation is demonstrated for the after-state produced by executing one event after another. | |||
The method is not limited to sequential composition and there is also a form of parallel composition. An essential property of the method is that the group refinement relation is demonstrated not just for a single arrangement of concrete events but for a whole set of traces of concrete events. There is a simple notation for the removal of undesired traces and constraining the model to specific traces. For each trace there appears one instance of action simulation proof obligation (and possibly other refinement and consistency proof obligations). Thus, for practical reasons, it is necessary to keep number of traces low. This is best accomplished by doing small refinement steps with few concrete events. | |||
=== Available Documentation === | === Available Documentation === | ||
The method is still in development. In particular, its formal foundations need careful study as to demonstrate the soundness of the new refinement laws and give an argument for the soundness of a development mixing normal and group refinement laws. A DEPLOY project member may study the use of group refinement in the setting of a realistic case study by examining the cruise control model. There is a wiki page - [[Group refinement plugin]] - briefly introducing the approach and the tool. | |||
=== Planning === | === Planning === | ||
The immediate plan is to produce a technical report on the semantics of group refinement during the first quarter of 2011. Long term plans are the tool maintenance and the investigation of the possibility of more expressive form of group refinement permitting branches and loops. | |||
Latest revision as of 23:20, 6 December 2010
Overview
Group refinement plug-in is a tool realising an alternative set of Event-B refinement laws in the Rodin platform. It lets a modeller to switch to differing style of event atomicity refinement for the scope of a single refinement steps. For a certain case of atomicity refinement the alternative laws result in a more natural and compact model with fewer and simpler proof obligations.
The method and the tool were development by Newcastle University.
Motivations
One of the project industrial partners 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 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 a large model.
Choices / Decisions
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 has an atomicity refinement technique where one can refine an atomic action into a loop of new actions. This is general eough to address the problem but, seemingly, the associated proof cost is prohibitively high and there is no evidence that such proofs may be efficiently mechanised.
The challenge was addressed by offering a method that lets a modeller to select an alternative set of refinement laws whenever the identified pattern of refinement is encountered. The new refinement laws are based on a different interpretation of a model: split refinement (a case of event refinement when an abstract event is refined into two or more concrete alternatives) is understood as a refinement into a composite event made of the concrete events arranged in some way. One simple arrangement case is when the concrete events are understood to execute sequentially. Then the refinement relation is demonstrated for the after-state produced by executing one event after another.
The method is not limited to sequential composition and there is also a form of parallel composition. An essential property of the method is that the group refinement relation is demonstrated not just for a single arrangement of concrete events but for a whole set of traces of concrete events. There is a simple notation for the removal of undesired traces and constraining the model to specific traces. For each trace there appears one instance of action simulation proof obligation (and possibly other refinement and consistency proof obligations). Thus, for practical reasons, it is necessary to keep number of traces low. This is best accomplished by doing small refinement steps with few concrete events.
Available Documentation
The method is still in development. In particular, its formal foundations need careful study as to demonstrate the soundness of the new refinement laws and give an argument for the soundness of a development mixing normal and group refinement laws. A DEPLOY project member may study the use of group refinement in the setting of a realistic case study by examining the cruise control model. There is a wiki page - Group refinement plugin - briefly introducing the approach and the tool.
Planning
The immediate plan is to produce a technical report on the semantics of group refinement during the first quarter of 2011. Long term plans are the tool maintenance and the investigation of the possibility of more expressive form of group refinement permitting branches and loops.
