Atomicity Decomposition Plug-in User Guide: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Asiehsalehi No edit summary |
imported>Asiehsalehi No edit summary |
||
| Line 13: | Line 13: | ||
The following steps will guide you through the setup process: | The following steps will guide you through the setup process: | ||
# Start Rodin. | # Start Rodin. | ||
# In the menu choose ''Help'' -> ''Install New Software...'' | # 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] | # 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 ''Atomicity Decomposition'' feature under the ''Atomicity Decomposition'' category, then click the check box | # Select the ''Atomicity Decomposition'' feature under the ''Atomicity Decomposition'' category, then click the check box. | ||
# Click ''Next'', after some time, the ''Install Details'' page appears | # Click ''Next'', after some time, the ''Install Details'' page appears. | ||
# Click ''Next'' and accept the license | # Click ''Next'' and accept the license. | ||
# Click ''Finish'' | # Click ''Finish''. | ||
# A ''Security Warning'' window may appear: click ''OK'' | # A ''Security Warning'' window may appear: click ''OK''. | ||
# Restart Rodin as suggested. | # Restart Rodin as suggested. | ||
| Line 26: | Line 26: | ||
== Creating Flow Diagrams == | == Creating Flow Diagrams == | ||
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 an abstract 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. | |||
== Validating Rules to Follow == | == Validating Rules to Follow == | ||
== Transforming to Event-B == | == Transforming to Event-B == | ||
Revision as of 16:26, 7 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
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.
- Select the Atomicity Decomposition feature under the Atomicity Decomposition 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 Rose Editor Plug-in and EMF Plug-in.
Creating Flow Diagrams
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. |
 |
 |
The following steps will guide you through a combined atomicity decomposition diagram:
- Create an abstract 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.
