creators_name: Silva, Renato creators_name: Butler, Michael creators_id: ras07r@ecs.soton.ac.uk creators_id: mjb@ecs.soton.ac.uk type: conference_item datestamp: 2012-05-16 08:21:11 lastmod: 2012-05-18 14:16:58 metadata_visibility: show title: Shared Event Composition/Decomposition in Event-B ispublished: pub subjects: Event-Bsemantics subjects: Refinement subjects: deploy_method_comp subjects: deploy_tooldev_modelc subjects: deploy_tooldev_rodinplugins full_text_status: public pres_type: paper abstract: 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. date: 2010-11 date_type: completed event_title: Formal Methods for Components and Objects 2010 event_location: Graz, Austria event_dates: November 2010 event_type: conference refereed: TRUE official_url: http://www.informatik.uni-trier.de/~ley/db/conf/fmco/fmco2010.html citation: Silva, Renato and Butler, Michael (2010) Shared Event Composition/Decomposition in Event-B. In: Formal Methods for Components and Objects 2010, November 2010, Graz, Austria. document_url: http://deploy-eprints.ecs.soton.ac.uk/399/1/comp_decomp_paper.pdf