ADVANCE D3.2 Model Composition and Decomposition - Revision history

imported>Asiehsalehi: /* Available Documentation */

2012-12-11T17:21:58Z

Available Documentation

← Older revision		Revision as of 17:21, 11 December 2012
Line 32:		Line 32:

	Documentation for composition is available in:		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 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>.		* 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:		Documentation for decomposition is available in:

imported>Asiehsalehi: /* Available Documentation */

2012-12-11T17:15:26Z

Available Documentation

← Older revision		Revision as of 17:15, 11 December 2012
Line 39:		Line 39:
	* The decomposition description<ref name="wikiEventModelDecomp">http://wiki.event-b.org/index.php/Event_Model_Decomposition</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 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>.		* 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>Asiehsalehi: /* Available Documentation */

2012-12-11T17:15:09Z

Available Documentation

← Older revision		Revision as of 17:15, 11 December 2012
Line 39:		Line 39:
	* The decomposition description<ref name="wikiEventModelDecomp">http://wiki.event-b.org/index.php/Event_Model_Decomposition</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 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>.		* 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>Tommy: /* Available Documentation */

2012-06-26T10:06:07Z

Available Documentation

← Older revision		Revision as of 10:06, 26 June 2012
Line 32:		Line 32:

	Documentation for composition is available in:		Documentation for composition is available in:
	* an 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 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>.		* a paper: ''Towards the Composition of Specifications in Event-B''<ref name="compPaper"> http://eprints.soton.ac.uk/272177/</ref>.

imported>Tommy: /* Available Documentation */

2012-06-26T10:04:55Z

Available Documentation

← Older revision		Revision as of 10:04, 26 June 2012
Line 33:		Line 33:
	Documentation for composition is available in:		Documentation for composition is available in:
	* an 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>.		* an 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>.		* 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:		Documentation for decomposition is available in:

imported>Tommy: /* Available Documentation */

2012-06-26T10:04:38Z

Available Documentation

← Older revision		Revision as of 10:04, 26 June 2012
Line 32:		Line 32:

	Documentation for composition is available in:		Documentation for composition is available in:

	* an 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>.		* an 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>.		* 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:		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 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>.		* The decomposition description<ref name="wikiEventModelDecomp">http://wiki.event-b.org/index.php/Event_Model_Decomposition</ref>.

imported>Tommy: /* Available Documentation */

2012-06-26T10:04:18Z

Available Documentation

← Older revision		Revision as of 10:04, 26 June 2012
Line 33:		Line 33:
	Documentation for composition is available in:		Documentation for composition is available in:

	* ~~User~~ guide and release history <ref name="wikiParallelComp"> http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B </ref>		* an 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>.
	* Towards the Composition of Specifications in Event-B <ref name="compPaper"> http://eprints.soton.ac.uk/272177/ </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:		Documentation for decomposition is available in:

	* ~~Decomposition~~ user guide <ref name="wikiDecompUserGuide"> http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide </ref>		* The decomposition user guide<ref name="wikiDecompUserGuide">http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide</ref>.
	* ~~Decomposition~~ description <ref name="wikiEventModelDecomp"> http://wiki.event-b.org/index.php/Event_Model_Decomposition </ref>		* The decomposition description<ref name="wikiEventModelDecomp">http://wiki.event-b.org/index.php/Event_Model_Decomposition</ref>.
	* ~~Decomposition~~ Tool for Event-B <ref name="DecompToolPaper"> http://eprints.soton.ac.uk/271714/ </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>		* 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>Tommy: /* Planning */

2012-06-26T10:02:10Z

Planning

← Older revision		Revision as of 10:02, 26 June 2012
Line 45:		Line 45:
	= Planning =		= Planning =

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

	~~== Decomposition ==~~

			'''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:		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.
	* 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.		* 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		* 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>Tommy: /* Motivations / Decisions */

2012-06-26T09:59:46Z

Motivations / Decisions

← Older revision		Revision as of 09:59, 26 June 2012
Line 9:		Line 9:
	= Motivations / Decisions =		= Motivations / Decisions =

	== Composition ==		'''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.5), several features were added to the shared event composition tool:		In the latest version released (v1.5), several features were added to the shared event composition tool:
Line 17:		Line 16:
	*The user interface was improved: using the form-based editor, if the symbol corresponding to a composed event is hovered, a preview of the composed event is displayed		*The user interface was improved: using the form-based editor, if the symbol corresponding to a composed event is hovered, a preview of the composed event is displayed

	== Decomposition ==		'''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.		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.

imported>Tommy: /* Decomposition */

2012-06-26T09:59:01Z

Decomposition

← Older revision		Revision as of 09:59, 26 June 2012
Line 21:		Line 21:
	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.		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.		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 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.3), the user's inputs and request were taken into account. In particular in terms of better usability of the tool. It is worth citing the following modifications:		In the latest version released (v1.2.3), the user's inputs and request were taken into account. In particular in terms of better usability of the tool. It is worth citing the following modifications: