ADVANCE D3.2 General Platform Maintenance - Revision history

imported>Laurent: /* Planning */

2012-07-18T13:18:30Z

Planning

← Older revision		Revision as of 13:18, 18 July 2012
Line 29:		Line 29:

	== Planning ==		== Planning ==
	Two releases of the core platform have been scheduled after Rodin 2.6 has been published: Rodin 2.7 ~~followed by Rodin 3.0. Rodin 2.7 is intended to be released by the~~ end of October 2012~~, and~~ Rodin 3.0 ~~will be available by the~~ end of January 2013. Rodin 2.7 will be corrective~~. It has been scheduled to respect the 3 monthly~~ release ~~policy, as the Rodin 3~~.~~0 version will require more that 3 months of development. In addition~~, ~~Rodin 2.7~~ will integrate the Theory plug-in (which is currently separate).		Two releases of the core platform have been scheduled after Rodin 2.6 has been published: Rodin 2.7 (end of October 2012) followed by Rodin 3.0 (end of January 2013). Rodin 2.7 will mainly be a corrective release. However, it will integrate the Theory plug-in (which allows to define mathematical extensions and is currently provided as a separate plug-in).

	~~Indeed, version~~ 3.0 of ~~the platform is being prepared since~~ Rodin 2.6, and will include lots of refactoring and evolutions in the published programming ~~interfaces~~ (API). ~~Here is a~~ non exhaustive list of the ~~main~~ improvements and ~~refactorings that will be part of it~~:		Work on release 3.0 will start concurrently with development of Rodin 2.7 and will include lots of refactoring and evolutions in the published programming interface (API). A non exhaustive list of the planned improvements and refactoring is:
	*Binders will be allowed in extensions.		*Binders will be allowed in extensions.
	*The platform will be based on Eclipse 4.		*The platform will be based on Eclipse 4.

imported>Laurent: /* Planning */

2012-07-18T13:13:26Z

Planning

← Older revision		Revision as of 13:13, 18 July 2012
Line 128:		Line 128:
	== Planning ==		== Planning ==

	There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, the method mentioned above<ref name="req1ref"/> lists a number of properties of a correct system description. For example, the ~~existance~~ of a trace between an artifact and its used phenomenon, or the fact that domain properties, requirement items and design decisions may only be expressed referring to phenomena that are visible in the environment, whereas design decisions and plaform properties may only be expressed referring to phenomena that are visible to the system. While the presence of such properties does not guarantee correctness, their absence indicates a problem. This is already done, to a degree, through the colour highlighting, but a reporting tool that lists all violations of those properties will be implemented.		There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, the method mentioned above<ref name="req1ref"/> lists a number of properties of a correct system description. For example, the existence of a trace between an artifact and its used phenomenon, or the fact that domain properties, requirement items and design decisions may only be expressed referring to phenomena that are visible in the environment, whereas design decisions and plaform properties may only be expressed referring to phenomena that are visible to the system. While the presence of such properties does not guarantee correctness, their absence indicates a problem. This is already done, to a degree, through the colour highlighting, but a reporting tool that lists all violations of those properties will be implemented.

	Currently, each used artifact is identified as belonging to one of the following class: domain properties, requirement items, specification elements, implementation elements, design decisions or platform properties. This in turn ~~determine~~ the different kinds of phenomena that are allowed to be used by the artefact. For the moment, the plugin does not support such classification by ~~phenomena~~ types. In a next step, we will work on a concept for classifying and maintaining phenomena with ProR.		Currently, each used artifact is identified as belonging to one of the following class: domain properties, requirement items, specification elements, implementation elements, design decisions or platform properties. This in turn determines the different kinds of phenomena that are allowed to be used by the artefact. For the moment, the plugin does not support such classification by phenomenon types. In a next step, we will work on a concept for classifying and maintaining phenomena with ProR.

	= Camille =		= Camille =

imported>Laurent at 13:08, 18 July 2012

2012-07-18T13:08:13Z

