imported>Asiehsalehi |
|
| Line 1: |
Line 1: |
| − | == Introduction ==
| |
| − | The Atomicity Decomposition (AD) plug-in allows an explicit representation of control flow and explicit representation of refinement relationships between an abstract event and the corresponding concrete events.
| |
| | | | |
| − | See the [http://wiki.event-b.org/index.php/Atomicity_Decomposition Atomicity Decomposition] page for technical details.
| |
| − |
| |
| − | Currently the AD diagrams can be defined in an EMF tree structure included in an Event-B machine which is opened by Rose editor. After defining the control flow and refinement relationships via AD diagrams, the AD diagrams can automatically transformed to the Event-B notation.
| |
| − |
| |
| − | == Installing and Requirements ==
| |
| − |
| |
| − | === Setup ===
| |
| − | The following steps will guide you through the setup process:
| |
| − | # Start Rodin.
| |
| − | # In the menu choose ''Help'' -> ''Install New Software...''.
| |
| − | # In the ''Work with'' dropdown list, choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates].
| |
| − | # Select the ''Event-B Atomicity Decomposition'' feature under the ''Modelling Extensions'' category, then click the check box.
| |
| − | # Click ''Next'', after some time, the ''Install Details'' page appears.
| |
| − | # Click ''Next'' and accept the license.
| |
| − | # Click ''Finish''.
| |
| − | # A ''Security Warning'' window may appear: click ''OK''.
| |
| − | # Restart Rodin as suggested.
| |
| − |
| |
| − | === Requirements ===
| |
| − | The AD plug-in requires [http://wiki.event-b.org/index.php/Rose_(Structured)_Editor Rose Editor Plug-in] and [http://www.eclipse.org/epsilon/download/ Epsilon framework].
| |
| − |
| |
| − | == Creating Flow Diagrams ==
| |
| − |
| |
| − | First you need to open the machine in the Rose editor by right-clicking on the machine.
| |
| − |
| |
| − | [[Image:machine_rose.jpg]]
| |
| − |
| |
| − | Then a flow can be created:
| |
| − | {|
| |
| − | |-
| |
| − | |1. Either for an Event-B machine, when right-clicking on the machine.
| |
| − | |2. Or for a pre-defined leaf, when right-clicking on the leaf.
| |
| − | |-
| |
| − | | valign="top" | [[Image:flow_machine.jpg|center]]
| |
| − | | valign="top" | [[Image:flow_leaf.jpg|center]]
| |
| − | |}
| |
| − |
| |
| − | The following steps will guide you through a combined atomicity decomposition diagram:
| |
| − | * Create a flow for the most abstract machine.
| |
| − | * When refining a machine, the pre-defined flows are copied to the new (refining) machine.
| |
| − | * In the new machine, you can create a new flow for each pre-defined leaf.
| |
| − |
| |
| − | == Elements and Properties ==
| |
| − |
| |
| − | For each flow, you can define one or more of the below elements, when right-clicking on the flow:
| |
| − | * typed parameter
| |
| − | * leaf
| |
| − | * ''loop'' constructor including one leaf (right-click on the ''loop'')
| |
| − | * ''and'' constructor including two or more leaves (right-click on the ''and'')
| |
| − | * ''or'' constructor including two or more leaves (right-click on the ''or'')
| |
| − | * ''xor'' constructor including two or more leaves (right-click on the ''xor'')
| |
| − | * ''all'' constructor including one leaf and one parameter (right-click on the ''all'')
| |
| − | * ''some'' constructor including one leaf and one parameter (right-click on the ''some'')
| |
| − | * ''one'' constructor including one leaf and one parameter (right-click on the ''one'')
| |
| − |
| |
| − | [[Image:flow_children.jpg]]
| |
| − |
| |
| − | === Flow Properties ===
| |
| − | * Name: a string containing the name of the root event.
| |
| − | * Sw: a boolean indicates strong (''true'') / weak (''false'') sequencing.
| |
| − |
| |
| − | === Leaf Properties ===
| |
| − | * Name: a string containing the name of the event.
| |
| − | * Ref: a boolean indicates refining (''true'') / non-refining (''false'') event.
| |
| − |
| |
| − | [[Image:leaf_properties.jpg]]
| |
| − |
| |
| − | === Constructor Properties ===
| |
| − | * Ref: a boolean indicates refining (''true'') / non-refining (''false'') constructor (''loop'', ''and'' / ''or'' / ''xor'' / ''all'' / ''some'' / ''one'').
| |
| − | NOTE: The refining property for (''loop'' / ''and'' / ''or'' / ''all'' / ''some'') constructors has to be ''false''.
| |
| − |
| |
| − | === Parameter Properties ===
| |
| − | * Name: a string containing the name of the parameter.
| |
| − | * Type: a string containing the type of the parameter.
| |
| − | NOTE: the parameter type has to be defined in the context.
| |
| − |
| |
| − | == Transforming to Event-B ==
| |
| − |
| |
| − | For each machine, after completing the flow construction process, you can perform the translation rules to transform the defined AD flow to the Event-B notation (For technical details see [http://wiki.event-b.org/index.php/Atomicity_Decomposition Atomicity Decomposition] page). This is done by right-clicking on the machine and launch ''Atomicity Decomposition Transformation -> Transform to Event-B''.
| |
| − |
| |
| − | As a result, some read-only event-B elements are generated in order to manage the defined control flow and refinement relationships. User defined event-B elements are allowed; but you can not alter the generated read-only elements.
| |
| − |
| |
| − | == Validation Rules to Follow ==
| |
| − |
| |
| − | In order to perform the translation rules correctly, you will need to follow these rules:
| |
| − | (For more information about technical reasons see [http://wiki.event-b.org/index.php/Atomicity_Decomposition Atomicity Decomposition] page)
| |
| − |
| |
| − | * Rules on the flow:
| |
| − | ** Never change the ''copy'' property of a flow. This is an internal property use to make the internal programming decision.
| |
| − | ** A most abstract flow is a flow with (''sw'' = ''true'') and its children are all non-refining (''ref'' = ''false'').
| |
| − | ** For each non-abstract flow, EXACTLY one refining child (''ref'' = ''true'') has to be defined.
| |
| − | ** Each flow inherits its parameter from its parent flow and parent (''all'' / ''some'' / ''one'') constructor (if exists). This has to be done manually. For each new defined flow, copy and paste all necessary parameters from pre-defined parent flow / constructor.
| |
| − | ** For technical reasons, a ''loop'' constructor never can placed as the first or last child of a flow.
| |
| − |
| |
| − | *Rules on the parameter:
| |
| − | ** The parameter type has to be defined in the context.
| |
| − | ** The parameter name has to be unique.
| |
| − |
| |
| − | * Rules on the constructors:
| |
| − | ** The refining property for (''loop'' / ''and'' / ''or'' / ''all'' / ''some'') constructors has to be ''false''.
| |
| − | ** A constructor leaf inherits its refining property from its parent constructor. For example, for a refining ''xor'' (''ref'' = ''true''), all of its leaves' refining property has to be ''true''. Therefore the (''loop'' / ''and'' / ''or'' / ''all'' / ''some'') children refining property is always ''false''.
| |
