Difference between revisions of "Atomicity Decomposition"

From Event-B
Jump to navigationJump to search
imported>Asiehsalehi
(New page: One weakness of Event-B is that control flow between events is typically modelled implicitly via variables and event guards. While this fits well with Event-B refinement, it can make model...)
 
imported>Asiehsalehi
 
(9 intermediate revisions by the same user not shown)
Line 1: Line 1:
 
One weakness of Event-B is that control flow between events is typically modelled implicitly via variables and event guards. While this fits well with Event-B refinement, it can make models involving sequencing of events more difficult to specify and understand than if control flow was explicitly specified. New events may be introduced in Event-B refinement and these are often used to decompose the atomicity of an abstract event into a series of steps. A second weakness of Event-B is that there is no explicit link between such new events that represent a step in the decomposition of atomicity and the abstract event to which they contribute. To address these weaknesses, '''Atomicity Decomposition (AD)''' approach supports the explicit modelling of control flow and refinement relationships for new events.
 
One weakness of Event-B is that control flow between events is typically modelled implicitly via variables and event guards. While this fits well with Event-B refinement, it can make models involving sequencing of events more difficult to specify and understand than if control flow was explicitly specified. New events may be introduced in Event-B refinement and these are often used to decompose the atomicity of an abstract event into a series of steps. A second weakness of Event-B is that there is no explicit link between such new events that represent a step in the decomposition of atomicity and the abstract event to which they contribute. To address these weaknesses, '''Atomicity Decomposition (AD)''' approach supports the explicit modelling of control flow and refinement relationships for new events.
  
You can find the AD background and the AD patterns [[Image:Atomicity_Decomposition.pdf]].
+
You can find the AD overview and the AD patterns here: [[Media:Atomicity_Decomposition.pdf]].
 +
 
 +
See the [http://wiki.event-b.org/index.php/Atomicity_Decomposition_Plug-in_User_Guide Atomicity Decomposition Plug-in User Guide] page for tool support details.

Latest revision as of 15:46, 7 August 2012

One weakness of Event-B is that control flow between events is typically modelled implicitly via variables and event guards. While this fits well with Event-B refinement, it can make models involving sequencing of events more difficult to specify and understand than if control flow was explicitly specified. New events may be introduced in Event-B refinement and these are often used to decompose the atomicity of an abstract event into a series of steps. A second weakness of Event-B is that there is no explicit link between such new events that represent a step in the decomposition of atomicity and the abstract event to which they contribute. To address these weaknesses, Atomicity Decomposition (AD) approach supports the explicit modelling of control flow and refinement relationships for new events.

You can find the AD overview and the AD patterns here: Media:Atomicity_Decomposition.pdf.

See the Atomicity Decomposition Plug-in User Guide page for tool support details.