D23 UML-B - Revision history

imported>Pascal: /* For PDF rendering */

2010-01-28T15:53:36Z

For PDF rendering

← Older revision		Revision as of 15:53, 28 January 2010
Line 1:		Line 1:
	=== Overview ===		= Overview =
	This part of the deliverable describes improvements to the UML-B plug-in feature, which is the responsibility of University of Southampton.		This part of the deliverable describes improvements to the UML-B plug-in feature, which is the responsibility of University of Southampton.

Line 6:		Line 6:
	The longer term development of UML-B relies on an EMF representation of Event-B. The development of a new EMF Event-B plugin-in feature is also described in this section. This feature was initially developed by University of Southampton, Heinrich-Heine University, Düsseldorf and University of Newcastle. It is now mostly maintained and developed by University of Southampton.		The longer term development of UML-B relies on an EMF representation of Event-B. The development of a new EMF Event-B plugin-in feature is also described in this section. This feature was initially developed by University of Southampton, Heinrich-Heine University, Düsseldorf and University of Newcastle. It is now mostly maintained and developed by University of Southampton.

	=== Motivations ===		= Motivations =

	====UML-B Support for State machine Refinement====		==UML-B Support for State machine Refinement==

	The current version of the UML-B tool has been improved to support the refinement of state-machines. At the last deliverable, refinement of classes was supported and state-machine refinement was beginning to be investigated. The investigation has experimented several notation and methodological alternatives. The design has now been finalised and an implementation has been achieved. State-machines can be refined by adding nested state-machines inside states. Some of the transitions in the nested state-machine do not represent new events but contribute to the refinements of existing transitions in the parent state-machine. A concept of ''transition elaboration'' has been invented to represent this relationship.		The current version of the UML-B tool has been improved to support the refinement of state-machines. At the last deliverable, refinement of classes was supported and state-machine refinement was beginning to be investigated. The investigation has experimented several notation and methodological alternatives. The design has now been finalised and an implementation has been achieved. State-machines can be refined by adding nested state-machines inside states. Some of the transitions in the nested state-machine do not represent new events but contribute to the refinements of existing transitions in the parent state-machine. A concept of ''transition elaboration'' has been invented to represent this relationship.

	====UML-B General Improvements====		==UML-B General Improvements==
	Many other minor improvements have been made to the UML-B tool including:		Many other minor improvements have been made to the UML-B tool including:
	* collapsing empty compartments on diagrams,		* collapsing empty compartments on diagrams,
Line 20:		Line 20:
	* support for theorems everywhere (i.e. invariants and axioms can now be designated as theorems).		* support for theorems everywhere (i.e. invariants and axioms can now be designated as theorems).

	====UML-B State-machine Animation====		==UML-B State-machine Animation==
	This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.		This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.

