Difference between revisions of "ADVANCE D3.3 Model Composition and Decomposition"

From Event-B
Jump to navigationJump to search
imported>Nicolas
(First draft)
 
imported>Asiehsalehi
Line 1: Line 1:
 
= Overview =
 
= Overview =
−
{{TODO}}
+
 
 +
'''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 re-usability and combination of systems especially when it comes to distributed systems.<br>
 +
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.<br>
 +
 
 +
'''Model decomposition''' is a powerful technique to scale the design of large and complex systems. It enables first developers to separate components development from the concerns of their integration and orchestration. Moreover, it tackles the complexity problem mentioned above, since decomposition allows the partitioning the complexity of the original model into separated components. This allows a decomposed part of the model to be treated as an independent artifact so that the modeller can concentrate on this part and does not have to worry about the other parts.<br>
 +
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 =
 
= Motivations / Decisions =
Line 6: Line 11:
  
 
= Available Documentation =
 
= Available Documentation =
−
{{TODO}}
+
 
 +
Documentation for composition is available in:
 +
* A user guide and release history on the Event-B wiki<ref name="wikiParallelComp"> http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B </ref>.
 +
* A paper: ''Towards the Composition of Specifications in Event-B''<ref name="compPaper"> http://eprints.soton.ac.uk/272177/</ref>.
 +
 
 +
Documentation for decomposition is available in:
 +
* The decomposition user guide<ref name="wikiDecompUserGuide">http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide</ref>.
 +
* The decomposition description<ref name="wikiEventModelDecomp">http://wiki.event-b.org/index.php/Event_Model_Decomposition</ref>.
 +
* A paper on the decomposition Tool for Event-B<ref name="DecompToolPaper">http://eprints.soton.ac.uk/271714/</ref>.
 +
* A Survey on Event-B Decomposition<ref name="DecompSurveyPaper">http://e-collection.library.ethz.ch/eserv/eth:5537/eth-5537-01.pdf</ref>.
  
 
= Planning =
 
= Planning =

Revision as of 13:49, 22 August 2013

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 re-usability and combination of systems especially when it comes to distributed systems.
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.

Model decomposition is a powerful technique to scale the design of large and complex systems. It enables first developers to separate components development from the concerns of their integration and orchestration. Moreover, it tackles the complexity problem mentioned above, since decomposition allows the partitioning the complexity of the original model into separated components. This allows a decomposed part of the model to be treated as an independent artifact so that the modeller can concentrate on this part and does not have to worry about the other parts.
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

Available Documentation

Documentation for composition is available in:

  • A user guide and release history on the Event-B wiki[1].
  • A paper: Towards the Composition of Specifications in Event-B[2].

Documentation for decomposition is available in:

  • The decomposition user guide[3].
  • The decomposition description[4].
  • A paper on the decomposition Tool for Event-B[5].
  • A Survey on Event-B Decomposition[6].

Planning

TODO

References

  1. ↑ http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B
  2. ↑ http://eprints.soton.ac.uk/272177/
  3. ↑ http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide
  4. ↑ http://wiki.event-b.org/index.php/Event_Model_Decomposition
  5. ↑ http://eprints.soton.ac.uk/271714/
  6. ↑ http://e-collection.library.ethz.ch/eserv/eth:5537/eth-5537-01.pdf
Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.3_Model_Composition_and_Decomposition&oldid=536’