Pattern

User:afuerst at ETH Zurich is in charge of the Pattern plugin.

Introduction

The intention of Design Patterns in Event-B is to have a methodological approach to reuse former developments (referred to as patterns) in a new development (the problem at hand). With the approach evolved during the master's thesis "Design Patterns in Event-B and Their Tool Support“, the proofs of the pattern can be reused too. It was shown that for the special case of a model that does not see any context and its events do not have any parameters, the generation of a refinement of the problem at hand is correct by construction and no proof obligation needs to be generated.

The correctness of the construction relies on a correct matching of the pattern with the problem at hand. With other words, the correctness of the refinement is implied by the correctness of the matching. The correctness of the matching, on the other hand, is syntactically checked rather than proved. Syntactical checking is easier than doing proofs, especially if they have to be done manually.

Construction of a refinement following the pattern approach

For the construction of reusing a pattern within a development to be correct (without any proof), the pattern and the development have to be matched. This means the elements of the abstract model of a pattern (pattern specification) have to be recognized in the problem at hand (hereinafter referred to as problem).

Example

On the left side is the abstract model of the pattern (pattern specification), on the right side th development where the pattern should be applied. The pattern provides a solution how to realize a communication channel for the transfer of a message. It is going to be applied for the transfer of the question in the development.

Matching

As a first step, all the variables of the pattern specification have to be matched with variables of the problem. Furthermore all the events of the pattern have to be matched with a event of the problem.

In the example the variable matching would be:

transferred → question

And the event matching:

init → init

transfer → question

Checking

The chosen matching is valid for the construction if the following checks turn out to be true. Note that this is only formally proved for models that does not see any context or having events with parameters. The proof of the correctness of the construction with general models is pending.

• Check that the guards of each event of the pattern specification are syntactically the same as the guards of the corresponding event in the problem.

• Check that the actions of each event of the pattern specification are syntactically the same as the actions of the corresponding event in the problem.

• Check that no event in the problem that is not matched alters a matched variable.

Syntactically the same means for example:

$a\bcmeq a+b$ is the same as $c\bcmeq c+d$, if $a$ is matched with $c$, and $b$ is matched with $d$.

The checks for the above example would be:

for the matching init → init

check if $transferred\bcmeq 0$ is syntactically the same as $question\bcmeq 0$

for the matching transfer → question

check if $transferred\bcmeq transferred+1$ is syntactically the same as $question\bcmeq question+1$

Note that there is no guard in the pattern event transfer. The guard $question=response$ acts therefore as an extra guard.

As there are usually multiple guards and action in an event, the user has (at the current state of the tool) to declare which guards and actions go together.

Incorporation

Once all checks are done, the refinement of the problem is generated by merging the pattern refinement with the problem.

Here is an overview of the refinement of the pattern example:

The following incorporation steps have to be done:

• Merge the variables from the pattern refinement with the not-matched variables from the problem.
• Copy the invariants from the pattern refinement.
• Extract the glueing invariants out of the invariants from the pattern refinement.
• Copy all not-matched events from the problem.
• Copy all new events from the pattern refinement.
• Merge all events from the pattern refinement that refine a matched event with the related extra guards and extra actions from the problem event.

The extraction of the gluing invariant is needed, if a variable from the pattern specification is refined in the pattern refinement and therefore disappears. By incorporating the pattern the variable in the problem that is matched to the disappearing variable will also disappear. References to this variable in predicates and assignments in the problem have to be replaced by the expression extracted from the gluing invariants.

In the example, the variable $question$ is matched with $transferred$. $transferred$, on the other hand, is refined by $sent$ as it can be seen in the invariants. Therefore, all appearances of $question$ in the problem events (e.g. event respond) have to be replaced by $sent$.

It might be necessary to rename some of the variables, if a variable name of the pattern refinement already exists in the problem. Renaming could also be used in general to give the variables a more meaningful name. The same applies for the event names.

In the example, the variables are renamed as follows:

