|
|
| (20 intermediate revisions by the same user not shown) |
| Line 1: |
Line 1: |
| [[User:Son]] at '''ETH Zurich''' is in charge of the plug-in.
| | Generic Instantiation tool is developed by Yokohama Research Laboratory, Hitachi Ltd. (YRL), ETH Zurich (ETHZ) and Hitachi India Pvt. Ltd (HIL) for Event-B as a Plug-in for the RODIN platform |
| {{TOCright}} | | {{TOCright}} |
|
| |
|
| Line 7: |
Line 7: |
|
| |
|
| == Installing and Updating == | | == Installing and Updating == |
| The plug-in is available through the main Rodin Update Site under '''Composition and Decomposition''' category. | | The plug-in is available through the following Eclipse update site: '''http://gen-inst.sourceforge.net/updates''' |
|
| |
|
| == News ==
| | More information about the plug-in can be found in the [http://sourceforge.net/projects/gen-inst/files/examples/GI_Plugin_UserGuide_1_0_2.pdf User Guide]. |
| * 11.05.2012: Version 0.2.2 released for Rodin 2.5.*
| |
|
| |
|
| == Technical References ==
| | The project is hosted on sourceforge at the [https://sourceforge.net/p/gen-inst/ project homepage] |
|
| |
|
| == Usage == | | == Change logs == |
| We use a small example to illustrate the usage of the Generic Instantiation plug-in. The archive of the example is available
| | === Version 1.1.0 === |
| [http://www.example.com here], which can be imported into the Rodin platform. The archive contains to projects called ''Channel'' and ''Negotiation''. ''Channel'' is the abtract base project. ''Negotiation'' is the concrete target project: models of ''Channel'' will be instantiated within the contexts of ''Negotiation''.
| | ==== New features ==== |
| | # Proof of Obligation integration to Generic Instantiation file:<br>Axiom replacement<br>Well-Definedness<br> |
| | # PO coloring:<br>Gray scale coloring of already proven PO’s as part of the instantiated Machines |
| | # Navigation functionality for GI file |
| | # Pretty print for GI file |
|
| |
|
| The ''Channel'' project contains the following components:
| | === Version 1.0.3 === |
| * Context ''message_ctx'' contains carrier set ''MESSAGE'' representing the set of possible messages exchanged.
| | ==== Compatibility upgrade ==== |
| [[Image:GenInst-message_ctx.jpg|Context ''message_ctx'']]
| | # Compatibility upgrade for Rodin 3.0.x |
|
| |
|
| * Machine ''channel'' sees ''message_ctx''. The machine specifies transfering of some messages from a sender to a receiver.
| | === Version 1.0.0 === |
| | | ==== (Initial) features ==== |
| * Context ''size_ctx'' contains constant ''channel_size'' representing the maximum number messages allowed in a channel.
| | # Generic Instantiation (GI) files for storing information about generic instantiation. |
| [[Image:GenInst-size_ctx.jpg|Context ''size_ctx'']]
| | # Wizard for creating GI files. |
| | | # Editor for GI files. |
| * Machine ''EO'' sees ''message_ctx'', ''size_ctx'' and refines ''channel''. The machine specifies that the messages are sent ''exactly-one''.
| | # Static checker for GI files. |
| | | # Performing generic instantiation by creating a new project based on a source project and generic instantiation files. |
| * Machine ''EOIO'' sees ''message_ctx'', ''size_ctx'' and refines ''EO''. The machine specifies that messages are sent ''exactly-one'' and ''in-order''.
| |
| | |
| The ''Negotiation'' project contains the following contexts:
| |
| * Context ''bandwidth_ctx'' contains constant ''bandwidth'' representing the bandwidth of the connection between partners
| |
| [[Image:GenInst-bandwidth_ctx.jpg|Context ''bandwidth_ctx'']]
| |
| | |
| * Context ''proposal_ctx'' contains carrier set ''PROPOSAL'' representing the proposals sending between partners, constant ''proposal_size'' representing the size of each proposal, and constant ''package_size'' respresenting the maximum number of proposals within each message.
| |
| | |
| [[Image:GenInst-proposal_ctx.jpg|Context ''proposal_ctx'']]
| |
| | |
| === Instantiation === | |
| We are going to instantiate the development in ''Channel'', in particular the refinement up to ''EOIO'' by instantiating the abstract carrier set ''MESSAGE'' and abstract constant ''channel_size''. Each message contains a number of proposals (no more than ''package_size''), each proposal has the size specified by ''proposal_size''. As a result, we instantiate ''MESSAGE'' by ''POW(PROPOSAL)'' and ''channel_size'' by ''bandwidth / (proposal_size * package_size)''. The instantiation is done via a wizard as follows.
| |
| | |
| * Open the New Wizard Dialog (File/New/Other) and choose Event-B Generic Instantiation.
| |
| [[Image:GenInst-wizard.jpg | Event-B Generic Instantiation]]
| |
| | |
| * The first page of the wizard is for choosing the different components for instantiation.
| |
| # Base machine: The abstract base machine. Choose ''Channel'' as the base project and ''EOIO'' as the base machine. | |
| # Seen contexts: The contexts in the target projects that will be used. Choose ''Negotiation'' as the target project, and select both ''bandwidth_ctx'' and ''proposal_ctx''. Select ''Next'' to go to the next page. | |
| [[Image:GenInst-wizard1.jpg | Choosing components]]
| |
| | |
| * The second page of the wizard is for entering instantiation for carrier sets and constants.
| |
| # Enter ''POW(PROPOSAL)'' for ''MESSAGE'' | |
| # Enter ''bandwidth / (proposal_size * package_size)'' for ''channel_size''
| |
| The expressions will be translated to Event-B mathematical expressions.
| |
| | |
| [[Image:GenInst-wizard2.jpg | Event-B Generic Instantiation]]
| |
| | |
| Select ''Next'' to go to the next page.
| |
| | |
| * The third page of the wizard is for saving the instantiation information for later use. We save the information into a file named ''GenInst''.
| |
| [[Image:GenInst-wizard3.jpg | Save information]]
| |
| | |
| Select ''Finish'' to complete the wizard.
| |
| | |
| * The following components are generated by the wizard.
| |
| # A generic instantiation file named ''GenInst''. | |
| # A context named ''GenInst''.
| |
| # A machine named ''channel''.
| |
| # A machine named ''EO''.
| |
| # A machine named ''EOIO''.
| |
| The machines are copied of the original abstract machines in ''Channel'' with replacement appropriately of the carrier set and constant.
| |
| | |
| [[Image:GenInst-Result1.jpg | Generated components]]
| |
| | |
| | |
| [[Image:GenInst-Result2.jpg | Generated components]]
| |
| | |
| == Additional features to be investigated/implemented ==
| |
| * There is currently no sanity checking for the instantiation. Users need to make sure that their instantiated model can be analysed and proved by Rodin.
| |
Generic Instantiation tool is developed by Yokohama Research Laboratory, Hitachi Ltd. (YRL), ETH Zurich (ETHZ) and Hitachi India Pvt. Ltd (HIL) for Event-B as a Plug-in for the RODIN platform
Introduction
The Generic Instantiation plug-in provides supports for instantiating an Event-B Models by providing concrete values for carrier sets and constants.
Installing and Updating
The plug-in is available through the following Eclipse update site: http://gen-inst.sourceforge.net/updates
More information about the plug-in can be found in the User Guide.
The project is hosted on sourceforge at the project homepage
Change logs
Version 1.1.0
New features
- Proof of Obligation integration to Generic Instantiation file:
Axiom replacement
Well-Definedness
- PO coloring:
Gray scale coloring of already proven PO’s as part of the instantiated Machines
- Navigation functionality for GI file
- Pretty print for GI file
Version 1.0.3
Compatibility upgrade
- Compatibility upgrade for Rodin 3.0.x
Version 1.0.0
(Initial) features
- Generic Instantiation (GI) files for storing information about generic instantiation.
- Wizard for creating GI files.
- Editor for GI files.
- Static checker for GI files.
- Performing generic instantiation by creating a new project based on a source project and generic instantiation files.
