D23 Pattern Plug-in
Overview
The pattern plug-in enables an Event-B developer to make advantage of former models and their refinements.
A refinement can also be seen as the solution to the problem encountered in the abstraction. One can make use of such a solution if the solved problem appears in the current development. Instead of solving the problem again we directly use the already known solution. Certainly, we have to show that our current problem (or at least part of it) is the same as the solved problem.
We refer to such a reusable model containing a certain solution to a problem as a pattern. Since these patterns 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 (solved problem).
As mentioned above, the problem at hand (or at least part of it) has to be similar to the 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 (problems) the refinement (solution) of the pattern can be incorporated into the problem at hand. This 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".
There are two main motivations to use patterns.
- Reusing solutions to problems:
- Usually there is more than one solution to a problem. But not every solution is of equal quality. There are solutions that are especially easy, elegant or short. For a lot of problems there is a best practice to solve it. Having a pattern consisting in this "best" solution one does not have to bother finding it ever again.
- Reusing proofs:
- As mentioned above, the pattern approach is able to generate a refinement that is correct by construction. This is possible because the construction of the refinement leads to the same proof obligations as in the pattern. Since they are proved in the pattern there is no need do the same proof steps in the current development again. 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 showed also another motivation to have such a tool. Using the pattern approach without tool support, especially the generation of the refinement, is time consuming and error prone. In this last step in the whole procedure, basically two machines are merged by copying and pasting elements. This 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 whole pattern process, we designed a plug-in providing a graphical wizard that consists in 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 programmatically. 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 central data object. Certain elements are contained in more than one list dependent to their attributes (e.g. a matched and renamed event).
- The correctness of the matching, which is checking the syntactical equality of the matched elements (guards, actions) is left to the developer for the moment. The automation of this was postponed to a later version as it appears to us as a minor point.
- As the pattern plug-in is in a pre-release phase, there is an option to generate the proof obligation in order to control the generation.
Available Documentation
Besides the documents mentioned above focusing on the theory there also exists a wiki page that is more tool related.
- See 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.
The current version of the pattern plug-in covers the following functionalities:
- Interactive guidance for matching the variables.
- Interactive guidance for matching the events and their parameters, guards and actions.
- Collecting the seen contexts in order to enable the user to match the carrier sets and constants.
- Checking for name clashes and proposing possible renaming.
- Detection of disappearing variables that have to be replaced.
- Detection of disappearing parameters that have to be replaced.
- Generation of the new machine file.
Desired functionalities that are missing in the current version:
- Automated syntactical check of the matched elements.
- Automated extraction of the glueing invariants to find the replacement for disappearing variables.
- Automated extraction of the witnesses to find the replacement for disappearing parameters.
The current version has been passed to interested partners for evaluation. The date for the missing functionalities being implemented in the plug-in will depend on the responses of the evaluators and their need of having those functionalities available.
