Modularisation Plug-in - Revision history

imported>Alexili at 10:57, 6 September 2010

2010-09-06T10:57:03Z

← Older revision		Revision as of 10:57, 6 September 2010
Line 17:		Line 17:

	This is teaching material for those wishing to learn about the Modularisation plugin. It includes a development and detailed explanatory slides.		This is teaching material for those wishing to learn about the Modularisation plugin. It includes a development and detailed explanatory slides.

			There is a dedicated page for [[Modularisation Integration Issues]].

	==General Motivation==		==General Motivation==

imported>Alexili at 14:25, 21 May 2010

2010-05-21T14:25:48Z

← Older revision		Revision as of 14:25, 21 May 2010
Line 14:		Line 14:
	The [[Modularisation Plug-in Tutorial]] page is currently in preparation.		The [[Modularisation Plug-in Tutorial]] page is currently in preparation.

			===[http://deploy-eprints.ecs.soton.ac.uk/227/ Modularisation Training]===

			This is teaching material for those wishing to learn about the Modularisation plugin. It includes a development and detailed explanatory slides.

	==General Motivation==		==General Motivation==

imported>Alexili at 13:31, 22 October 2009

2009-10-22T13:31:21Z

← Older revision		Revision as of 13:31, 22 October 2009
Line 23:		Line 23:
	Finally, decomposition may be realised by hierarchical structuring where part of a an overall system functionality is encapsulated in some self-conatined modelling unit embedded into another unit. The distinctive characteristic of this style is that recomposition of happens at the same point where model is decomposed.		Finally, decomposition may be realised by hierarchical structuring where part of a an overall system functionality is encapsulated in some self-conatined modelling unit embedded into another unit. The distinctive characteristic of this style is that recomposition of happens at the same point where model is decomposed.

	~~One suitable metaphor for the latter is a procedure call.~~ Modularisation plug-in realises the latter approach. The procedure call concept is used to accomplish single point composition/decomposition.		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:		There are a number of reasons to try to split a development into modules. Some of them are:

imported>Alexili at 13:26, 22 October 2009

2009-10-22T13:26:36Z

← Older revision		Revision as of 13:26, 22 October 2009
Line 13:		Line 13:

	The [[Modularisation Plug-in Tutorial]] page is currently in preparation.		The [[Modularisation Plug-in Tutorial]] page is currently in preparation.


			==General Motivation==

			There are three major approaches to decomposition. One is to identify 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. An imported theory of stack contributes axioms and theorems assisting in reasoning about stacks.

			Another form of decomposition is 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 further constraints must be satisfied to ensure the validity of a recomposed model.

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

			One suitable metaphor for the latter is a procedure call. 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.
			* 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.
			* 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.
			* Connection to library components
			* Code generation/legacy code

imported>Alexili at 12:54, 22 October 2009

2009-10-22T12:54:36Z

← Older revision		Revision as of 12:54, 22 October 2009
Line 12:		Line 12:
	Please see the [[Modularisation Plug-in Installation Instructions]] for details on obtaining and installing the plug-in.		Please see the [[Modularisation Plug-in Installation Instructions]] for details on obtaining and installing the plug-in.

			The [[Modularisation Plug-in Tutorial]] page is currently in preparation.

imported>Alexili at 12:26, 22 October 2009

2009-10-22T12:26:56Z

← Older revision		Revision as of 12:26, 22 October 2009
Line 236:		Line 236:
	y := push(7)		y := push(7)

	Several operation ~~call~~ may be combined to form complex action expression:		Several operation calls may be combined to form complex action expression:

	z := push(pop * pop)		z := push(pop * pop)

imported>Alexili at 12:24, 22 October 2009

2009-10-22T12:24:20Z

← Older revision		Revision as of 12:24, 22 October 2009
Line 21:		Line 21:
	While a speciﬁcation based on a single module may be used to describe fairly large systems		While a speciﬁcation based on a single module may be used to describe fairly large systems
	such approach presents a number of limitations. The only speciﬁcation structuring mechanism		such approach presents a number of limitations. The only speciﬁcation structuring mechanism
	of module is the notion of event. A ~~suﬃciently~~ detailed model would correspond to a module		of module is the notion of event. A sufficiently detailed model would correspond to a module
	with a substantial number of events. This leads to the scalability problems as the number of		with a substantial number of events. This leads to the scalability problems as the number of
	events and actions contained in them is linearly proportional to the number of proof obligations.		events and actions contained in them is linearly proportional to the number of proof obligations.
Line 65:		Line 65:

	====Operation Call====		====Operation Call====
	The passive observation of a subordinate module state is ~~suﬃcient~~ only for the simplest composition		The passive observation of a subordinate module state is sufficient only for the simplest composition
	scenarious. The notion of a module operation oﬀers a parent module the ability to		scenarious. The notion of a module operation oﬀers a parent module the ability to
	request a service of a subordinate module at the moment when it is needed. From the parent model		request a service of a subordinate module at the moment when it is needed. From the parent model

imported>Alexili at 12:20, 22 October 2009

2009-10-22T12:20:49Z

← Older revision		Revision as of 12:20, 22 October 2009
Line 271:		Line 271:
	* [[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)


	~~[[Modularisation Plug-in Composition Semantics]]~~

	[[Category:Plugin]]		[[Category:Plugin]]

imported>Alexili at 12:08, 22 October 2009

2009-10-22T12:08:18Z

← Older revision		Revision as of 12:08, 22 October 2009
Line 11:		Line 11:

	Please see the [[Modularisation Plug-in Installation Instructions]] for details on obtaining and installing the plug-in.		Please see the [[Modularisation Plug-in Installation Instructions]] for details on obtaining and installing the plug-in.



Line 273:		Line 272:
	* [[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)


			[[Modularisation Plug-in Composition Semantics]]

	[[Category:Plugin]]		[[Category:Plugin]]

imported>Alexili at 10:00, 22 October 2009

2009-10-22T10:00:01Z

← Older revision		Revision as of 10:00, 22 October 2009
Line 196:		Line 196:

	The interface editor is based on the platform composite editor and follows the same principles and structure.		The interface editor is based on the platform composite editor and follows the same principles and structure.



	==Importing a Module==		==Importing a Module==
Line 222:		Line 224:

	The only place where an imported operation may appear is an action expression. Since it is a state updating relation it may not be a part of a guard or invariant.		The only place where an imported operation may appear is an action expression. Since it is a state updating relation it may not be a part of a guard or invariant.



	=== Calling an operation ===		=== Calling an operation ===
Line 247:		Line 251:




	==Implementing a Module==		==Implementing a Module==

Line 258:		Line 264:

	An interface operation is realised by a set of events. It is required to provide a realisation (however abstract) for all the interface operations. A connection between an event and operation is established by marking an event as a part of a specific ''event group''.		An interface operation is realised by a set of events. It is required to provide a realisation (however abstract) for all the interface operations. A connection between an event and operation is established by marking an event as a part of a specific ''event group''.