Atomicity Decomposition: Difference between revisions
imported>Asiehsalehi No edit summary |
imported>Asiehsalehi No edit summary |
||
| (6 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 overview and the AD patterns here: [[ | 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.