sent → sent_question

channel → channel_question

received → received_question

The events are renamed as follow:

send → send_question

receive → receive_question

The result of the incorporation in the example would the be:

Tool support

To support developers in using patterns, there exists a plug-in for Rodin. A first try-out version of the tool is available at the location _exploratory/fuersta/ch.ethz.eventb.pattern within the svn-trunk.

Starting the plug-in

• The pattern wizard is started with File → New → Other... (or just clicking on the New button) and then choosing in the New dialog the Event-B Pattern wizard in section Event-B.

• Click Next to proceed to the matching page.

Matching page

• Choose the pattern and the problem project and machine. If a file was selected before starting the wizard, the tool tries to set it as problem machine.

• In the variable section, add variable matchings by choosing a pattern and a problem variable from the drop down menu and click on the Add Matching button. All matchings are listed in the text field below. A matching can be removed by selecting it and clicking on the Remove button.

• In the event section, add event matchings by choosing a pattern and a problem event from the drop down menu and click on the Add Matching button. All matchings are listed in the text field below. A matchings can be removed by selecting it and clicking on the Remove button. The matching of the INITIALISATION events is set by default and cannot be removed.

• There is a section for setting the context matchings. For each carrier set and each constant of the context seen by the pattern specification a correspondent can be entered. If there is a context seen by the problem the possible choices are listed in a drop down menu. Alternatively an expression can be entered. This might be necessary if a carrier set has to be matched with a default carrier set such as BOOL or INT. Although the tool is capable of dealing with context, it's not part of the proved construction.

• For the checking of the guards and actions, it is needed (in the current version of the tool) to declare which guard/action of the pattern event goes together with which guard/action of the corresponding problem event. This sub-matchings are set in a dialog that opens when double clicking on a existing event-matching in the text field of the event section.

• Enter for the guards and actions the sub-matchings in the same way as done for the variables and events. Note that there is also the possibility of matching the parameters. If you use this option, be aware of the fact that, although the generation works, parameters are not part of the proved construction.

• Click on OK to return to the wizard. The added sub-matchings are displayed in the text field of the event section.

• In the option section, it can be set if all variables and events as well as all of their guards and action have to be matched. This is a condition for the correctness of the construction. If no proof obligations are generated this option should be enabled. There are situations where not all guards can be matched, e.g. if the corresponding guard in the problem event does not exist because it is implied by another guard. In this case the problem event should be adapted. But since the wizard (in the current version) has to be aborted in order to adapt the machine there is this option.

• If there are no errors in the matching the Next button is enabled to proceed to the next step.

Checking page

• At the moment, the checking of the sub-matchings is done by clicking the confirmation box at the bottom. The idea for a later version of the tool is to have a checker that controls the entered sub-matchings.

• If the confirmation box is ticked, the Next button is enabled to proceed to the next step.

Renaming page

• For every variable and every event of the pattern refinement that is copied to the generated problem refinement, a name can be chosen. For every item a name is proposed. If the pattern variable was matched with the problem, the original name within the problem machine is proposed. If the pattern event refines a matched event, the original name within the problem machine is proposed.

• Otherwise the name within the pattern refinement is proposed.

• In the case of more than one problem event being matched with the same pattern event, the pattern events can be distinguished by the name of the matched problem event in the parentheses.

• If there are no duplicate names or names that already exist in the not-matched part of the problem, the Next button is enabled to proceed to the next step.

Incorporating page

• Enter the name for the new problem refinement machine.

• The replacement for disappearing variables have to be set. To extract this information from the gluing invariant all the invariants are listed at the top of the wizard page.

• If there is a witness in an event of the pattern refinement, this witness is used to determine the replacement of the former parameters in the extra guards and extra actions.

• It can be chosen whether the proof obligation should be generated or not.

• If all replacements are set, the Finish button is enables to start the generation of the problem refinement.

• After the generation of the problem refinement, the new machine is opened in an editor.