Difference between revisions of "Group refinement plugin"

From Event-B
Jump to navigationJump to search
imported>Alexei
m
imported>Alexei
m
Line 7: Line 7:
 
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.  
 
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.  
  
 +
The approach is best demonstrated by a simple example. The abstract model specifies single event ''swap'' that swaps the values of two variables.
  
[[Abstract.png]]
+
[[Image:Abstract.png]]
 +
 
 +
In the refinement we want to eliminate the case of assigning to two variables at the same time (e.g., the target architecture does not support such an operation). Instead, the swap is modelled using the addition and subtraction operations. The general idea is to introduce a pair of new variables, realise the swap algorithm on these variables, and then use the refinement of event \emph{swap} in the role of a housekeeping event to prove the refinement relation. A refined model takes the following form.
 +
 
 +
[[Image:Normal.png]]
 +
 
 +
The additional ''pc = ...'' invariants are necessary to propagate the information on state evolution through the steps of the algorithm. Without these, it would be impossible to prove the action refinement of ''swap''.
 +
 
 +
Let us now consider an alternative refinement model where there no auxiliary variables and no housekeeping event.
 +
 
 +
[[Image:Groupref.png]]
 +
 
 +
Not shown above but present in the model is the information on the refinement relationship among the \emph{swap\_} and \emph{swap}, and the restriction of the possible traces of \emph{swap\_} events. The latter is necessary as the refinement relationship holds only when \emph{swap1} is followed by \emph{swap2} and the by \emph{swap3}. The traces restriction information is not encoded in the state of the model (that is, by auxiliary variables) but rather taken into the account when generating proof obligations.
  
 
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.
 
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.
 +
 +
=== Installation ===
 +
 +
An alpha version of the plugin is available for the Rodin platform version 1.3.0 or higher. The installation procedure is as follows:
 +
 +
* Go to Help/Software Updates
 +
* Go into Available software tab
 +
* Click Add Site
 +
** the site url is: http://iliasov.org/refplugin
 +
* In the software list window, select the Modelling Extensions category and then Group refinement feature and hit Install
 +
* Go through the dialogs and confirm the platform restart at the end
 +
       
 +
Now you should have the plugin up and running. To start using the plugin, select a refinement machine in the Project Explorer, right-click to open a pop-up menu. At the bottom there should be two new menu items: ''Normal profile'' and ''Group profile''. These options control the current style of refinement lass. The normal profile stands for the standard set fo refinement laws. The group profile activates the additional laws for event group refinement.
 +
 +
[[Category:Plugin]]

Revision as of 14:31, 16 August 2010

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.

The approach is best demonstrated by a simple example. The abstract model specifies single event swap that swaps the values of two variables.

Abstract.png

In the refinement we want to eliminate the case of assigning to two variables at the same time (e.g., the target architecture does not support such an operation). Instead, the swap is modelled using the addition and subtraction operations. The general idea is to introduce a pair of new variables, realise the swap algorithm on these variables, and then use the refinement of event \emph{swap} in the role of a housekeeping event to prove the refinement relation. A refined model takes the following form.

Normal.png

The additional pc = ... invariants are necessary to propagate the information on state evolution through the steps of the algorithm. Without these, it would be impossible to prove the action refinement of swap.

Let us now consider an alternative refinement model where there no auxiliary variables and no housekeeping event.

Groupref.png

Not shown above but present in the model is the information on the refinement relationship among the \emph{swap\_} and \emph{swap}, and the restriction of the possible traces of \emph{swap\_} events. The latter is necessary as the refinement relationship holds only when \emph{swap1} is followed by \emph{swap2} and the by \emph{swap3}. The traces restriction information is not encoded in the state of the model (that is, by auxiliary variables) but rather taken into the account when generating proof obligations.

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.

Installation

An alpha version of the plugin is available for the Rodin platform version 1.3.0 or higher. The installation procedure is as follows:

  • Go to Help/Software Updates
  • Go into Available software tab
  • Click Add Site
  • In the software list window, select the Modelling Extensions category and then Group refinement feature and hit Install
  • Go through the dialogs and confirm the platform restart at the end

Now you should have the plugin up and running. To start using the plugin, select a refinement machine in the Project Explorer, right-click to open a pop-up menu. At the bottom there should be two new menu items: Normal profile and Group profile. These options control the current style of refinement lass. The normal profile stands for the standard set fo refinement laws. The group profile activates the additional laws for event group refinement.