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.

---

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

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 := a + b$ is the same as $c := c + d$, if $a$ is matched with $c$, and $b$ is matched with $d$.

to be continued......