D23 Decomposition - Revision history

imported>Pascal: /* Available Documentation */

2010-01-27T13:27:42Z

Available Documentation

← Older revision		Revision as of 13:27, 27 January 2010
Line 36:		Line 36:
	= Available Documentation =		= Available Documentation =
	The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:		The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:
	* ~~Shared variables (A-style)~~ decomposition specification.		* Event model decomposition specification.
	:See [http://wiki.event-b.org/index.php/Event_Model_Decomposition Event Model Decomposition].		:See [http://wiki.event-b.org/index.php/Event_Model_Decomposition Event Model Decomposition].
	* Decomposition plug-in user's guide.		* Decomposition plug-in user's guide.

imported>Laurent: /* Planning */ Added 1,.3 release

2010-01-27T11:35:55Z

Planning: Added 1,.3 release

← Older revision		Revision as of 11:35, 27 January 2010
Line 43:		Line 43:
	= Planning =		= Planning =
	The decomposition plug-in has been available since release 1.2 of the platform (initial version).		The decomposition plug-in has been available since release 1.2 of the platform (initial version).

			A further version allowing to edit an existing decomposition configuration is planned with release 1.3 of the platform.

	:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release Notes] and [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition Release History].		:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release Notes] and [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition Release History].

	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Laurent: /* Planning */

2010-01-27T11:33:13Z

Planning

← Older revision		Revision as of 11:33, 27 January 2010
Line 42:		Line 42:

	= Planning =		= Planning =
	The decomposition plug-in is available since release 1.2 of the platform (initial version).		The decomposition plug-in has been available since release 1.2 of the platform (initial version).
	:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release Notes] and [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition Release History].		:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release Notes] and [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition Release History].

	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Pascal: /* Planning */

2010-01-26T18:08:57Z

Planning

← Older revision		Revision as of 18:08, 26 January 2010
Line 42:		Line 42:

	= Planning =		= Planning =
	The decomposition plug-in is available since release 1.2 of the platform.		The decomposition plug-in is available since release 1.2 of the platform (initial version).
	:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release Notes] and [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition Release History].		:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release Notes] and [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition Release History].

	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Pascal: /* Planning */

2010-01-08T11:41:54Z

Planning

← Older revision		Revision as of 11:41, 8 January 2010
Line 43:		Line 43:
	= Planning =		= Planning =
	The decomposition plug-in is available since release 1.2 of the platform.		The decomposition plug-in is available since release 1.2 of the platform.
	:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release Notes]		:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release Notes] and [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition Release History].
	:and [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition Release History].

	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Pascal: /* Planning */

2010-01-08T11:41:41Z

Planning

