D32 Teamwork - Revision history

imported>Tommy: /* References */

2010-12-21T11:22:55Z

References

← Older revision		Revision as of 11:22, 21 December 2010
Line 34:		Line 34:
	** Introduction of a graphical interface for decomposition, where the user ''drags and drop'' the elements to the respective sub-component.		** Introduction of a graphical interface for decomposition, where the user ''drags and drop'' the elements to the respective sub-component.

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

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Tommy at 10:21, 20 December 2010

2010-12-20T10:21:49Z

← Older revision		Revision as of 10:21, 20 December 2010
Line 1:		Line 1:
	=== Overview ===		= Overview =
	Teamwork consists of		Teamwork consists of

Line 6:		Line 6:
	* '''Decomposition Plug-in''' was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: ''shared event'' (studied initially by Michael Butler<ref>http://eprints.ecs.soton.ac.uk/16965/</ref><ref>http://eprints.ecs.soton.ac.uk/16910/</ref> ) and ''shared variable'' (studied initially by Jean-Raymond Abrial et al <ref>http://iospress.metapress.com/content/c74274t385t6r72r/</ref> <ref>http://www.inf.ethz.ch/research/disstechreps/techreports/</ref>). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.		* '''Decomposition Plug-in''' was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: ''shared event'' (studied initially by Michael Butler<ref>http://eprints.ecs.soton.ac.uk/16965/</ref><ref>http://eprints.ecs.soton.ac.uk/16910/</ref> ) and ''shared variable'' (studied initially by Jean-Raymond Abrial et al <ref>http://iospress.metapress.com/content/c74274t385t6r72r/</ref> <ref>http://www.inf.ethz.ch/research/disstechreps/techreports/</ref>). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.

	=== Motivations ===		= Motivations =
	Main reasons for implementing teamwork are:		Main reasons for implementing teamwork are:
	* SVN Teamwork		* SVN Teamwork
Line 14:		Line 14:
	: Difficulties in managing complex models (in particular for a large number of proof obligations) fed the idea of decomposing a model in a way that the resulting sub-models could be developed by different individuals. The decomposition process should be seen as a refinement step where the original properties and respective proof obligations should remain valid. With shared event and shared variable decomposition, these requirements are preserved, with the advantage of simplifying the overall development by dealing with sub-parts of the model at once in each sub-model.		: Difficulties in managing complex models (in particular for a large number of proof obligations) fed the idea of decomposing a model in a way that the resulting sub-models could be developed by different individuals. The decomposition process should be seen as a refinement step where the original properties and respective proof obligations should remain valid. With shared event and shared variable decomposition, these requirements are preserved, with the advantage of simplifying the overall development by dealing with sub-parts of the model at once in each sub-model.

	=== Choices / Decisions ===		= Choices / Decisions =
	* SVN Teamwork		* SVN Teamwork
	: The desired objective of a plug-in that would bring support for Subversion in Rodin was to make a Rodin project compatible with standard SVN interface. Due to nature of the Rodin resource management, in particular the use of Rodin database and non-XMI serialisation, it turned out a hard task. A solution to this difficulty was to provide an alternative serialisation method, that would be compatible with Subversion interface. XMI serialisation has been chosen in the final plug-in, which together with Event-B EMF framework provides a shareable copy of the resources of a Rodin project and takes care of synchronisation between two.		: The desired objective of a plug-in that would bring support for Subversion in Rodin was to make a Rodin project compatible with standard SVN interface. Due to nature of the Rodin resource management, in particular the use of Rodin database and non-XMI serialisation, it turned out a hard task. A solution to this difficulty was to provide an alternative serialisation method, that would be compatible with Subversion interface. XMI serialisation has been chosen in the final plug-in, which together with Event-B EMF framework provides a shareable copy of the resources of a Rodin project and takes care of synchronisation between two.
Line 21:		Line 21:
	: The two styles of decomposition use as criteria of partition two of the most important elements of an Event-B model: variables and events. The plug-in supports the two styles and allows the decomposition through a stepwise wizard or through a ''decomposition file'' (with extension ''.dcp'') that can be stored are re-run whenever necessary. For the shared event decomposition, the user needs to selects which variables are allocated to which sub-component. For the share variable decomposition, the user selects which events with be part of which sub-component. The rest of the sub-component (which is no more than an ordinary machine) is built automatically (after some validations).		: The two styles of decomposition use as criteria of partition two of the most important elements of an Event-B model: variables and events. The plug-in supports the two styles and allows the decomposition through a stepwise wizard or through a ''decomposition file'' (with extension ''.dcp'') that can be stored are re-run whenever necessary. For the shared event decomposition, the user needs to selects which variables are allocated to which sub-component. For the share variable decomposition, the user selects which events with be part of which sub-component. The rest of the sub-component (which is no more than an ordinary machine) is built automatically (after some validations).

	=== Available Documentation ===		= Available Documentation =
	* SVN Team-based development documentation<ref>http://wiki.event-b.org/index.php/Team-based_development</ref>		* SVN Team-based development documentation<ref>http://wiki.event-b.org/index.php/Team-based_development</ref>
	* Decomposition plug-in user guide <ref>http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide</ref>		* Decomposition plug-in user guide <ref>http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide</ref>
Line 27:		Line 27:
	* Decomposition tool for Event-B <ref>http://eprints.ecs.soton.ac.uk/21714/</ref>		* Decomposition tool for Event-B <ref>http://eprints.ecs.soton.ac.uk/21714/</ref>

	=== Planning ===		= Planning =
	This paragraph shall give a timeline and current status (as of 28 Jan 2011).		This paragraph shall give a timeline and current status (as of 28 Jan 2011).

Line 34:		Line 34:
	** Introduction of a graphical interface for decomposition, where the user ''drags and drop'' the elements to the respective sub-component.		** Introduction of a graphical interface for decomposition, where the user ''drags and drop'' the elements to the respective sub-component.

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

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Renato: /* Overview */

2010-11-26T11:52:07Z

Overview

← Older revision		Revision as of 11:52, 26 November 2010
Line 4:		Line 4:
	* '''Team-working Plug-in''' is a new feature developed by University of Southampton in request to industrial partners who required support of Rodin project management and team development using Subversion system. Having this support would bring the benefit of centralised model storage and versioning, as well as parallel development. Despite a few functional limitations, derived by specific nature of the Rodin projects, the implemented plug-in gives support for Subversion-based project sharing and collaborative development.		* '''Team-working Plug-in''' is a new feature developed by University of Southampton in request to industrial partners who required support of Rodin project management and team development using Subversion system. Having this support would bring the benefit of centralised model storage and versioning, as well as parallel development. Despite a few functional limitations, derived by specific nature of the Rodin projects, the implemented plug-in gives support for Subversion-based project sharing and collaborative development.

	* '''Decomposition Plug-in''' was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: ''shared event'' (studied initially by Michael Butler<ref>http://eprints.ecs.soton.ac.uk/16965/</ref><ref>http://eprints.ecs.soton.ac.uk/16910/</ref> ) and ''shared variable'' (studied initially by Jean-Raymond Abrial <ref>http://www.inf.ethz.ch/research/disstechreps/techreports/</ref>). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.		* '''Decomposition Plug-in''' was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: ''shared event'' (studied initially by Michael Butler<ref>http://eprints.ecs.soton.ac.uk/16965/</ref><ref>http://eprints.ecs.soton.ac.uk/16910/</ref> ) and ''shared variable'' (studied initially by Jean-Raymond Abrial et al <ref>http://iospress.metapress.com/content/c74274t385t6r72r/</ref> <ref>http://www.inf.ethz.ch/research/disstechreps/techreports/</ref>). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.

	=== Motivations ===		=== Motivations ===

imported>Renato: /* Overview */

2010-11-26T11:48:18Z

Overview

← Older revision		Revision as of 11:48, 26 November 2010
Line 4:		Line 4:
	* '''Team-working Plug-in''' is a new feature developed by University of Southampton in request to industrial partners who required support of Rodin project management and team development using Subversion system. Having this support would bring the benefit of centralised model storage and versioning, as well as parallel development. Despite a few functional limitations, derived by specific nature of the Rodin projects, the implemented plug-in gives support for Subversion-based project sharing and collaborative development.		* '''Team-working Plug-in''' is a new feature developed by University of Southampton in request to industrial partners who required support of Rodin project management and team development using Subversion system. Having this support would bring the benefit of centralised model storage and versioning, as well as parallel development. Despite a few functional limitations, derived by specific nature of the Rodin projects, the implemented plug-in gives support for Subversion-based project sharing and collaborative development.

	* '''Decomposition Plug-in''' was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: ''shared event'' (studied initially by Michael Butler) and ''shared variable'' (studied initially by Jean-Raymond Abrial). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.		* '''Decomposition Plug-in''' was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: ''shared event'' (studied initially by Michael Butler<ref>http://eprints.ecs.soton.ac.uk/16965/</ref><ref>http://eprints.ecs.soton.ac.uk/16910/</ref> ) and ''shared variable'' (studied initially by Jean-Raymond Abrial <ref>http://www.inf.ethz.ch/research/disstechreps/techreports/</ref>). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.

	=== Motivations ===		=== Motivations ===

imported>Renato: /* Overview */

2010-11-26T11:44:41Z

Overview

← Older revision		Revision as of 11:44, 26 November 2010
Line 1:		Line 1:
	=== Overview ===		=== Overview ===
	Teamwork consists of		Teamwork consists of
	* SVN enabling teamwork plug-in
	* Decomposition methods

			* '''Team-working Plug-in''' is a new feature developed by University of Southampton in request to industrial partners who required support of Rodin project management and team development using Subversion system. Having this support would bring the benefit of centralised model storage and versioning, as well as parallel development. Despite a few functional limitations, derived by specific nature of the Rodin projects, the implemented plug-in gives support for Subversion-based project sharing and collaborative development.

	* ~~Team-working~~ Plug-in is a new feature developed by University of Southampton in request to industrial partners who required support of Rodin project management and team development using Subversion system. Having this support would bring the benefit of centralised model storage and versioning, as well as parallel development. Despite a few functional limitations, derived by specific nature of the Rodin projects, the implemented plug-in gives support for Subversion-based project sharing and collaborative development.		* '''Decomposition Plug-in''' was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: ''shared event'' (studied initially by Michael Butler) and ''shared variable'' (studied initially by Jean-Raymond Abrial). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.

	* Decomposition plug-in was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: ''shared event'' (studied initially by Michael Butler) and ''shared variable'' (studied initially by Jean-Raymond Abrial). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.

	=== Motivations ===		=== Motivations ===

imported>Renato: /* Planning */

2010-11-26T11:43:26Z

Planning

← Older revision		Revision as of 11:43, 26 November 2010
Line 34:		Line 34:

	*Decomposition		*Decomposition
	~~: The next stage of the development for the decomposition~~ plug-~~in will involve the introduction~~ of a graphical interface for decomposition, where the user ''drags and drop'' the elements to the respective sub-component.		** Solve compatibility problems with other plug-ins: Records, Modularisation
			** Introduction of a graphical interface for decomposition, where the user ''drags and drop'' the elements to the respective sub-component.

	=References=		=References=

imported>Renato: /* Planning */

2010-11-26T11:38:46Z

Planning

← Older revision		Revision as of 11:38, 26 November 2010
Line 32:		Line 32:
	=== Planning ===		=== Planning ===
	This paragraph shall give a timeline and current status (as of 28 Jan 2011).		This paragraph shall give a timeline and current status (as of 28 Jan 2011).

			*Decomposition
			: The next stage of the development for the decomposition plug-in will involve the introduction of a graphical interface for decomposition, where the user ''drags and drop'' the elements to the respective sub-component.

	=References=		=References=

imported>Renato: /* Choices / Decisions */

2010-11-26T11:35:59Z

Choices / Decisions

← Older revision		Revision as of 11:35, 26 November 2010
Line 20:		Line 20:
	* SVN Teamwork		* SVN Teamwork
	: The desired objective of a plug-in that would bring support for Subversion in Rodin was to make a Rodin project compatible with standard SVN interface. Due to nature of the Rodin resource management, in particular the use of Rodin database and non-XMI serialisation, it turned out a hard task. A solution to this difficulty was to provide an alternative serialisation method, that would be compatible with Subversion interface. XMI serialisation has been chosen in the final plug-in, which together with Event-B EMF framework provides a shareable copy of the resources of a Rodin project and takes care of synchronisation between two.		: The desired objective of a plug-in that would bring support for Subversion in Rodin was to make a Rodin project compatible with standard SVN interface. Due to nature of the Rodin resource management, in particular the use of Rodin database and non-XMI serialisation, it turned out a hard task. A solution to this difficulty was to provide an alternative serialisation method, that would be compatible with Subversion interface. XMI serialisation has been chosen in the final plug-in, which together with Event-B EMF framework provides a shareable copy of the resources of a Rodin project and takes care of synchronisation between two.

			* Decomposition
			: The two styles of decomposition use as criteria of partition two of the most important elements of an Event-B model: variables and events. The plug-in supports the two styles and allows the decomposition through a stepwise wizard or through a ''decomposition file'' (with extension ''.dcp'') that can be stored are re-run whenever necessary. For the shared event decomposition, the user needs to selects which variables are allocated to which sub-component. For the share variable decomposition, the user selects which events with be part of which sub-component. The rest of the sub-component (which is no more than an ordinary machine) is built automatically (after some validations).

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

imported>Renato: /* Available Documentation */

2010-11-26T11:27:41Z

Available Documentation

← Older revision		Revision as of 11:27, 26 November 2010
Line 25:		Line 25:
	* Decomposition plug-in user guide <ref>http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide</ref>		* Decomposition plug-in user guide <ref>http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide</ref>
	* Event Model decomposition for shared variable approach <ref>http://wiki.event-b.org/index.php/Event_Model_Decomposition</ref>		* Event Model decomposition for shared variable approach <ref>http://wiki.event-b.org/index.php/Event_Model_Decomposition</ref>
			* Decomposition tool for Event-B <ref>http://eprints.ecs.soton.ac.uk/21714/</ref>

	=== Planning ===		=== Planning ===

imported>Renato: /* Available Documentation */

2010-11-26T11:14:43Z

Available Documentation

← Older revision		Revision as of 11:14, 26 November 2010
Line 23:		Line 23:
	=== Available Documentation ===		=== Available Documentation ===
	* SVN Team-based development documentation<ref>http://wiki.event-b.org/index.php/Team-based_development</ref>		* SVN Team-based development documentation<ref>http://wiki.event-b.org/index.php/Team-based_development</ref>
			* Decomposition plug-in user guide <ref>http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide</ref>
			* Event Model decomposition for shared variable approach <ref>http://wiki.event-b.org/index.php/Event_Model_Decomposition</ref>

	=== Planning ===		=== Planning ===