Industrial deployment of system engineering methods providing high dependability and productivity

 

Shared Event Composition/Decomposition in Event-B

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.

[img]
Preview
PDF
927Kb

Official URL: http://www.informatik.uni-trier.de/~ley/db/conf/fmco/fmco2010.html

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.

Item Type:Conference or Workshop Item (Paper)
Subjects:Event-B
Methodology > Refinement
Methodology > Composition and reuse
Tool developments > Model construction
Tool developments > Rodin plug-ins
ID Code:399
Deposited By: Renato Silva
Deposited On:16 May 2012 08:21
Last Modified:18 May 2012 14:16

Repository Staff Only: item control page

Deploy-Project - All right reserved