ADVANCE D3.3 Model Composition and Decomposition - Revision history

imported>Asiehsalehi: /* Motivations / Decisions */

2013-09-23T10:48:59Z

Motivations / Decisions

← Older revision		Revision as of 10:48, 23 September 2013
Line 21:		Line 21:

	In the latest version released (v1.2.6) compatible with Rodin v2.8, some bugs are fixed.		In the latest version released (v1.2.6) compatible with Rodin v2.8, some bugs are fixed.

			Composition and decomposition have already been identified as important features for the WP1 and WP2 case studies and they will continue to be evaluated by these WPs.

	== Available Documentation ==		== Available Documentation ==

imported>Nicolas: Fix title levels

2013-08-27T12:37:02Z

Fix title levels

← Older revision		Revision as of 12:37, 27 August 2013
Line 1:		Line 1:
	= Overview =		== 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.<br>		'''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>
Line 7:		Line 7:
	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.		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 ==

	'''Composition'''<br>		'''Composition'''<br>
Line 22:		Line 22:
	In the latest version released (v1.2.6) compatible with Rodin v2.8, some bugs are fixed.		In the latest version released (v1.2.6) compatible with Rodin v2.8, some bugs are fixed.

	= Available Documentation =		== Available Documentation ==

	Documentation for composition is available in:		Documentation for composition is available in:
Line 34:		Line 34:
	* A Survey on Event-B Decomposition<ref name="DecompSurveyPaper">http://e-collection.library.ethz.ch/eserv/eth:5537/eth-5537-01.pdf</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 ==

	'''Composition'''<br>		'''Composition'''<br>
Line 46:		Line 46:
	* Build a list of architectures templates to be used for decomposition according to the number of sub-components to be generated/kind of architecture to be followed/etc.		* Build a list of architectures templates to be used for decomposition according to the number of sub-components to be generated/kind of architecture to be followed/etc.

	= References =		== References ==
	<references/>		<references/>

	[[Category:ADVANCE D3.3 Deliverable]]		[[Category:ADVANCE D3.3 Deliverable]]

imported>Asiehsalehi: /* Planning */

2013-08-22T13:54:24Z

Planning

← Older revision		Revision as of 13:54, 22 August 2013
Line 35:		Line 35:

	= Planning =		= Planning =
	~~{{TODO}}~~
			'''Composition'''<br>
			Support for animation directly over a composed machine is planned. This will allow multiple machine to interact with each other.
			Improvements in usability of the tool will be made.

			'''Decomposition'''<br>
			Although the actual decomposition operation is mature enough, the feeling is that the steps leading to that stage require some additional support. The preparation steps preceding the decomposition usually require some adjustments to the model in order to the decomposition to be beneficial in the following refinements of each generated sub-component. Therefore we aim to:
			* Receive more feedback from the users to improve tool usability.
			* Auto fixing of problems before executing decomposition: building a set of problem templates and respective solutions to be suggested to the modeller before executing decomposition.
			* Build a list of architectures templates to be used for decomposition according to the number of sub-components to be generated/kind of architecture to be followed/etc.

	= References =		= References =

imported>Asiehsalehi: /* Motivations / Decisions */

2013-08-22T13:53:46Z

Motivations / Decisions

← Older revision		Revision as of 13:53, 22 August 2013
Line 11:		Line 11:
	'''Composition'''<br>		'''Composition'''<br>
	While applying composition, properties must be maintained and proofs obligations need to be discharged in order for the ﬁnal result to be considered valid. Since the composition maintains the monotonicity property of the systems, the sub-systems can be reﬁned independently on a further stage, preserving composition properties.<br>		While applying composition, properties must be maintained and proofs obligations need to be discharged in order for the ﬁnal result to be considered valid. Since the composition maintains the monotonicity property of the systems, the sub-systems can be reﬁned independently on a further stage, preserving composition properties.<br>

	In the latest version released (v1.6.1), some bugs are fixed to make it compatible with Rodin v2.8.		In the latest version released (v1.6.1), some bugs are fixed to make it compatible with Rodin v2.8.

Line 19:		Line 20:
	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.		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.

	In the latest version released (v1.2.6)~~, some bugs are fixed to make it~~ compatible with Rodin v2.8.		In the latest version released (v1.2.6) compatible with Rodin v2.8, some bugs are fixed.

	= Available Documentation =		= Available Documentation =

imported>Asiehsalehi at 13:52, 22 August 2013

2013-08-22T13:52:48Z

← Older revision		Revision as of 13:52, 22 August 2013
Line 8:		Line 8:

	= Motivations / Decisions =		= Motivations / Decisions =
	~~{{TODO}}~~
			'''Composition'''<br>
			While applying composition, properties must be maintained and proofs obligations need to be discharged in order for the ﬁnal result to be considered valid. Since the composition maintains the monotonicity property of the systems, the sub-systems can be reﬁned independently on a further stage, preserving composition properties.<br>
			In the latest version released (v1.6.1), some bugs are fixed to make it compatible with Rodin v2.8.

			'''Decomposition'''<br>
			The main goal of Decomposition is to "cut" a model <math>M</math> into sub-models <math>M_1, ..., M_n</math>, 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 <math>MR</math> in a way that guarantees that <math>MR</math> refines <math>M</math>. Note that this particular 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.<br>
			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.

			In the latest version released (v1.2.6), some bugs are fixed to make it compatible with Rodin v2.8.

	= Available Documentation =		= Available Documentation =

imported>Asiehsalehi at 13:49, 22 August 2013

2013-08-22T13:49:34Z

← Older revision		Revision as of 13:49, 22 August 2013
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 =

imported>Nicolas: First draft

2013-07-15T13:35:17Z

First draft

New page

= Overview =
{{TODO}}

= Motivations / Decisions =
{{TODO}}

= Available Documentation =
{{TODO}}

= Planning =
{{TODO}}

= References =
<references/>

[[Category:ADVANCE D3.3 Deliverable]]