← Older revision		Revision as of 13:08, 18 July 2012
Line 18:		Line 18:
	End users asked the Rodin team to provide 32-bit and 64-bit versions of the Rodin platform for Linux and Windows operating systems. Before Rodin 2.4, the only 64-bit version of Rodin was available on Mac platforms as 32-bit Mac (early 2006) platforms are no longer maintained by Apple. The motivation that would push forward 64-bit architectures is the possibility to increase the available java heap size which is, for example, extensively used during the automated proof. After a phase of testing and despite the drawbacks of assembling and maintaining five platforms instead of three, Linux and Windows 64-bit as well as 32-bit platforms are now systematically made available since the Rodin 2.4 release.		End users asked the Rodin team to provide 32-bit and 64-bit versions of the Rodin platform for Linux and Windows operating systems. Before Rodin 2.4, the only 64-bit version of Rodin was available on Mac platforms as 32-bit Mac (early 2006) platforms are no longer maintained by Apple. The motivation that would push forward 64-bit architectures is the possibility to increase the available java heap size which is, for example, extensively used during the automated proof. After a phase of testing and despite the drawbacks of assembling and maintaining five platforms instead of three, Linux and Windows 64-bit as well as 32-bit platforms are now systematically made available since the Rodin 2.4 release.

	'''The Rodin Editor ~~and the Theory plug-in~~ in the Rodin core platform'''<br>		'''The Rodin Editor in the Rodin core platform'''<br>
	According to ~~their~~ role in the Rodin toolset, and ~~their~~ stabilization, the Rodin Editor,<ref>http://wiki.event-b.org/index.php/Rodin_Editor</ref> ~~and later the Theory plug-in<ref>http://wiki.event-b.org/index.php/Theory_Plug-in</ref> were reintegrated~~ into ~~the core platform. The Rodin Editor was released in~~ the core platform since Rodin 2.4~~, and the Theory plug-in is planned to be integrated in Rodin 2.7~~.		According to its role in the Rodin toolset, and its stabilization, the Rodin Editor,<ref>http://wiki.event-b.org/index.php/Rodin_Editor</ref> has been integrated into the core platform since Rodin release 2.4.

	== Available Documentation ==		== Available Documentation ==
Line 29:		Line 29:

	== Planning ==		== Planning ==
	Two ~~platforms~~ have been scheduled after Rodin 2.6 has been published: Rodin 2.7 followed by Rodin 3.0. Rodin 2.7 is intended to be released by the end of October 2012, and Rodin 3.0 will be available by the end of January 2013. Rodin 2.7 will be corrective. It has been scheduled to respect the 3 monthly release policy, as the Rodin 3.0 version will require more that 3 months of development. Indeed, ~~this latter~~ version of the platform is being prepared since Rodin 2.6, and will include lots of ~~refactorings~~ and evolutions in the published programming interfaces (API). Here is a non exhaustive list of the main improvements and refactorings that will be part of it:		Two releases of the core platform have been scheduled after Rodin 2.6 has been published: Rodin 2.7 followed by Rodin 3.0. Rodin 2.7 is intended to be released by the end of October 2012, and Rodin 3.0 will be available by the end of January 2013. Rodin 2.7 will be corrective. It has been scheduled to respect the 3 monthly release policy, as the Rodin 3.0 version will require more that 3 months of development. In addition, Rodin 2.7 will integrate the Theory plug-in (which is currently separate).

			Indeed, version 3.0 of the platform is being prepared since Rodin 2.6, and will include lots of refactoring and evolutions in the published programming interfaces (API). Here is a non exhaustive list of the main improvements and refactorings that will be part of it:
	*Binders will be allowed in extensions.		*Binders will be allowed in extensions.
	*The platform will be based on Eclipse 4.		*The platform will be based on Eclipse 4.

imported>Tommy: /* Planning */

2012-07-16T13:48:39Z

Planning

← Older revision		Revision as of 13:48, 16 July 2012
Line 76:		Line 76:
	The following work is planned:		The following work is planned:
	* Re-base the Event-B EMF framework on the EMF model of the Rodin database (which is now available as a result of the development of a new Rodin editor to replace the form based editor).		* Re-base the Event-B EMF framework on the EMF model of the Rodin database (which is now available as a result of the development of a new Rodin editor to replace the form based editor).
	* Re-write the Event-B generator of the ~~State~~-machine diagram editor so that it uses the generic generator from the Event-B GMF Support for Generic Diagrams framework. This will improve performance.		* Re-write the Event-B generator of the state-machine diagram editor so that it uses the generic generator from the Event-B GMF Support for Generic Diagrams framework. This will improve performance.
	* Improve the ~~State~~-machine diagram animation interface so that it supports animation of multiple diagrams.		* Improve the state-machine diagram animation interface so that it supports animation of multiple diagrams.
	* Complete the development of the new version of the UML-B Class Diagram editor.		* Complete the development of the new version of the UML-B Class Diagram editor.
	* Develop Animation interface for the Class diagram editor.		* Develop Animation interface for the Class diagram editor.