← Older revision		Revision as of 11:41, 8 January 2010
Line 43:		Line 43:
	= Planning =		= Planning =
	The decomposition plug-in is available since release 1.2 of the platform.		The decomposition plug-in is available since release 1.2 of the platform.
	:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes ~~http://wiki~~.~~event-b.org/index.php/Rodin_Platform_1.2_Release_Notes~~].		:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release Notes]
	:and [http://wiki.event-b.org/index.php/Decomposition_Release_History ~~http://wiki.event-b.org/index.php/Decomposition_Release_History~~].		:and [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition Release History].

	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Pascal: /* Available Documentation */

2010-01-08T11:20:58Z

Available Documentation

← Older revision		Revision as of 11:20, 8 January 2010
Line 37:		Line 37:
	The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:		The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:
	* Shared variables (A-style) decomposition specification.		* Shared variables (A-style) decomposition specification.
	:See [~~[Event_Model_Decomposition \|~~ http://wiki.event-b.org/index.php/Event_Model_Decomposition]].		:See [http://wiki.event-b.org/index.php/Event_Model_Decomposition Event Model Decomposition].
	* Decomposition plug-in user's guide.		* Decomposition plug-in user's guide.
	:See [~~[Decomposition_Plug-in_User_Guide \|~~ http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide]].		:See [http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide Decomposition Plug-in User Guide].

	= Planning =		= Planning =

imported>Pascal: /* Motivations */

2010-01-08T11:20:03Z

Motivations

← Older revision		Revision as of 11:20, 8 January 2010
Line 11:		Line 11:
	Therefore, the reﬁnement process entails an increasing complexity of a model, where one has to deal with a growing number of events, state variables, and consequently proof obligations.		Therefore, the reﬁnement process entails an increasing complexity of a model, where one has to deal with a growing number of events, state variables, and consequently proof obligations.
	This is well illustrated in the ''Event build-up'' slide of the Wright presentation during the Rodin Workshop 2009.		This is well illustrated in the ''Event build-up'' slide of the Wright presentation during the Rodin Workshop 2009.
	: See [http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf ~~http://wiki.event~~-~~b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf~~].		: See [http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf Experiences with a Quite Big Event-B Model].

	The purpose of the Event-B model decomposition is precisely to give a way to address such a difficulty, by cutting a large model <math>M</math> into smaller sub-models <math>M_1, ..., M_n</math>. The sub-models can then 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>.		The purpose of the Event-B model decomposition is precisely to give a way to address such a difficulty, by cutting a large model <math>M</math> into smaller sub-models <math>M_1, ..., M_n</math>. The sub-models can then 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>.

imported>Laurent: /* Choices / Decisions */

2010-01-06T15:19:30Z

Choices / Decisions

← Older revision		Revision as of 15:19, 6 January 2010
Line 23:		Line 23:

	= Choices / Decisions =		= Choices / Decisions =
	The main decision concerning the implementation of the Event-B model decomposition in the Rodin platform is to make available both decomposition styles (''shared variables'' ~~vs.~~ ''shared events'') through one single plug-in. These approaches are indeed complementary and the end-user may take advantage of the former or of the latter, depending on the model ~~(eg~~. the ''shared variables'' approach seems more suitable when modelling parallel system and the ''shared events'' approach seems more suitable when modelling message-passing distributed systems).		The main decision concerning the implementation of the Event-B model decomposition in the Rodin platform is to make available both decomposition styles (''shared variables'' and ''shared events'') through one single plug-in. These approaches are indeed complementary and the end-user may take advantage of the former or of the latter, depending on the model, e.g., the ''shared variables'' approach seems more suitable when modelling parallel system and the ''shared events'' approach seems more suitable when modelling message-passing distributed systems.

	Choices, either related to the plug-in core or to the plug-in graphical user interface, have been made with the following constraints in mind:		Choices, either related to the plug-in core or to the plug-in graphical user interface, have been made with the following constraints in mind:
	* Planning. Some options, such as using the Graphical Modelling Framework for the decomposition visualization, or outsourcing the context decomposition, have not been explored (at least in the first instance), mainly because of time constraints (~~according to~~ the DEPLOY description of work, the decomposition support ~~was expected by the~~ end of 2009).		* Planning. Some options, such as using the Graphical Modelling Framework for the decomposition visualization, or outsourcing the context decomposition, have not been explored (at least in the first instance), mainly because of time constraints (in the DEPLOY description of work, the decomposition support is planned for end of 2009).
	* Easy-to-use (however not simplistic) tool. It applies on the one hand to the tool implementation (decomposition wizard, configuration file to replay the decomposition) and on the other hand to the tool documentation (the purpose of the user's guide is to provide useful information for beginners and for more advanced users, in particular through a ''Tips and Tricks'' section).		* Easy-to-use (however not simplistic) tool. It applies on the one hand to the tool implementation (decomposition wizard, configuration file to replay the decomposition) and on the other hand to the tool documentation (the purpose of the user's guide is to provide useful information for beginners and for more advanced users, in particular through a ''Tips and Tricks'' section).
	* Modularity and consistency. In particular, the developments have not been performed in the Event-B core. Instead the Eclipse extension mechanisms have been used to keep the plug-in independent (eg. the static checker, the proof obligation generator and the editor have been extended).		* Modularity and consistency. In particular, the developments have not been performed in the Event-B core. Instead the Eclipse extension mechanisms have been used to keep the plug-in independent (e.g., the static checker, the proof obligation generator and the editor have been extended).
	* Performance.		* Performance. The decomposition tool should perform in reasonable time and memory, compared to other Rodin plug-ins.
	* Recursivity. ~~Thus, it is~~ possible to decompose a previously decomposed model.		* Recursivity. It must be possible to decompose a previously decomposed model.

	Other technical decisions are justified in the specification wiki pages.		Other technical decisions are justified in the specification wiki pages.

imported>Laurent: /* Motivations */ Refactored first paragraph.

2010-01-06T15:14:22Z

Motivations: Refactored first paragraph.

← Older revision		Revision as of 15:14, 6 January 2010
Line 7:		Line 7:

	= Motivations =		= Motivations =
	One of the most important feature of the Event-B approach is the possibility to introduce new events and data~~-refinement of variables~~ during refinement steps.		One of the most important feature of the Event-B approach is the possibility to introduce additional details such as new events and data during refinement steps.

	~~It however results in~~ an increasing complexity of ~~the reﬁnement process when having~~ to deal with ~~many~~ events, ~~many~~ state variables, and consequently ~~many~~ proof obligations.		Therefore, the reﬁnement process entails an increasing complexity of a model, where one has to deal with a growing number of events, state variables, and consequently proof obligations.
	This is well illustrated in the ''Event build-up'' slide of the Wright presentation during the Rodin Workshop 2009.		This is well illustrated in the ''Event build-up'' slide of the Wright presentation during the Rodin Workshop 2009.
	: See [http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf].		: See [http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf].