Atomicity Decomposition

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.