ADVANCE D3.2 Model Composition and Decomposition

Overview

Composition is the process by which it is possible to combine different sub-systems into a larger system. Known and studied in several areas, this has the advantage of reusability and combination of systems especially when it comes to distributed systems. While applying composition, properties must be maintained and proofs obligations need to be discharged in order for the final result to be considered valid. Since the composition maintains the monotonicity property of the systems, the sub-systems can be refined independently on a further stage, preserving composition properties.

One of the most important feature of the Event-B approach is the possibility to introduce new events during refinement steps, but a consequence is an increasing complexity of the refinement process when having to deal with many events and many state variables. The main goal of Decomposition is to cut a model $M$ into sub-models $M_1, ..., M_n$, which can be refined separately and more comfortably than the whole. The constraint that shall be satisfied by the decomposition is that these refined models might be recomposed into a whole model $MR$ in a way that guarantees that $MR$ refines $M$. Note that this recomposition will never be performed in practice.

• In an shared variable decomposition, the events of a model are partitioned to form the events of the sub-models. In parallel, the variables on which these events act are distributed among the sub-models.
• In an shared event decomposition, the variables of a model are partitioned among the sub-models. Consequently, the events are partitioned accordingly to each sub-model.

Composition and decomposition can be seen as inverse operations: while composition starts with different components that can be assembled together, decomposition starts with a single components that can be partitioned into different components.

Motivations / Decisions

TODO: Fill this paragraph.

Available Documentation

TODO: Fill this paragraph.

Documentation for composition is available in:

• http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B (user guide and release history)
• http://eprints.soton.ac.uk/272177/ (Towards the Composition of Specifications in Event-B)

Documentation for decomposition is available in:

• http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide (user guide)
• http://wiki.event-b.org/index.php/Event_Model_Decomposition (decomposition description)
• http://eprints.soton.ac.uk/271714/ (Decomposition Tool for Event-B)
• http://e-collection.library.ethz.ch/eserv/eth:5537/eth-5537-01.pdf (A Survey on Event-B Decomposition)

Planning

TODO: Fill this paragraph.