Industrial deployment of system engineering methods providing high dependability and productivity


Towards the Composition of Specifications in Event-B

Silva, Renato (2011) Towards the Composition of Specifications in Event-B. In: B 2011 Workshop, 20-24 June 2011, Lero, Limerick, Ireland.


Official URL:


The development of a system can start with the creation of a specification. Following this viewpoint, we claim that often a specification can be constructed from the combination of specifications which can be seen as composition. Event-B is a formal method that allows modelling and refinement of systems. The combination, reuse and validation of component specifications are not currently supported in Event-B. We extend the Event-B formalism using shared event composition as an option for developing (distributed) systems. Refinement is used in the development of specifications using composed machines and we prove that properties and proof obligations of specifications can be reused to ensure valid composed specifications. The main contributions of this work are the Event-B extension to support shared event composition and refinement including the proof obligations for a composed machine.

Item Type:Conference or Workshop Item (Paper)
Methodology > Refinement
Methodology > Composition and reuse
Tool developments > Rodin plug-ins
ID Code:398
Deposited By: Renato Silva
Deposited On:16 May 2012 08:20
Last Modified:18 May 2012 14:17

Repository Staff Only: item control page

Deploy-Project - All right reserved