imported>Afuerst |
|
| Line 1: |
Line 1: |
| − | [[User:afuerst]] at [[ETH Zurich]] is in charge of the [[Pattern]] plugin.
| |
| | | | |
| − |
| |
| − |
| |
| − | The tool can be found in the svn-trunk at location <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern'''</tt>.
| |
| − |
| |
| − | An example including cheat sheet and event-b sources is available at <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern.example'''</tt>.
| |
| − |
| |
| − |
| |
| − |
| |
| − | == 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 [http://e-collection.ethbib.ethz.ch/view/eth:41612 "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 ==
| |
| − |
| |
| − | :[[Image:Pattern_overview.png]]
| |
| − |
| |
| − |
| |
| − | 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.
| |
| − |
| |
| − |
| |
| − | ::[[Image:Pattern_example.png]]
| |
| − |
| |
| − |
| |
| − |
| |
| − | ==== 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:
| |
| − |
| |
| − | <math>a\bcmeq a+b</math> is the same as <math>c\bcmeq c+d</math>, if <math>a</math> is matched with <math>c</math>, and <math>b</math> is matched with <math>d</math>.
| |
| − |
| |
| − |
| |
| − | :The '''checks''' for the above example would be:
| |
| − |
| |
| − | ::for the matching ''init → init''
| |
| − | :::check if <math>transferred\bcmeq 0</math> is syntactically the same as <math>question\bcmeq 0</math>
| |
| − |
| |
| − | ::for the matching ''transfer → question''
| |
| − | :::check if <math>transferred\bcmeq transferred+1</math> is syntactically the same as <math>question\bcmeq question+1</math>
| |
| − |
| |
| − | :Note that there is no guard in the pattern event transfer. The guard <math>question=response</math> 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:
| |
| − |
| |
| − | :[[Image:Pattern_refinement.png]]
| |
| − |
| |
| − |
| |
| − | 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 <math>question</math> is matched with <math>transferred</math>. <math>transferred</math>, on the other hand, is refined by <math>sent</math> as it can be seen in the invariants. Therefore, all appearances of <math>question</math> in the problem events (e.g. event respond) have to be replaced by <math>sent</math>.
| |
| − |
| |
| − |
| |
| − | 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:
| |
| − |
| |
| − | :[[Image:Pattern_incorporation.png]]
| |
| − |
| |
| − |
| |
| − | == 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 <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern'''</tt> within the svn-trunk.
| |
| − |
| |
| − |
| |
| − | There is also an example including cheat sheet and event-b sources available. At <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern.example'''</tt> you find the package. When starting Rodin
| |
| − | including this package you can start the cheat sheet with ''Help'' → ''Cheat Sheets...'' and then selecting ''Other'' → ''Pattern plug-in''.
| |
| − |
| |
| − | In the menu ''Pattern Example'' you can generate machines as an example with the one-click command ''Generate Machine''. The machines are created using the API of the pattern plugin directly without wizard support.
| |
| − |
| |
| − |
| |
| − | For those interested in using the pattern plugin API directly rather than the wizard, the corresponding code snippets are presented at each step.
| |
| − |
| |
| − |
| |
| − | ==== 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'''.
| |
| − |
| |
| − | :[[Image:Pattern_startWizard.jpg]]
| |
| − |
| |
| − |
| |
| − | <span style="color:darkgreen;">// get the Rodin Database</span>
| |
| − | IRodinDB rodinDB = RodinCore.getRodinDB();
| |
| − |
| |
| − | <span style="color:darkgreen;">// get a data instance</span>
| |
| − | IData data = DataFactory.createData();
| |
| − |
| |
| − | ==== 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.
| |
| − |
| |
| − |
| |
| − | :[[Image:Pattern_machineMatching.jpg]]
| |
| − |
| |
| − | <span style="color:darkgreen;">// SET PROBLEM MACHINE</span>
| |
| − | data.changeProblemMachine(problemMachine); <span style="color:darkgreen;">// problemMachine is of type IMachineRoot</span>
| |
| − |
| |
| − | <span style="color:darkgreen;">// SET PATTERN ABSTRACT MACHINE</span>
| |
| − | data.changePatternAbstractMachine(patternAbstractMachine); <span style="color:darkgreen;">// patternAbstractMachine is of type IMachineRoot</span>
| |
| − |
| |
| − |
| |
| − | *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.
| |
| − |
| |
| − | <span style="color:darkgreen;">// SET VARIABLE MATCHINGS</span>
| |
| − | data.addMatching(patternVariable, problemVariable); <span style="color:darkgreen;">// both inputs are of type IVariable</span>
| |
| − |
| |
| − |
| |
| − | *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.
| |
| − |
| |
| − | <span style="color:darkgreen;">// SET EVENT MATCHINGS</span>
| |
| − | data.addMatching(patternEvent, problemEvent); <span style="color:darkgreen;">// both inputs are of type IEvent</span>
| |
| − |
| |
| − |
| |
| − | *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.
| |
| − |
| |
| − | <span style="color:darkgreen;">// SET CONTEXT MATCHINGS</span>
| |
| − | data.updateMatching(carrierSetOrConstant, "PROPOSAL"); <span style="color:darkgreen;">// the first input is of type ICarrierSet or IConstant, the second input is a String</span>
| |
| − |
| |
| − |
| |
| − | :[[Image:Pattern_elementMatching.jpg]]
| |
| − |
| |
| − |
| |
| − | *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.
| |
| − |
| |
| − | <span style="color:darkgreen;">// SET PARAMETERS</span>
| |
| − | data.addMatching(patternParameter, problemParameter); <span style="color:darkgreen;">// both inputs are of type IParameter</span>
| |
| − |
| |
| − | <span style="color:darkgreen;">// SET GUARDS</span>
| |
| − | data.addMatching(patternGuard, problemGuard); <span style="color:darkgreen;">// both inputs are of type IGuard</span>
| |
| − |
| |
| − | <span style="color:darkgreen;">// SET ACTIONS</span>
| |
| − | data.addMatching(patternAction, problemAction); <span style="color:darkgreen;">// both inputs are of type IAction</span>
| |
| − |
| |
| − |
| |
| − | *Click on ''OK'' to return to the wizard. The added sub-matchings are displayed in the text field of the event section.
| |
| − |
| |
| − |
| |
| − | :[[Image:Pattern_submatchingDialog.jpg]]
| |
| − |
| |
| − |
| |
| − | *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.
| |
| − |
| |
| − | *There is the possibility of saving and loading matchings. This is convenient if the models have to be adapted and therefore the wizard has to be closed. The matchings are stored in a file with the name of your choice and the ending ''.pat'' within the current problem project.
| |
| − |
| |
| − |
| |
| − |
| |
| − | :[[Image:Pattern_loadFile.png]]
| |
| − |
| |
| − | ==== 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.
| |
| − |
| |
| − |
| |
| − | :[[Image:Pattern_checking.jpg]]
| |
| − |
| |
| − |
| |
| − | ==== Merging page ====
| |
| − |
| |
| − | ==== 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.
| |
| − |
| |
| − |
| |
| − | :[[Image:Pattern_renaming.jpg]]
| |
| − |
| |
| − | ==== 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.
| |
| − |
| |
| − |
| |
| − | :[[Image:Pattern_incorporation.jpg]]
| |
| − |
| |
| − |
| |
| − | *After the generation of the problem refinement, the new machine is opened in an editor.
| |
| − |
| |
| − |
| |
| − | :[[Image:Pattern_editor.jpg]]
| |
| − |
| |
| − | [[Category:Work in progress]]
| |
| − | [[Category:User Manual]]
| |
| − | [[Category:plugin]]
| |
