Difference between revisions of "D23 Pattern Plug-in"

From Event-B
Jump to navigationJump to search
imported>Afuerst
(New page: = 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 enc...)
 
imported>Pascal
 
(11 intermediate revisions by 2 users not shown)
Line 1: Line 1:
 
= Overview =
 
= 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.
+
The pattern plug-in enables an Event-B developer to make advantage of former models and their refinements.
  
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. With 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.
+
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 =
 
= Motivations =
 
The idea of patterns and their usage is described in every detail in the Master Thesis [http://e-collection.ethbib.ethz.ch/view/eth:41612 "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 [http://www.springerlink.com/content/d088h53531x7226j "Using Design Patterns in Formal Methods: An Event-B Approach"].
 
The idea of patterns and their usage is described in every detail in the Master Thesis [http://e-collection.ethbib.ethz.ch/view/eth:41612 "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 [http://www.springerlink.com/content/d088h53531x7226j "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.
+
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.
  
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.
+
*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 =
 
= 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.
+
*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 programatically. For this the first version of the plug-in was revised by having the generation apart from the pure graphical interface.
+
*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 data object. Certain elements are contained in more than one list dependent to their attributes (e.g. a matched and renamed event).
+
*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).
  
*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.
+
*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 =
 
= Available Documentation =
 
Besides the documents mentioned above focusing on the theory there also exists a wiki page that is more tool related.
 
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 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.
+
:See [http://wiki.event-b.org/index.php/Pattern 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 =
 
= Planning =
  
 
The pattern tool is available as an external plug-in for Rodin release 1.1 and above.
 
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 http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes]
+
:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release Notes] and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].
:and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes].
+
 
 +
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.
 +
 
 
[[Category:D23 Deliverable]]
 
[[Category:D23 Deliverable]]

Latest revision as of 14:43, 27 January 2010

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.

See Rodin Platform 1.1 Release Notes and Rodin Platform 1.2 Release_Notes.

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.