imported>Tommy: /* Motivations / Decisions */

2012-07-16T13:48:07Z

Motivations / Decisions

← Older revision		Revision as of 13:48, 16 July 2012
Line 54:		Line 54:
	* ''The Event-B GMF Diagrams Generic Support framework'' provides support for developing new diagram notations (started in the DEPLOY project but mostly developed during the ADVANCE project). It provides generic support for diagrammatic aspects of modelling extensions, and a generic validation and Event-B generation service (which has recently been added).		* ''The Event-B GMF Diagrams Generic Support framework'' provides support for developing new diagram notations (started in the DEPLOY project but mostly developed during the ADVANCE project). It provides generic support for diagrammatic aspects of modelling extensions, and a generic validation and Event-B generation service (which has recently been added).

	A new release of the ~~State~~-machine diagram editor has been made. This release corrected some problems and improved use of the generic framework features.		A new release of the state-machine diagram editor has been made. This release corrected some problems and improved use of the generic framework features.

	Work is in progress on a new version of the UML-B Class Diagram editor. This takes the same approach as the state-machines editor in that the models are contained within machines (and, in this case, also contexts) and that diagrammatic model features link to and enhance existing Event-B elements rather than generate everything. The Class diagram editor is currently a prototype and has not been released.		Work is in progress on a new version of the UML-B Class Diagram editor. This takes the same approach as the state-machines editor in that the models are contained within machines (and, in this case, also contexts) and that diagrammatic model features link to and enhance existing Event-B elements rather than generate everything. The Class diagram editor is currently a prototype and has not been released.

imported>Tommy: /* Overview */

2012-07-16T13:47:52Z

Overview

← Older revision		Revision as of 13:47, 16 July 2012
Line 42:		Line 42:
	== Overview ==		== Overview ==

	The UML-B plug-in and associated frameworks are developed and maintained by Dr Colin Snook at the University of Southampton. Significant contributions (to the latest version) have been made by Vitaly Savicks (~~State~~-machines) and Gintautas Sulskus (Class Diagrams). The UML-B plugin provides UML-like diagrammatic modelling as an extension to Event-B and the Rodin platform. UML-B is an established plug-in which will be developed and improved to support the aims of the ADVANCE project. UML-B was redeveloped during the DEPLOY project to provide closer integration with Event-B. A state-machine diagram editor is already released in this integrated version and a class diagram editor is now being developed as a prototype.		The UML-B plug-in and associated frameworks are developed and maintained by Dr Colin Snook at the University of Southampton. Significant contributions (to the latest version) have been made by Vitaly Savicks (state-machines) and Gintautas Sulskus (Class Diagrams). The UML-B plugin provides UML-like diagrammatic modelling as an extension to Event-B and the Rodin platform. UML-B is an established plug-in which will be developed and improved to support the aims of the ADVANCE project. UML-B was redeveloped during the DEPLOY project to provide closer integration with Event-B. A state-machine diagram editor is already released in this integrated version and a class diagram editor is now being developed as a prototype.
	[[Image:Umlb_cap2.jpg\|center\|A UML-B state machine and its Event-B counterpart]]		[[Image:Umlb_cap2.jpg\|center\|A UML-B state machine and its Event-B counterpart]]
	Other improvements will include new diagrammatic notations which are directly related to the aims of ADVANCE, such as component diagrams, as well as more general improvements, such as usability, and any features required by the projects industrial partners.		Other improvements will include new diagrammatic notations which are directly related to the aims of ADVANCE, such as component diagrams, as well as more general improvements, such as usability, and any features required by the projects industrial partners.

imported>Tommy: /* Motivations / Decisions */

2012-07-16T13:47:36Z

Motivations / Decisions

