D23 Pattern Plug-in

Overview

The pattern plug-in enables an Event-B developer to make advantage of former models and their refinements. The refinement, which can be seen as the solution to the problem encountered in the abstraction, can be reused if the abstracted problem is similar to a part of the problem at hand. We call such reusable models to be patterns and since they are just regular models every model can be a pattern in principle. There is only a limit in terms of usability that correlates with the specificity of the model.

As mentioned above, the problem at hand (or at least part of it) has to be similar to pattern we want to use. To ensure this similarity the developer has to match the pattern with the problem at hand. After a successful matching of the models the solution (refinement) of the pattern can be incorporated into the problem at hand which leads to a refinement of this model that is correct by construction. In other words, a new refinement of the problem at hand can be generated which includes the achievements of the pattern and is correct without proving any proof obligation.

Motivations

The idea of patterns and their usage is described in every detail in the Master Thesis "Design Patterns in Event-B and Their Tool Support“. This approach follows the earlier proposal of Jean-Raymond Abrial and Thai Son Hoang stated in the paper "Using Design Patterns in Formal Methods: An Event-B Approach".

The advantage of the pattern approach lies in the "recycling" of proofs. Reusing proofs, especially manual discharged proof obligations, saves a lot of time for the developer. The drawback reflects in the effort to match the pattern with the problem before a refinement can be generated. But this effort can be minimised by a tool that does as many steps as possible automatically or at least supports the developer wherever user interaction is required.

Case studies of using the pattern approach without tool support showed that especially the generation of the refinement is time consuming and error prone. This last step in which basically two machines are merged by copying and pasting elements often leads to name clashes where a developer can easily loose track. Having a tool checking for possible name clashes in advance can avoid a lot of confusion.

Choices / Decisions

• To support the developer and guide him through the hole pattern process we designed a plug-in providing a graphical wizard that consists of several pages, one for each major step.

• It was desired to have direct access to the pattern plug-in in form of an API in addition to the wizard. This enables other Rodin developers to use the pattern plug-in programatically. For this the first version of the plug-in was revised by having the generation apart from the pure graphical interface.

• In order to speed up the process, all required Event-B element of the involved machines are collected in a data object. Certain elements are contained in more than one list dependent to their attributes (e.g. a matched and renamed event).

• Having complementary lists in the data object such as matched and not-matched events and in addition a combination containing all events is surely redundant. On the other hand, does it prevent countless iterations and checks that would be needed to keep the wizard up-to-date?

Available Documentation

Besides the documents mentioned above focusing on the theory there also exists a wiki page that is more tool related.

See http://wiki.event-b.org/index.php/Pattern for a short overview of the idea of patterns in Event-B and stepwise instructions for both developers interested in using the wizard and those more thrilled by APIs.

Planning

The pattern tool is available as an external plug-in for Rodin release 1.1 and above.

See http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes

and http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes.