"399","Shared Event Composition/Decomposition in Event-B","The construction of specifications is often a combination of smaller sub-components. Composition and decomposition are techniques that support reuse and allow us to formally combine sub-components through refinement steps while reusing their properties. Sub-components can result from a design or architectural goal and a refinement framework should allow further parallel development over the sub-components. We propose the definition of composition and decomposition in the Event-B formalism following a shared event approach where sub-components interact via synchronisation over shared events and shared states are not allow. We define the necessary proof obligations to ensure a valid composition or decomposition.  We also show that shared event composition preserves refinement proofs for sub-components, that is, in order to maintain refinement of compositions, it is sufficient to prove refinement between corresponding subcomponents.  A case study applying these two techniques is illustrated using Rodin, the Event-B toolset.","http://deploy-eprints.ecs.soton.ac.uk/399/","Silva, Renato and Butler, Michael","UNSPECIFIED","       <span class=\"person_name\">Silva, Renato</span> and <span class=\"person_name\">Butler, Michael</span>     (2010)  <a href=\"http://deploy-eprints.ecs.soton.ac.uk/399/\"><em>Shared Event Composition/Decomposition in Event-B.</em></a>       In: Formal Methods for Components and Objects 2010, November 2010, Graz, Austria.           ","ras07r@ecs.soton.ac.uk,mjb@ecs.soton.ac.uk","2010-11"