Line 32:		Line 32:
	[http://wiki.event-b.org/index.php/Statemachine_Animation_Large_Screenshot Statemachine Animation Large Screenshot]		[http://wiki.event-b.org/index.php/Statemachine_Animation_Large_Screenshot Statemachine Animation Large Screenshot]

	====EMF Framework for Event-B====		==EMF Framework for Event-B==

	An EMF (Eclipse Modelling Framework) based representation of Event-B was developed and made available as a plug-in feature for Rodin. This enables Event-B machines and contexts to be loaded into EMF based tools. Serialisation (i.e. loading and saving) is performed via the Rodin API. This feature can be viewed as an ''enabling technology''. Hence motivation derives from several sources including:		An EMF (Eclipse Modelling Framework) based representation of Event-B was developed and made available as a plug-in feature for Rodin. This enables Event-B machines and contexts to be loaded into EMF based tools. Serialisation (i.e. loading and saving) is performed via the Rodin API. This feature can be viewed as an ''enabling technology''. Hence motivation derives from several sources including:
Line 39:		Line 39:
	* '''UML-B integration''' - since UML-B is based on EMF, the development of an EMF representation of Event-B enables UML-B concepts to be added as extensions.		* '''UML-B integration''' - since UML-B is based on EMF, the development of an EMF representation of Event-B enables UML-B concepts to be added as extensions.

	=== Choices / Decisions ===		= Choices / Decisions =


	====UML-B Support for State machine Refinement====		==UML-B Support for State machine Refinement==
	The methods and modelling notations for refinement in UML-B were developed by experimentation using a case study of an ATM. The use of hierarchical nested state-machines (which were already available in UML-B) as a technique for adding detail in refinement was quickly adapted by making changes to the meta-model and translation. This technique was found to be suitable. Some further experimentation was needed in order to understand the need to link transitions of the nested state-machines with those in their parent. A concept of ''elaboration'' was introduced, whereby an elaborating transition contributes guards and actions to the event produced from the elaborated parent transition. Transition splitting (analogous to event splitting in Event-B refinements) is a natural consequence of refinement of states. An idea to ''bundle'' the split transitions in the parent state-machine so that the correspondence with the abstract refined state-machine is more obvious has not been pursued for now since it would add complication to the tooling.		The methods and modelling notations for refinement in UML-B were developed by experimentation using a case study of an ATM. The use of hierarchical nested state-machines (which were already available in UML-B) as a technique for adding detail in refinement was quickly adapted by making changes to the meta-model and translation. This technique was found to be suitable. Some further experimentation was needed in order to understand the need to link transitions of the nested state-machines with those in their parent. A concept of ''elaboration'' was introduced, whereby an elaborating transition contributes guards and actions to the event produced from the elaborated parent transition. Transition splitting (analogous to event splitting in Event-B refinements) is a natural consequence of refinement of states. An idea to ''bundle'' the split transitions in the parent state-machine so that the correspondence with the abstract refined state-machine is more obvious has not been pursued for now since it would add complication to the tooling.

	====UML-B State-machine Animation====		==UML-B State-machine Animation==
	Initially, we attempted to model the animation state information as an extension to the UML-B meta-model. We discovered technological difficulties in extending EMF models in this way. Therefore, we adopted an alternative solution using an independent meta-model of animation diagrams. These replicate parts of the structure of UML-B but add meta-properties to model the animation. When a model is to be animated, an animation model is constructed programmatically to match the UML-B model. Thereafter, the animation runs independently of UML-B. This has the additional benefit that the diagram can be simplified and tailored to better suit animation. For example, removing the editing palette.		Initially, we attempted to model the animation state information as an extension to the UML-B meta-model. We discovered technological difficulties in extending EMF models in this way. Therefore, we adopted an alternative solution using an independent meta-model of animation diagrams. These replicate parts of the structure of UML-B but add meta-properties to model the animation. When a model is to be animated, an animation model is constructed programmatically to match the UML-B model. Thereafter, the animation runs independently of UML-B. This has the additional benefit that the diagram can be simplified and tailored to better suit animation. For example, removing the editing palette.

	====EMF Framework for Event-B====		==EMF Framework for Event-B==
	The structure of the EMF meta-model for Event-B was studied in great detail. Various options for sub-packaging the model were tried but it has been found that it is more convenient for users to keep a simple package structure. Currently this consists of three packages; a ''core'' package containing abstract basis and project level meta-model, a ''machine'' package and a ''context'' package. A flexible abstract basis has been derived through experimentation. The abstract basis consists of an inheritance hierarchy of abstract meta-classes which provide great flexibility for writing code that deals with the meta-model in as generic a manner as possible. A driving factor in the design was to support both project level tools and component level tools. The latter should be able to manipulate a single machine or context without loading referenced components. This was achieved customising the EMF proxies (used in references) so that they are calculated lazily (when a request to resolve is received).		The structure of the EMF meta-model for Event-B was studied in great detail. Various options for sub-packaging the model were tried but it has been found that it is more convenient for users to keep a simple package structure. Currently this consists of three packages; a ''core'' package containing abstract basis and project level meta-model, a ''machine'' package and a ''context'' package. A flexible abstract basis has been derived through experimentation. The abstract basis consists of an inheritance hierarchy of abstract meta-classes which provide great flexibility for writing code that deals with the meta-model in as generic a manner as possible. A driving factor in the design was to support both project level tools and component level tools. The latter should be able to manipulate a single machine or context without loading referenced components. This was achieved customising the EMF proxies (used in references) so that they are calculated lazily (when a request to resolve is received).

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

	UML-B Refinement is described in a paper which was presented at the FM2009 conference in Eindhoven. It is available here:		UML-B Refinement is described in a paper which was presented at the FM2009 conference in Eindhoven. It is available here:
Line 69:		Line 69:
	:[http://eprints.ecs.soton.ac.uk/18262 An EMF Framework for Event-B]		:[http://eprints.ecs.soton.ac.uk/18262 An EMF Framework for Event-B]

	=== Planning ===		= Planning =
	UML-B integration:		UML-B integration:
	* Develop extensibility mechanisms for EMF Event-B framework via experimentation with structured data (records) plug-in.		* Develop extensibility mechanisms for EMF Event-B framework via experimentation with structured data (records) plug-in.

imported>Colin: /* UML-B State-machine Animation */

2010-01-28T15:15:12Z

UML-B State-machine Animation

← Older revision		Revision as of 15:15, 28 January 2010
Line 23:		Line 23:
	This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.		This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.

	The screenshot below shows a statemachine ~~(top left) and its refinement (top right)~~ being animated ~~in parallel with the nested statemachines (bottom left and right) that are contained in the refined states~~. Two class instances are currently active; one models an ATM that is not available (e.g. in ~~maintenace~~) and the other is in the process of validating a card. Transitions that are enabled for one or other of the class instances are emboldened. (The instance to be used when a transition is fired is selected when the transitions is clicked upon)~~. Note that the ancillary views around the diagrams are ProB views which can also be used during the animation~~.		The screenshot below shows a simple statemachine being animated. Two class instances are currently active; one models an ATM that is not available (e.g. in maintenance) and the other is in the process of validating a card. Transitions that are enabled for one or other of the class instances are emboldened. (The instance to be used when a transition is fired is selected when the transitions is clicked upon).

	[[Image:Screenshot-1.png\|Screenshot of a state-machine hierarchy during animation]].		[[Image:Screenshot-1.png\|Screenshot of a state-machine hierarchy during animation]].

imported>Pascal: /* Revert missing paragraph erroneously deleted */

2010-01-28T15:01:29Z

Revert missing paragraph erroneously deleted

← Older revision		Revision as of 15:01, 28 January 2010
Line 23:		Line 23:
	This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.		This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.

			The screenshot below shows a statemachine (top left) and its refinement (top right) being animated in parallel with the nested statemachines (bottom left and right) that are contained in the refined states. Two class instances are currently active; one models an ATM that is not available (e.g. in maintenace) and the other is in the process of validating a card. Transitions that are enabled for one or other of the class instances are emboldened. (The instance to be used when a transition is fired is selected when the transitions is clicked upon). Note that the ancillary views around the diagrams are ProB views which can also be used during the animation.

	[[Image:Screenshot-1.png\|Screenshot of a state-machine hierarchy during animation]].		[[Image:Screenshot-1.png\|Screenshot of a state-machine hierarchy during animation]].

imported>Pascal: /* UML-B State-machine Animation */

2010-01-28T14:58:47Z

UML-B State-machine Animation

← Older revision		Revision as of 14:58, 28 January 2010
Line 27:		Line 27:


	A larger screenshot of refined and nested statemachines being animated in parallel is shown here:-		A larger screenshot of refined and nested statemachines being animated in parallel is shown here:

	[[Statemachine Animation Large Screenshot]]		[http://wiki.event-b.org/index.php/Statemachine_Animation_Large_Screenshot Statemachine Animation Large Screenshot]

	====EMF Framework for Event-B====		====EMF Framework for Event-B====

imported>Colin: /* UML-B State-machine Animation */

2010-01-28T14:43:12Z

UML-B State-machine Animation

← Older revision		Revision as of 14:43, 28 January 2010
Line 27:		Line 27:


	A larger screenshot of statemachines being animated is shown here:-		A larger screenshot of refined and nested statemachines being animated in parallel is shown here:-

	[[Statemachine Animation Large Screenshot]]		[[Statemachine Animation Large Screenshot]]

imported>Colin: /* UML-B State-machine Animation */

2010-01-28T14:42:45Z

UML-B State-machine Animation

← Older revision		Revision as of 14:42, 28 January 2010
Line 26:		Line 26:
	[[Image:Screenshot-1.png\|Screenshot of a state-machine hierarchy during animation]].		[[Image:Screenshot-1.png\|Screenshot of a state-machine hierarchy during animation]].

	~~[[Statemachine Animation Large Screenshot\|~~A larger screenshot of statemachines being animated is shown here]]
			A larger screenshot of statemachines being animated is shown here:-

			[[Statemachine Animation Large Screenshot]]

	====EMF Framework for Event-B====		====EMF Framework for Event-B====

imported>Colin: /* UML-B State-machine Animation */

2010-01-28T14:41:35Z

UML-B State-machine Animation

← Older revision		Revision as of 14:41, 28 January 2010
Line 23:		Line 23:
	This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.		This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.

	The screenshot below shows a statemachine (top left) and its refinement (top right) being animated in parallel with the nested statemachines (bottom left and right) that are contained in the refined states. Two class instances are currently active; one models an ATM that is not available (e.g. in maintenace) and the other is in the process of validating a card. Transitions that are enabled for one or other of the class instances are emboldened. (The instance to be used when a transition is fired is selected when the transitions is clicked upon). Note that the ancillary views around the diagrams are ProB views which can also be used during the animation.

	[[Image:~~SmAnimScreenshot~~.png]]		[[Image:Screenshot-1.png\|Screenshot of a state-machine hierarchy during animation]].

			[[Statemachine Animation Large Screenshot\|A larger screenshot of statemachines being animated is shown here]]

	====EMF Framework for Event-B====		====EMF Framework for Event-B====

imported>Colin: /* UML-B State-machine Animation */

2010-01-27T21:59:45Z

UML-B State-machine Animation

← Older revision		Revision as of 21:59, 27 January 2010
Line 23:		Line 23:
	This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.		This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.

	The screenshot below shows a statemachine (top left) and its refinement (top right) being animated in parallel with the nested statemachines (bottom left and right) that are contained in the refined states. Two class instances are currently active; one models an ATM that is not available (e.g. in maintenace) and the other is in the process of validating a card. Transitions that are enabled for one or other of the class instances are emboldened. (The instance to be used when a transition is fired is selected when the transitions is clicked upon.		The screenshot below shows a statemachine (top left) and its refinement (top right) being animated in parallel with the nested statemachines (bottom left and right) that are contained in the refined states. Two class instances are currently active; one models an ATM that is not available (e.g. in maintenace) and the other is in the process of validating a card. Transitions that are enabled for one or other of the class instances are emboldened. (The instance to be used when a transition is fired is selected when the transitions is clicked upon). Note that the ancillary views around the diagrams are ProB views which can also be used during the animation.

	[[Image:SmAnimScreenshot.png]]		[[Image:SmAnimScreenshot.png]]

imported>Colin: /* UML-B State-machine Animation */

2010-01-27T21:58:13Z

UML-B State-machine Animation

← Older revision		Revision as of 21:58, 27 January 2010
Line 22:		Line 22:
	====UML-B State-machine Animation====		====UML-B State-machine Animation====
	This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.		This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.

			The screenshot below shows a statemachine (top left) and its refinement (top right) being animated in parallel with the nested statemachines (bottom left and right) that are contained in the refined states. Two class instances are currently active; one models an ATM that is not available (e.g. in maintenace) and the other is in the process of validating a card. Transitions that are enabled for one or other of the class instances are emboldened. (The instance to be used when a transition is fired is selected when the transitions is clicked upon.

			[[Image:SmAnimScreenshot.png]]

	====EMF Framework for Event-B====		====EMF Framework for Event-B====

imported>Colin: /* UML-B improvements */

2010-01-27T14:21:21Z

UML-B improvements

← Older revision		Revision as of 14:21, 27 January 2010
Line 32:		Line 32:
	=== Choices / Decisions ===		=== Choices / Decisions ===

	~~====UML-B improvements====~~

			====UML-B Support for State machine Refinement====
	The methods and modelling notations for refinement in UML-B were developed by experimentation using a case study of an ATM. The use of hierarchical nested state-machines (which were already available in UML-B) as a technique for adding detail in refinement was quickly adapted by making changes to the meta-model and translation. This technique was found to be suitable. Some further experimentation was needed in order to understand the need to link transitions of the nested state-machines with those in their parent. A concept of ''elaboration'' was introduced, whereby an elaborating transition contributes guards and actions to the event produced from the elaborated parent transition. Transition splitting (analogous to event splitting in Event-B refinements) is a natural consequence of refinement of states. An idea to ''bundle'' the split transitions in the parent state-machine so that the correspondence with the abstract refined state-machine is more obvious has not been pursued for now since it would add complication to the tooling.		The methods and modelling notations for refinement in UML-B were developed by experimentation using a case study of an ATM. The use of hierarchical nested state-machines (which were already available in UML-B) as a technique for adding detail in refinement was quickly adapted by making changes to the meta-model and translation. This technique was found to be suitable. Some further experimentation was needed in order to understand the need to link transitions of the nested state-machines with those in their parent. A concept of ''elaboration'' was introduced, whereby an elaborating transition contributes guards and actions to the event produced from the elaborated parent transition. Transition splitting (analogous to event splitting in Event-B refinements) is a natural consequence of refinement of states. An idea to ''bundle'' the split transitions in the parent state-machine so that the correspondence with the abstract refined state-machine is more obvious has not been pursued for now since it would add complication to the tooling.