Group refinement plugin

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.

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.

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.

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

Proof Obligations

(todo)

Event Ordering Constraints

In a general case, not all concrete event traces realise a valid refinement of an abstract event. For instance, in the example given above, it necessary to ensure that swap1 takes place before swap2 and, in its turn, swap2 before swap3. One solution is to count the step as it is done in the model with program counter pc. The plugin, however, offers a more elegant mechanism of removing unwanted traces.

To indicate the required event ordering a modeller should provide event ordering constraining expressions. These are places in the comments next to event declarations (in the text editor such comments is placed between event ce and refines ae). The plugin will know that it is an event constrainign expression by seeing double square brackets, e.g., [[first]]. Everything placed within such brackets is considered to be a constraining expressions. No other characters should be placed on the same line before or after brackets (normall comment may follow or precede on other lines in a multi-line comment).

The syntax is following. There are just four keywords: first, next, last and or. A constraining expression takes one of the following forms:

• first: the corresponding event is the first event in the trace
• last: the event is the last event in the trace
• next event (or event)*: the event is followed by a given list of events

In addition, several expressions may be combined with single [[..]] brackets by separating with a semicolon (;). For example

first; next ev1

states that a given event is first and the next event is ev1. Expression

next ev1 or ev2

means that the current event may be followed events ev1 or ev2.

In the example given above, machine m1b has the following event constraining expressions:

• swap1: [[first; next swap2]]
• swap2: none
• swap3: none

Bugs

• witness warning: the plugin does not contribute static checker rules and thus a missing parameter in one of a group refinement events would make the static checker to complain about missing witness