UML-B Integration and Improvements - Revision history

imported>Mathieu: Category:UML-B Category:Work in progress

2009-03-04T09:13:28Z

Category:UML-B Category:Work in progress

← Older revision		Revision as of 09:13, 4 March 2009
Line 37:		Line 37:

	* Logging (of internal errors and exceptions etc.) has been improved and now uses standard Eclipse error logging facilities.		* Logging (of internal errors and exceptions etc.) has been improved and now uses standard Eclipse error logging facilities.

			[[Category:UML-B]]
			[[Category:Work in progress]]

imported>Colin: /* UML-B integration with Event-B */

2009-01-28T17:59:35Z

UML-B integration with Event-B

← Older revision		Revision as of 17:59, 28 January 2009
Line 7:		Line 7:


	The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element. However, many features of UML-B are a replication of corresponding Event-B features. For example, the project diagram in UML-B, uses the concepts of machines and contexts and their relationships (''refines'', ''sees'' and ''extends''). The project diagram would be just as applicable to an Event-B project that did not use any UML like modelling concepts. Similarly, while modelling in UML-B class diagrams, model elements are introduced to a machine that are directly equivalent to their Event-B counterparts. Greater integration would allow UML-B diagrams to be interspersed with Event-B model elements in a flexible mixed modelling interface. This has not been possible due to the differing underlying technologies used for Event-B (bespoke data repository) and UML-B (Eclipse Modelling Framework (EMF)). <nowiki>"The EMF project is a modeling framework and code generation facility for building tools and other applications based on a structured data model".</nowiki> [http://www.eclipse.org/modeling/emf/]		The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element. However, many features of UML-B are a replication of corresponding Event-B features. For example, the project diagram in UML-B, uses the concepts of machines and contexts and their relationships (''refines'', ''sees'' and ''extends'').


			[[Image:UMLBRefinementChain.jpg\|UML-B package diagram showing a refinement chain]]


			The project diagram would be just as applicable to an Event-B project that did not use any UML like modelling concepts. Similarly, while modelling in UML-B class diagrams, model elements are introduced to a machine that are directly equivalent to their Event-B counterparts. Greater integration would allow UML-B diagrams to be interspersed with Event-B model elements in a flexible mixed modelling interface. This has not been possible due to the differing underlying technologies used for Event-B (bespoke data repository) and UML-B (Eclipse Modelling Framework (EMF)). <nowiki>"The EMF project is a modeling framework and code generation facility for building tools and other applications based on a structured data model".</nowiki> [http://www.eclipse.org/modeling/emf/]

	The integration between UML-B and Event-B will be improved by introducing an [[EMF_framework_for_Event-B\|EMF framework for Event-B]]. This will allow UML-B to be re-implemented as an extension to Event-B. Work has begun on this framework and resulting integrated tools will become available during 2009.		The integration between UML-B and Event-B will be improved by introducing an [[EMF_framework_for_Event-B\|EMF framework for Event-B]]. This will allow UML-B to be re-implemented as an extension to Event-B. Work has begun on this framework and resulting integrated tools will become available during 2009.

imported>Colin: /* UML-B integration with Event-B */

2009-01-28T17:33:25Z

UML-B integration with Event-B

← Older revision		Revision as of 17:33, 28 January 2009
Line 1:		Line 1:
	=== UML-B integration with Event-B===		=== UML-B integration with Event-B===

	[[UML-B]] provides a 'UML-like' graphical front end for Event-B. It adds support for class-oriented and state machine modelling but also provides visualisation of existing Event-B modelling concepts. UML-B is similar to UML but is a new notation with its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B tools so that when a drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element. However, many features of UML-B are a replication of corresponding Event-B features. For example, the project diagram in UML-B, uses the concepts of machines and contexts and their relationships (''refines'', ''sees'' and ''extends''). The project diagram would be just as applicable to an Event-B project that did not use any UML like modelling concepts. Similarly, while modelling in UML-B class diagrams, model elements are introduced to a machine that are directly equivalent to their Event-B counterparts. Greater integration would allow UML-B diagrams to be interspersed with Event-B model elements in a flexible mixed modelling interface. This has not been possible due to the differing underlying technologies used for Event-B (bespoke data repository) and UML-B (Eclipse Modelling Framework (EMF)). <nowiki>"The EMF project is a modeling framework and code generation facility for building tools and other applications based on a structured data model".</nowiki> [http://www.eclipse.org/modeling/emf/]		[[UML-B]] provides a 'UML-like' graphical front end for Event-B. It adds support for class-oriented and state machine modelling but also provides visualisation of existing Event-B modelling concepts. UML-B is similar to UML but is a new notation with its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B tools so that when a drawing is saved the translator automatically generates the corresponding Event-B model.


			[[Image:statemachine.jpg\|UML-B perspective with state machine diagram]]


			The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element. However, many features of UML-B are a replication of corresponding Event-B features. For example, the project diagram in UML-B, uses the concepts of machines and contexts and their relationships (''refines'', ''sees'' and ''extends''). The project diagram would be just as applicable to an Event-B project that did not use any UML like modelling concepts. Similarly, while modelling in UML-B class diagrams, model elements are introduced to a machine that are directly equivalent to their Event-B counterparts. Greater integration would allow UML-B diagrams to be interspersed with Event-B model elements in a flexible mixed modelling interface. This has not been possible due to the differing underlying technologies used for Event-B (bespoke data repository) and UML-B (Eclipse Modelling Framework (EMF)). <nowiki>"The EMF project is a modeling framework and code generation facility for building tools and other applications based on a structured data model".</nowiki> [http://www.eclipse.org/modeling/emf/]

	The integration between UML-B and Event-B will be improved by introducing an [[EMF_framework_for_Event-B\|EMF framework for Event-B]]. This will allow UML-B to be re-implemented as an extension to Event-B. Work has begun on this framework and resulting integrated tools will become available during 2009.		The integration between UML-B and Event-B will be improved by introducing an [[EMF_framework_for_Event-B\|EMF framework for Event-B]]. This will allow UML-B to be re-implemented as an extension to Event-B. Work has begun on this framework and resulting integrated tools will become available during 2009.

imported>Colin: /* UML-B Integration with Event-B */

2009-01-28T15:57:49Z

UML-B Integration with Event-B

← Older revision		Revision as of 15:57, 28 January 2009
Line 1:		Line 1:
	=== UML-B ~~Integration~~ with Event-B===		=== UML-B integration with Event-B===

	[[UML-B]] provides a 'UML-like' graphical front end for Event-B. It adds support for class-oriented and state machine modelling but also provides visualisation of existing Event-B modelling concepts. UML-B is similar to UML but is a new notation with its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B tools so that when a drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element. However, many features of UML-B are a replication of corresponding Event-B features. For example, the project diagram in UML-B, uses the concepts of machines and contexts and their relationships (''refines'', ''sees'' and ''extends''). The project diagram would be just as applicable to an Event-B project that did not use any UML like modelling concepts. Similarly, while modelling in UML-B class diagrams, model elements are introduced to a machine that are directly equivalent to their Event-B counterparts. Greater integration would allow UML-B diagrams to be interspersed with Event-B model elements in a flexible mixed modelling interface. This has not been possible due to the differing underlying technologies used for Event-B (bespoke data repository) and UML-B (Eclipse Modelling Framework (EMF)). <nowiki>"The EMF project is a modeling framework and code generation facility for building tools and other applications based on a structured data model".</nowiki> [http://www.eclipse.org/modeling/emf/]		[[UML-B]] provides a 'UML-like' graphical front end for Event-B. It adds support for class-oriented and state machine modelling but also provides visualisation of existing Event-B modelling concepts. UML-B is similar to UML but is a new notation with its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B tools so that when a drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element. However, many features of UML-B are a replication of corresponding Event-B features. For example, the project diagram in UML-B, uses the concepts of machines and contexts and their relationships (''refines'', ''sees'' and ''extends''). The project diagram would be just as applicable to an Event-B project that did not use any UML like modelling concepts. Similarly, while modelling in UML-B class diagrams, model elements are introduced to a machine that are directly equivalent to their Event-B counterparts. Greater integration would allow UML-B diagrams to be interspersed with Event-B model elements in a flexible mixed modelling interface. This has not been possible due to the differing underlying technologies used for Event-B (bespoke data repository) and UML-B (Eclipse Modelling Framework (EMF)). <nowiki>"The EMF project is a modeling framework and code generation facility for building tools and other applications based on a structured data model".</nowiki> [http://www.eclipse.org/modeling/emf/]

imported>Colin: /* Improvements to the existing version of UML-B */

2009-01-28T15:55:45Z

Improvements to the existing version of UML-B

← Older revision		Revision as of 15:55, 28 January 2009
Line 24:		Line 24:
	* File maintenance has been improved so that diagrams and Event-B models are deleted when corresponding model elements are deleted.		* File maintenance has been improved so that diagrams and Event-B models are deleted when corresponding model elements are deleted.

	* ~~Error logging~~ (of internal errors and exceptions etc.) has been improved and now uses standard ~~eclipse~~ facilities.		* Logging (of internal errors and exceptions etc.) has been improved and now uses standard Eclipse error logging facilities.

imported>Colin: /* Improvements to the existing version of UML-B */

2009-01-28T15:54:56Z

Improvements to the existing version of UML-B

← Older revision		Revision as of 15:54, 28 January 2009
Line 6:		Line 6:

	===Improvements to the existing version of UML-B===		===Improvements to the existing version of UML-B===
	While this new UML-B is being developed, improvements to the existing version of UML-B are ongoing. A new release of UML-B (0.5.0)) contains significant improvements, most notably the addition of support for refinement of ~~statemachines~~. New features include:		While this new UML-B is being developed, improvements to the existing version of UML-B are ongoing. A new release of UML-B (0.5.x) contains significant improvements, most notably the addition of support for refinement of state machines. New features include:

	* Support for refinement of state machines in UML-B. This release allows a ~~statemachine~~ to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined ~~statemachine~~ can be elaborated by adding more detailed hierarchical ~~statemachines~~. This addition is described in more detail in [[media:SaidButlerSnook09.pdf\|Said, Butler and Snook]]		* Support for refinement of state machines in UML-B. This release allows a state machine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined state machine can be elaborated by adding more detailed hierarchical state machines. This addition is described in more detail in [[media:SaidButlerSnook09.pdf\|Said, Butler and Snook]]

	* Support for synchronisation of transitions from different ~~statemachines~~. This feature will allow two or more transitions in different ~~statemachines~~ to contribute to a single event. This feature is needed because a single event can alter several variables (in this case ~~statemachines~~) simultaneously.		* Support for synchronisation of transitions from different state machines. This feature will allow two or more transitions in different state machines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case state machines) simultaneously.

	* Allow user to allocate the name of the 'implicit contextual instance' used in a class. Events and Transitions owned by a class are implicitly acting upon an instance of the class which was formerly denoted by the reserved word 'self'. This modification allows the modeller to override 'self' (which is now the default name) with any other identifier. This feature is needed to avoid name clashes when synchronising transitions into a single event. It also allows events to be moved between different classes (or outside of all classes) during refinement without creating name clashes.		* Allow user to allocate the name of the 'implicit contextual instance' used in a class. Events and Transitions owned by a class are implicitly acting upon an instance of the class which was formerly denoted by the reserved word 'self'. This modification allows the modeller to override 'self' (which is now the default name) with any other identifier. This feature is needed to avoid name clashes when synchronising transitions into a single event. It also allows events to be moved between different classes (or outside of all classes) during refinement without creating name clashes.
Line 16:		Line 16:
	* The properties view has been improved with the addition of a tab for 'model'. This tab allows direct access to the underlying EMF model element so that its properties can be viewed and changed.		* The properties view has been improved with the addition of a tab for 'model'. This tab allows direct access to the underlying EMF model element so that its properties can be viewed and changed.

	* Some improvements have been made to the UML-B perspective layout to reflect changes to the Event-B one. The task and problem views have been removed and the 'Rodin Problem' view has been added instead.		* Some improvements have been made to the UML-B perspective layout to reflect changes to the Event-B one. The task and problem views have been removed and the 'Rodin Problem' view has been added instead.

			* An ''action'' (toolbar button and menu item) has been added to enable manual invocation of the UML-B to Event-B translation process. This can be used in place of the automatic builder for larger projects where frequent re-verification may be inconvenient.

			* Synchronisation of different diagram editors and views has been improved.

			* File maintenance has been improved so that diagrams and Event-B models are deleted when corresponding model elements are deleted.

			* Error logging (of internal errors and exceptions etc.) has been improved and now uses standard eclipse facilities.

imported>Colin: /* UML-B Integration with Event-B */

2009-01-28T15:37:19Z

UML-B Integration with Event-B

← Older revision		Revision as of 15:37, 28 January 2009
Line 1:		Line 1:
	=== UML-B Integration with Event-B===		=== UML-B Integration with Event-B===

	[[UML-B]] provides a 'UML-like' graphical front end for Event-B. It adds support for class-oriented and state machine modelling but also provides visualisation of existing Event-B modelling concepts. UML-B is similar to UML but is a new notation with its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B tools so that when a drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element. However, many features of UML-B are a replication of corresponding Event-B features. For example, the project diagram in UML-B, uses the concepts of machines and contexts and their relationships (refines, sees and extends). The project diagram would be just as applicable to an Event-B project that did not use any UML like modelling concepts. Similarly, while modelling in UML-B class diagrams, model elements are introduced to a machine that are directly equivalent to their Event-B counterparts. Greater integration would allow UML-B diagrams to be interspersed with Event-B model elements in a flexible mixed modelling interface. This has not been possible due to the differing underlying technologies used for Event-B (bespoke data repository) and UML-B (EMF).		[[UML-B]] provides a 'UML-like' graphical front end for Event-B. It adds support for class-oriented and state machine modelling but also provides visualisation of existing Event-B modelling concepts. UML-B is similar to UML but is a new notation with its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B tools so that when a drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element. However, many features of UML-B are a replication of corresponding Event-B features. For example, the project diagram in UML-B, uses the concepts of machines and contexts and their relationships (''refines'', ''sees'' and ''extends''). The project diagram would be just as applicable to an Event-B project that did not use any UML like modelling concepts. Similarly, while modelling in UML-B class diagrams, model elements are introduced to a machine that are directly equivalent to their Event-B counterparts. Greater integration would allow UML-B diagrams to be interspersed with Event-B model elements in a flexible mixed modelling interface. This has not been possible due to the differing underlying technologies used for Event-B (bespoke data repository) and UML-B (Eclipse Modelling Framework (EMF)). <nowiki>"The EMF project is a modeling framework and code generation facility for building tools and other applications based on a structured data model".</nowiki> [http://www.eclipse.org/modeling/emf/]

	The integration between UML-B and Event-B will be improved by introducing an [[EMF_framework_for_Event-B\|EMF framework for Event-B]]. This will allow UML-B to be re-implemented as an extension to Event-B. Work has begun on this framework and resulting integrated tools will become available during 2009.		The integration between UML-B and Event-B will be improved by introducing an [[EMF_framework_for_Event-B\|EMF framework for Event-B]]. This will allow UML-B to be re-implemented as an extension to Event-B. Work has begun on this framework and resulting integrated tools will become available during 2009.

imported>Colin: /* Improvements to the existing version of UML-B */

2008-12-16T18:14:14Z

Improvements to the existing version of UML-B

← Older revision		Revision as of 18:14, 16 December 2008
Line 8:		Line 8:
	While this new UML-B is being developed, improvements to the existing version of UML-B are ongoing. A new release of UML-B (0.5.0)) contains significant improvements, most notably the addition of support for refinement of statemachines. New features include:		While this new UML-B is being developed, improvements to the existing version of UML-B are ongoing. A new release of UML-B (0.5.0)) contains significant improvements, most notably the addition of support for refinement of statemachines. New features include:

	* Support for refinement of state machines in UML-B. This release allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines. This addition is described in more detail in [[#SaidButlerSnook09.pdf\|Said, Butler and Snook]]		* Support for refinement of state machines in UML-B. This release allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines. This addition is described in more detail in [[media:SaidButlerSnook09.pdf\|Said, Butler and Snook]]

	* Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.		* Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.

imported>Colin: /* Improvements to the existing version of UML-B */

2008-12-16T17:59:10Z

Improvements to the existing version of UML-B

← Older revision		Revision as of 17:59, 16 December 2008
Line 8:		Line 8:
	While this new UML-B is being developed, improvements to the existing version of UML-B are ongoing. A new release of UML-B (0.5.0)) contains significant improvements, most notably the addition of support for refinement of statemachines. New features include:		While this new UML-B is being developed, improvements to the existing version of UML-B are ongoing. A new release of UML-B (0.5.0)) contains significant improvements, most notably the addition of support for refinement of statemachines. New features include:

	* Support for refinement of state machines in UML-B. This release allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines. This addition is described in more detail in [[~~Image:~~SaidButlerSnook09.pdf\|Said, Butler and Snook]]		* Support for refinement of state machines in UML-B. This release allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines. This addition is described in more detail in [[#SaidButlerSnook09.pdf\|Said, Butler and Snook]]

	* Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.		* Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.

imported>Colin: /* Improvements to the existing version of UML-B */

2008-12-16T17:56:29Z

Improvements to the existing version of UML-B

← Older revision		Revision as of 17:56, 16 December 2008
Line 8:		Line 8:
	While this new UML-B is being developed, improvements to the existing version of UML-B are ongoing. A new release of UML-B (0.5.0)) contains significant improvements, most notably the addition of support for refinement of statemachines. New features include:		While this new UML-B is being developed, improvements to the existing version of UML-B are ongoing. A new release of UML-B (0.5.0)) contains significant improvements, most notably the addition of support for refinement of statemachines. New features include:

	* Support for refinement of state machines in UML-B. This release allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines. This addition is described in more detail in [[SaidButlerSnook09.pdf\|Said, Butler and Snook]]		* Support for refinement of state machines in UML-B. This release allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines. This addition is described in more detail in [[Image:SaidButlerSnook09.pdf\|Said, Butler and Snook]]

	* Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.		* Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.