← Older revision		Revision as of 13:47, 16 July 2012
Line 56:		Line 56:
	A new release of the State-machine diagram editor has been made. This release corrected some problems and improved use of the generic framework features.		A new release of the State-machine diagram editor has been made. This release corrected some problems and improved use of the generic framework features.

	Work is in progress on a new version of the UML-B Class Diagram editor. This takes the same approach as the ~~State~~-machines editor in that the models are contained within ~~Machines~~ (and, in this case, also ~~Contexts~~) and that diagrammatic model features link to and enhance existing Event-B elements rather than generate everything. The Class diagram editor is currently a prototype and has not been released.		Work is in progress on a new version of the UML-B Class Diagram editor. This takes the same approach as the state-machines editor in that the models are contained within machines (and, in this case, also contexts) and that diagrammatic model features link to and enhance existing Event-B elements rather than generate everything. The Class diagram editor is currently a prototype and has not been released.

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

imported>Tommy: /* Available Documentation */

2012-07-16T13:46:40Z

Available Documentation

← Older revision		Revision as of 13:46, 16 July 2012
Line 67:		Line 67:
	http://wiki.event-b.org/index.php/Generic_Event-B_EMF_extensions (Under Construction)		http://wiki.event-b.org/index.php/Generic_Event-B_EMF_extensions (Under Construction)

	A paper exists about the Event-B ~~Statemachines~~:		A paper exists about the Event-B state-machines:
	Savicks, Vitaly, Snook, Colin and Butler, Michael (2009) ''Animation of UML-B State-machines'' in Rodin User & Developer Workshop 2010 Proceedings. Düsseldorf University, 2010.<ref>http://eprints.soton.ac.uk/268261/</ref>		Savicks, Vitaly, Snook, Colin and Butler, Michael (2009) ''Animation of UML-B State-machines'' in Rodin User & Developer Workshop 2010 Proceedings. Düsseldorf University, 2010.<ref>http://eprints.soton.ac.uk/268261/</ref>

imported>Tommy: /* Motivations / Decisions */

2012-07-16T13:46:08Z

Motivations / Decisions

← Older revision		Revision as of 13:46, 16 July 2012
Line 89:		Line 89:

	== Motivations / Decisions ==		== Motivations / Decisions ==
	State machines are frequently used to describe the behaviour of embedded systems. It is a relatively new feature in Event-B, and we augment the tool with the ability to generate code from state-machine diagrams in version 0.2.3 of the code generation feature plug-in. Implementation code is generated from the diagram itself, and no additional mark-up of the model is required; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-machines are created, using the existing state-machine plug-in, subject to the limitations described after.		State-machines are frequently used to describe the behaviour of embedded systems. It is a relatively new feature in Event-B, and we augment the tool with the ability to generate code from state-machine diagrams in version 0.2.3 of the code generation feature plug-in. Implementation code is generated from the diagram itself, and no additional mark-up of the model is required; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-machines are created, using the existing state-machine plug-in, subject to the limitations described after.

	The current code generation tool is restricted to generating code for a single Event-B machine, which may contain one or more state-machines. We have yet to explore the decomposition/composition of machines containing state-machines. In principal we should be able to apply decomposition techniques to decompose the single Event-B machine with state-machines into a number of machines, with the state-machines, or the elements of state-machines, distributed between them.		The current code generation tool is restricted to generating code for a single Event-B machine, which may contain one or more state-machines. We have yet to explore the decomposition/composition of machines containing state-machines. In principal we should be able to apply decomposition techniques to decompose the single Event-B machine with state-machines into a number of machines, with the state-machines, or the elements of state-machines, distributed between them.

imported>Tommy: /* Overview */

2012-07-16T13:44:27Z

Overview

← Older revision		Revision as of 13:44, 16 July 2012
Line 85:		Line 85:

	== Overview ==		== Overview ==
	~~We released~~ the latest Code Generation ~~Feature~~ on 30th May 2012.		The code generation feature provides the support for the generation of code from refined Event-B models. The development of the approach, and the tools to support it, involved a number of team members at Southampton. To this end a multi-tasking approach, which is conceptually similar to that of the Ada tasking model, was designed. Tasks are modelled by an extension to Event-B, called Tasking Machines which are an extension of the existing Event-B Machine component.
	~~New~~ features include code generation from state-machine diagrams.		The latest Code Generation feature was released on 30th May 2012. The new features in this release include code generation from state-machine diagrams (see UML-B).

	== Motivations / Decisions ==		== Motivations / Decisions ==