D23 Modularisation Plug-in - Revision history

imported>Pascal: /* Planning */

2010-01-08T11:43:04Z

Planning

← Older revision		Revision as of 11:43, 8 January 2010
Line 52:		Line 52:

	= Planning =		= Planning =
	The plug-in is available since the release 1.1 of the platform. See the [[Modularisation Plug-in Release Notes~~\|release notes]~~].		The plug-in is available since the release 1.1 of the platform. See the [http://wiki.event-b.org/index.php/Modularisation_Plug-in_Release_Notes Modularisation Plug-in Release Notes].

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

imported>Pascal: /* Available Documentation */

2010-01-08T11:38:18Z

Available Documentation

← Older revision		Revision as of 11:38, 8 January 2010
Line 43:		Line 43:
	There is a dedicated wiki page covering the plug-in functionality. Also, we are working on further documentation and tutorial.		There is a dedicated wiki page covering the plug-in functionality. Also, we are working on further documentation and tutorial.

	* [~~[Modularisation Plug~~-in\|Plug-in wiki]]		* [http://wiki.event-b.org/index.php/Modularisation_Plug-in Plug-in wiki]
	* [~~[Modularisation Plug~~-~~in Tutorial\|~~Plug-in tutorial]]		* [http://wiki.event-b.org/index.php/Modularisation_Plug-in_Tutorial Plug-in tutorial]
	* [~~[Modularisation Plug~~-~~in Installation Instructions\|~~Installation guide]]		* [http://wiki.event-b.org/index.php/Modularisation_Plug-in_Installation_Instructions Installation guide]

	Two small-scale examples are available:		Two small-scale examples are available:
	* [[http://iliasov.org/modplugin/ticketmachine.zip]] - A model of queue based on two ticket machine module instantiations (very basic).		* [http://iliasov.org/modplugin/ticketmachine.zip] - A model of queue based on two ticket machine module instantiations (very basic).
	* [[http://iliasov.org/modplugin/doors.zip]] - Two doors sluice controller specification that is decomposed into a number of independent developments (few first steps only).		* [http://iliasov.org/modplugin/doors.zip] - Two doors sluice controller specification that is decomposed into a number of independent developments (few first steps only).

	= Planning =		= Planning =

imported>Pascal: /* Typos */

2009-12-04T11:36:59Z

Typos

imported>Alexili at 10:28, 18 November 2009

2009-11-18T10:28:55Z

← Older revision		Revision as of 10:28, 18 November 2009
Line 46:		Line 46:
	* [[Modularisation Plug-in Tutorial\|Plugin tutorial]]		* [[Modularisation Plug-in Tutorial\|Plugin tutorial]]
	* [[Modularisation Plug-in Installation Instructions\|Installation guide]]		* [[Modularisation Plug-in Installation Instructions\|Installation guide]]


	Two small-scale examples are available:		Two small-scale examples are available:

imported>Alexili at 10:28, 18 November 2009

2009-11-18T10:28:30Z

← Older revision		Revision as of 10:28, 18 November 2009
Line 43:		Line 43:
	There is a dedicated wiki page covering the plugin functionality. Also, we are working on further documentation and tutorial.		There is a dedicated wiki page covering the plugin functionality. Also, we are working on further documentation and tutorial.

	* [[~~Plugin wiki\|~~Modularisation Plug-in]]		* [[Modularisation Plug-in\|Plugin wiki]]
	* [[~~Plugin tutorial\|~~Modularisation Plug-in Tutorial]]		* [[Modularisation Plug-in Tutorial\|Plugin tutorial]]
	* [[~~Installation guide\|~~Modularisation Plug-in Installation Instructions]]		* [[Modularisation Plug-in Installation Instructions\|Installation guide]]

imported>Alexili at 10:27, 18 November 2009

2009-11-18T10:27:08Z

← Older revision		Revision as of 10:27, 18 November 2009
Line 53:		Line 53:

	= Planning =		= Planning =
			The plugin is available since Platform version 1.1. See the [[Modularisation Plug-in Release Notes\|release notes]].

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

imported>Alexili at 10:25, 18 November 2009

2009-11-18T10:25:22Z

← Older revision		Revision as of 10:25, 18 November 2009
Line 35:		Line 35:
	* During the initial experiments we have identified a need for multiple module instantiation. This allows a modeller to use several copies of the some module using a qualifier prefix to distinguish between objects imported from the modules.		* During the initial experiments we have identified a need for multiple module instantiation. This allows a modeller to use several copies of the some module using a qualifier prefix to distinguish between objects imported from the modules.

	*		* One crucial point was realising modularisation support in such a way that structuring may be recursively applied within modules. Indeed, a module implemenation (module body) is a machine and thus it is self-similar to a caller context that is a machine.

			* For the current version, we have not implemented the generation of enabledness condition logically required for module implementation. This condition, in some form, should be present in the Platform core.

	= Available Documentation =		= Available Documentation =

			There is a dedicated wiki page covering the plugin functionality. Also, we are working on further documentation and tutorial.

			* [[Plugin wiki\|Modularisation Plug-in]]
			* [[Plugin tutorial\|Modularisation Plug-in Tutorial]]
			* [[Installation guide\|Modularisation Plug-in Installation Instructions]]


			Two small-scale examples are available:
			* [[http://iliasov.org/modplugin/ticketmachine.zip]] - a model of queue based on two ticket machine module instantiations (very basic)
			* [[http://iliasov.org/modplugin/doors.zip]] - two doors sluice controller specification that is decomposed into a number of independent developments (few first steps only)

	= Planning =		= Planning =
	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Alexili at 10:16, 18 November 2009

2009-11-18T10:16:29Z

← Older revision		Revision as of 10:16, 18 November 2009
Line 25:		Line 25:
	* Code generation/legacy code		* Code generation/legacy code

			= Choices / Decisions =

			The pimary objective in the tool design was to provide a simple to use tool that could be used by a non-expert modeller. Of course, close integration with the core platform functionality was paramount.

			* We have decided there is a need for a new type of Event-B component: interface. A decomposition based on explicit interface (rather than an implicit one such as in A-style decomposition) facilitates reuse of modules and makes it easier to provider a rich management infrastructure.

			* At some we had to make a decision of whether to make module integration more explicit and flexible or hide details under syntax sugar and thus achieve better model readability. We have decided that model readability should take priority over everything else. However, while model representation becomes more compact, it does not make proofs any easier.

			* During the initial experiments we have identified a need for multiple module instantiation. This allows a modeller to use several copies of the some module using a qualifier prefix to distinguish between objects imported from the modules.

			*

	~~= Choices / Decisions =~~
	= Available Documentation =		= Available Documentation =
	= Planning =		= Planning =
	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Alexili at 10:00, 18 November 2009

2009-11-18T10:00:53Z

@@ Line 7: / Line 7: @@
 = Motivations =
 = Choices / Decisions =
 = Available Documentation =
 = Planning =
 [[Category:D23 Deliverable]]

imported>Alexili at 09:55, 18 November 2009

2009-11-18T09:55:04Z

← Older revision		Revision as of 09:55, 18 November 2009
Line 2:		Line 2:
	Modularisation Plugin realises a support for structuring Event-B developments into modules. The objective is to achieve better structuring of models and proofs while also providing a facility for model reuse. It is expected that the structuring approach realised in the plugin would complement the functionality A/B-style decomposition plugin.		Modularisation Plugin realises a support for structuring Event-B developments into modules. The objective is to achieve better structuring of models and proofs while also providing a facility for model reuse. It is expected that the structuring approach realised in the plugin would complement the functionality A/B-style decomposition plugin.

	The plugin was developed in Newcastle University in cooperation with Abo Academy ~~(Turku)~~ and Space Systems Finland.		The module concept is very close to the notion Event-B development (a refinement tree of Event-B machines). However, unlike a conventional development, a module is equipped with an interface. An interface defines the conditions on the way a module may be incorporated into another development (that is, another module). The plugin follows an approach where an interface is characterised by a list of operations specifying the services provided by the module. An integration of a module into a main development is accomplished by referring operations from Event-B machine actions using an intuitive procedure call notation.

			The plugin was developed in Newcastle University in cooperation with Abo Academy and Space Systems Finland.

	= Motivations =		= Motivations =

← Older revision		Revision as of 11:36, 4 December 2009
Line 1:		Line 1:
	= Overview =		= Overview =
	Modularisation ~~Plugin~~ realises a support ~~for structuring~~ Event-B developments into modules. The objective is to achieve better structuring of models and proofs while also providing a facility for model reuse. It is expected that the structuring approach realised in the ~~plugin~~ would complement the functionality A/B-style decomposition ~~plugin~~.		The Modularisation plug-in realises a support to structure Event-B developments into modules. The objective is to achieve better structuring of models and proofs while also providing a facility for model reuse. It is expected that the structuring approach realised in the plug-in would complement the functionality A/B-style decomposition plug-in.

	The module concept is very close to the notion Event-B development (a refinement tree of Event-B machines). However, unlike a conventional development, a module is equipped with an interface. An interface defines the conditions on the way a module may be incorporated into another development (that is, another module). The ~~plugin~~ follows an approach where an interface is characterised by a list of operations specifying the services provided by the module. An integration of a module into a main development is accomplished by referring operations from Event-B machine actions using an intuitive procedure call notation.		The module concept is very close to the notion of Event-B development (a refinement tree of Event-B machines). However, unlike a conventional development, a module is equipped with an interface. An interface defines the conditions on the way a module may be incorporated into another development (that is, another module). The plug-in follows an approach where an interface is characterised by a list of operations specifying the services provided by the module. An integration of a module into a main development is accomplished by referring operations from Event-B machine actions using an intuitive procedure call notation.

	The ~~plugin~~ was developed in Newcastle University in cooperation with Abo Academy and Space Systems Finland.		The plug-in was developed in Newcastle University in cooperation with Abo Academy and Space Systems Finland.

	= Motivations =		= Motivations =
Line 12:		Line 12:
	One approach to decomposition is to identify a general theory that, once formally formulated, would contribute to the main development. For instance, a model realising a stack-based interpreter could be simplified by considering the stack concept in isolation, constructing a general theory of stacks and then reusing the results in the main development. Thus, an imported theory of stack contributes axioms and theorems assisting in reasoning about stacks.		One approach to decomposition is to identify a general theory that, once formally formulated, would contribute to the main development. For instance, a model realising a stack-based interpreter could be simplified by considering the stack concept in isolation, constructing a general theory of stacks and then reusing the results in the main development. Thus, an imported theory of stack contributes axioms and theorems assisting in reasoning about stacks.

	Decomposition may also be achieved by splitting a system into a number of parts and then proceeding with independent development of each part. At some point, the model parts are recomposed to construct an overall final model. This decomposition style relies on the monotonicity of refinement in Event-B although some further constraints must be satisfied to ensure the validity of a recomposed model. A-style and B-style decompositions fit into this class.		Decomposition may also be achieved by splitting a system into a number of parts and then proceeding with independent development of each part. At some point, the model parts are recomposed to construct an overall final model. This decomposition style relies on the monotonicity of refinement in Event-B although some further constraints must be satisfied to ensure the validity of a recomposed model. A-style and B-style decompositions fit into this class.

	Finally, decomposition may be realised by hierarchical structuring where some part of an overall system functionality is encapsulated in a self-~~conatined~~ modelling unit embedded into another unit. The distinctive characteristic of this style is that recomposition of model parts happens at the same point where model is decomposed.		Finally, decomposition may be realised by hierarchical structuring where some part of an overall system functionality is encapsulated in a self-contained modelling unit embedded into another unit. The distinctive characteristic of this style is that recomposition of model parts happens at the same point where model is decomposed.

	Modularisation ~~plugin~~ realises the latter approach. The procedure call concept is used to accomplish single point composition/decomposition. There are a number of reasons to try to split a development into modules. Some of them are:		The Modularisation plug-in realises the latter approach. The procedure call concept is used to accomplish single point composition/decomposition. There are a number of reasons to try to split a development into modules. Some of them are:

	* Structuring large specifications: it is difficult to read and edit large model; there is also a limit to the size of model that the ~~Platform~~ may handle comfortably and thus decomposition is an absolute necessity for large scale developments.		* Structuring large specifications: it is difficult to read and edit a large model; there is also a limit to the size of a model that the platform may handle comfortably and thus decomposition is an absolute necessity for large scale developments.
	* Decomposing proof effort: splitting helps to split verification effort. It also helps to reuse proofs: it is not unusual to return back in refinement chain and partially redo abstract models. Normally, this would invalidate most proofs in the dependent components. Model structuring helps to localise the effect of such changes.		* Decomposing proof effort: splitting helps to split verification effort. It also helps to reuse proofs: it is not unusual to return back in refinement chain and partially redo abstract models. Normally, this would invalidate most proofs in the dependent components. Model structuring helps to localise the effect of such changes.
	* Team development: large models may only be developed by a (often distributed) developers team.		* Team development: large models may only be developed by a (often distributed) developers team.
	* Model reuse: modules may be ~~exchange~~ and reused in different projects. The notion of interface make it easier to integrate a module in a new context.		* Model reuse: modules may be exchanged and reused in different projects. The notion of interface make it easier to integrate a module in a new context.
	* Connection to library components		* Connection to library components.
	* Code generation/legacy code		* Code generation/legacy code.

	= Choices / Decisions =		= Choices / Decisions =

	The ~~pimary~~ objective in the tool design was to provide a simple to use tool that could be used by a non-expert modeller. Of course, close integration with the core platform functionality was paramount.		The primary objective in the tool design was to provide a simple to use tool that could be used by a non-expert modeller. Of course, close integration with the core platform functionality was paramount.

	* We have decided there is a need for a new type of Event-B component: interface. A decomposition based on explicit interface (rather than an implicit one such as in A-style decomposition) facilitates reuse of modules and makes it easier to ~~provider~~ a rich management infrastructure.		* We have decided that there is a need for a new type of Event-B component: interface. A decomposition based on explicit interface (rather than on an implicit one, such as in A-style decomposition) facilitates the reuse of modules and makes it easier to provide a rich management infrastructure.

	* ~~At some we~~ had to ~~make a decision of~~ whether to make module integration more explicit and flexible or hide details under ~~syntax~~ sugar and thus achieve better model readability. We have decided that model readability should take priority over everything else. However, while model representation becomes more compact, it does not make proofs ~~any~~ easier.		* We have had to decide whether to make module integration more explicit and flexible or hide details under syntactic sugar and thus achieve better model readability. We have decided that model readability should take priority over everything else. However, while model representation becomes more compact, it does not make proofs easier.

	* During the initial experiments we have identified a need for multiple module instantiation. This allows a modeller to use several copies of the ~~some~~ module using a qualifier prefix to distinguish ~~between~~ objects imported from the modules.		* During the initial experiments we have identified a need for multiple module instantiation. This allows a modeller to use several copies of the same module using a qualifier prefix to distinguish objects imported from the modules.

	* One crucial point was ~~realising~~ modularisation support in such a way that structuring may be recursively applied within modules. Indeed, a module ~~implemenation~~ (module body) is a machine and thus it is self-similar to a caller context that is a machine.		* One crucial point was to realise modularisation support in such a way that structuring may be recursively applied within modules. Indeed, a module implementation (module body) is a machine and thus it is self-similar to a caller context that is a machine.

	* For the current version, we have not implemented the generation of enabledness condition logically required for module implementation. This condition, in some form, should be present in the ~~Platform~~ core.		* For the current version, we have not implemented the generation of enabledness condition logically required for module implementation. This condition, in some form, should be present in the platform core.

	= Available Documentation =		= Available Documentation =

	There is a dedicated wiki page covering the ~~plugin~~ functionality. Also, we are working on further documentation and tutorial.		There is a dedicated wiki page covering the plug-in functionality. Also, we are working on further documentation and tutorial.

	* [[Modularisation Plug-in\|~~Plugin~~ wiki]]		* [[Modularisation Plug-in\|Plug-in wiki]]
	* [[Modularisation Plug-in Tutorial\|~~Plugin~~ tutorial]]		* [[Modularisation Plug-in Tutorial\|Plug-in tutorial]]
	* [[Modularisation Plug-in Installation Instructions\|Installation guide]]		* [[Modularisation Plug-in Installation Instructions\|Installation guide]]

	Two small-scale examples are available:		Two small-scale examples are available:
	* [[http://iliasov.org/modplugin/ticketmachine.zip]] - a model of queue based on two ticket machine module instantiations (very basic)		* [[http://iliasov.org/modplugin/ticketmachine.zip]] - A model of queue based on two ticket machine module instantiations (very basic).
	* [[http://iliasov.org/modplugin/doors.zip]] - ~~two~~ doors sluice controller specification that is decomposed into a number of independent developments (few first steps only)		* [[http://iliasov.org/modplugin/doors.zip]] - Two doors sluice controller specification that is decomposed into a number of independent developments (few first steps only).

	= Planning =		= Planning =
	The ~~plugin~~ is available since ~~Platform version~~ 1.1. See the [[Modularisation Plug-in Release Notes\|release notes]].		The plug-in is available since the release 1.1 of the platform. See the [[Modularisation Plug-in Release Notes\|release notes]].

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