Difference between revisions of "Atomicity Decomposition Plug-in User Guide"

From Event-B
Jump to navigationJump to search
imported>Asiehsalehi
imported>Asiehsalehi
 
(3 intermediate revisions by the same user not shown)
Line 7: Line 7:
  
 
== Installing and Requirements ==
 
== Installing and Requirements ==
 +
 +
=== Requirements ===
 +
The AD plug-in relies on the Epsilon tool suite. Before installing the AD plug-in, perform the below installation steps in order:
 +
 +
* Choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates]. Select and install ''Event-B EMF - Support for Modelling Extensions'' and ''Event-B EMF Framework'' under the ''Frameworks'' category. 
 +
 +
 +
[[Image:EMF.jpg|center]]
 +
 +
 +
* Choose the location URL: Indigo Update Site - [http://download.eclipse.org/releases/indigo http://download.eclipse.org/releases/indigo]. Select and install ''EMF Compare'' under the ''Modeling'' category. 
 +
 +
 +
[[Image:EMFCompare.jpg|center]]
 +
 +
 +
* Add the Epsilon update site available at [http://download.eclipse.org/epsilon/updates/ http://download.eclipse.org/epsilon/updates/]. Select and install ''the Epsilon Core (Incubation)'' and ''Human Usable Texual Notation (Incubation)'' components.
 +
 +
 +
[[Image:Epsilon.jpg|center]]
 +
  
 
=== Setup ===
 
=== 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 ===
+
* Choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates].
* The AD plug-in relies on the Epsilon tool suite. Before installing the AD plug-in, install Epsilon using the Epsilon update site available at [http://download.eclipse.org/epsilon/updates/ http://download.eclipse.org/epsilon/updates/]. Select and install ''the Epsilon Core (Incubation)'' and ''Human Usable Texual Notation (Incubation)'' components.
+
* Select and install the ''Atomicity Decomposition'' feature under the ''Modelling Extensions'' category.
  
  
[[Image:Epsilon.jpg|center]]
+
[[Image:AD.jpg|center]]
  
 
== Creating Flow Diagrams ==
 
== Creating Flow Diagrams ==

Latest revision as of 15:13, 21 August 2012

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 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

Requirements

The AD plug-in relies on the Epsilon tool suite. Before installing the AD plug-in, perform the below installation steps in order:


EMF.jpg



EMFCompare.jpg



Epsilon.jpg


Setup


AD.jpg

Creating Flow Diagrams

First you need to open the machine in the Rose editor by right-clicking on the machine.


Machine rose.jpg


Then a flow can be created:

1. Either for an Event-B machine, when right-clicking on the machine.


Flow machine.jpg


2. Or for a pre-defined leaf, when right-clicking on the leaf.


Flow leaf.jpg


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)


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.


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 Atomicity Decomposition page). This is done by right-clicking on the machine and launch Atomicity Decomposition Transformation -> Transform to Event-B.


AD2B.jpg


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 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.