D45 Scalability - Revision history

imported>Tommy: /* Available Documentation */

2012-04-20T20:57:53Z

Available Documentation

← Older revision		Revision as of 20:57, 20 April 2012
Line 73:		Line 73:

	Camille Documentation		Camille Documentation
	* As the Camille text editor is based on the standard Eclipse editor, that documentation applies fully as well~~: <br>~~		* As the Camille text editor is based on the standard Eclipse editor, that documentation applies fully as well<ref>http://help.eclipse.org/indigo/topic/org.eclipse.platform.doc.user/concepts/concepts-6.htm Eclipse</ref>.
	~~help on Editors~~<ref>http://help.eclipse.org/indigo/topic/org.eclipse.platform.doc.user/concepts/concepts-6.htm Eclipse</ref>
	* Additional information is available in the Text Editor<ref>http://wiki.event-b.org/index.php/Text_Editor</ref> section on the wiki.		* Additional information is available in the Text Editor<ref>http://wiki.event-b.org/index.php/Text_Editor</ref> section on the wiki.
	* The Rodin Handbook<ref>http://handbook.event-b.org/</ref> provides some basic usage information in a few places.		* The Rodin Handbook<ref>http://handbook.event-b.org/</ref> provides some basic usage information in a few places.

imported>Tommy: /* Available Documentation */

2012-04-20T20:57:12Z

Available Documentation

← Older revision		Revision as of 20:57, 20 April 2012
Line 61:		Line 61:
	= Available Documentation =		= Available Documentation =
	Links for Improved Performance		Links for Improved Performance
	:*[http://wiki.event-b.org/index.php/Rodin_Performances ~~Rodin Performance]~~		:* There is a wiki page concerning the Rodin Performance<ref>http://wiki.event-b.org/index.php/Rodin_Performances</ref>.
	Links for Design Pattern Management / Generic Instantiation		Links for Design Pattern Management / Generic Instantiation
	:* ~~Silva, Renato and Butler, Michael (2009) "Supporting reuse of Event-B developments through~~ generic instantiation"<ref name="genInst1">Silva, Renato and Butler, Michael (2009) "Supporting reuse of Event-B developments through generic instantiation". In, International Conference on Formal Engineering Methods (ICFEM 09), Rio de Janeiro, Brazil, 09 - 12 Dec 2009. 19pp. (Submitted) http://eprints.soton.ac.uk/68737/</ref>		:* A paper concerning the generic instantiation is available<ref name="genInst1">Silva, Renato and Butler, Michael (2009) "Supporting reuse of Event-B developments through generic instantiation". In, International Conference on Formal Engineering Methods (ICFEM 09), Rio de Janeiro, Brazil, 09 - 12 Dec 2009. 19pp. (Submitted) http://eprints.soton.ac.uk/68737/</ref>
	:*~~The~~ article about Pattern Management on the wiki[http://wiki.event-b.org/index.php/Pattern]		:*An article about Pattern Management is published on the wiki<ref>http://wiki.event-b.org/index.php/Pattern</ref>.
	:*The article about Generic Instantiation on the wiki[http://wiki.event-b.org/index.php/Generic_Instantiation]		:*The article about Generic Instantiation on the wiki<ref>http://wiki.event-b.org/index.php/Generic_Instantiation</ref>
	Links for Edition		Links for Edition
	:Two documentation pages have been created for the Rodin Editor:		:Two documentation pages have been created for the Rodin Editor:
	:* A general page describing the editor and how it works <ref name="RodinEditorPage">http://wiki.event-b.org/index.php/Rodin_Editor</ref>		:* A general page describing the editor and how it works <ref name="RodinEditorPage">http://wiki.event-b.org/index.php/Rodin_Editor</ref>.
	:* A user guide page <ref name="RodinEditorUserManual">http://wiki.event-b.org/index.php/Rodin_Editor_User_Guide</ref>		:* A user guide page <ref name="RodinEditorUserManual">http://wiki.event-b.org/index.php/Rodin_Editor_User_Guide</ref>.
	: Moreover, a special category has been created on both SourceForge feature request<ref name="featTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651672</ref> and bug<ref name="bugTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651669</ref> trackers		: Moreover, a special category has been created on both SourceForge feature request<ref name="featTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651672</ref> and bug<ref name="bugTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651669</ref> trackers.

	Camille Documentation		Camille Documentation
	* As the Camille text editor is based on the standard Eclipse editor, that documentation applies fully as well: [http://help.eclipse.org/indigo/topic/org.eclipse.platform.doc.user/concepts/concepts-6.htm Eclipse ~~Help on Editors]~~		* As the Camille text editor is based on the standard Eclipse editor, that documentation applies fully as well: <br>
	* Additional information is available in the [http://wiki.event-b.org/index.php/Text_Editor ~~Text Editor] Section~~ on the wiki		help on Editors<ref>http://help.eclipse.org/indigo/topic/org.eclipse.platform.doc.user/concepts/concepts-6.htm Eclipse</ref>
	* The [http://handbook.event-b.org/ ~~Rodin Handbook]~~ provides some basic usage information in a few places		* Additional information is available in the Text Editor<ref>http://wiki.event-b.org/index.php/Text_Editor</ref> section on the wiki.
	* The technical report<ref name="camille-arch-tech-report">http://cobra.cs.uni-duesseldorf.de/w/Special:Publication/Weigelt2012</ref> ~~describing~~ analysis of user's needs and possible solutions		* The Rodin Handbook<ref>http://handbook.event-b.org/</ref> provides some basic usage information in a few places.
			* The technical report<ref name="camille-arch-tech-report">http://cobra.cs.uni-duesseldorf.de/w/Special:Publication/Weigelt2012</ref> describes analysis of user's needs and possible solutions.

	= Status =		= Status =

imported>Tommy: /* Available Documentation */

2012-04-20T20:49:22Z

Available Documentation

← Older revision		Revision as of 20:49, 20 April 2012
Line 72:		Line 72:
	: Moreover, a special category has been created on both SourceForge feature request<ref name="featTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651672</ref> and bug<ref name="bugTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651669</ref> trackers		: Moreover, a special category has been created on both SourceForge feature request<ref name="featTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651672</ref> and bug<ref name="bugTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651669</ref> trackers

	* Camille Documentation		Camille Documentation
	** As the Camille text editor is based on the standard Eclipse editor, that documentation applies fully as well: [http://help.eclipse.org/indigo/topic/org.eclipse.platform.doc.user/concepts/concepts-6.htm Eclipse Help on Editors]		* As the Camille text editor is based on the standard Eclipse editor, that documentation applies fully as well: [http://help.eclipse.org/indigo/topic/org.eclipse.platform.doc.user/concepts/concepts-6.htm Eclipse Help on Editors]
	** Additional information is available in the [http://wiki.event-b.org/index.php/Text_Editor Text Editor] Section on the wiki		* Additional information is available in the [http://wiki.event-b.org/index.php/Text_Editor Text Editor] Section on the wiki
	** The [http://handbook.event-b.org/ Rodin Handbook] provides some basic usage information in a few places		* The [http://handbook.event-b.org/ Rodin Handbook] provides some basic usage information in a few places
	** The technical report<ref name="camille-arch-tech-report">http://cobra.cs.uni-duesseldorf.de/w/Special:Publication/Weigelt2012</ref> describing analysis of user's needs and possible solutions		* The technical report<ref name="camille-arch-tech-report">http://cobra.cs.uni-duesseldorf.de/w/Special:Publication/Weigelt2012</ref> describing analysis of user's needs and possible solutions

	= Status =		= Status =

imported>Tommy: /* Overview */

2012-04-20T20:48:16Z

Overview

← Older revision		Revision as of 20:48, 20 April 2012
Line 1:		Line 1:
	= Overview =		= Overview =
	Three main domains concerned the scalability task during the last year of the project:		Three main domains concerned the scalability task during the last year of the project:<br>
	'''Improved Performance'''. According to the refocus mentioned in the General Platform Maintenance chapter, much of the reworking efforts performed on the core platform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed in a separate chapter.<br>		'''Improved Performance'''. According to the refocus mentioned in the General Platform Maintenance chapter, much of the reworking efforts performed on the core platform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed in a separate chapter.<br>
	'''Design pattern management / Generic Instantiation'''. Formal methods are applicable to various domains for constructing models of complex systems. However, often they lack some systematic methodological approaches, in particular in reusing existing models, for helping the development process. The objective in introducing design patterns within formal methods in general, and in Event-B in particular, is to overcome this limitation.<br>		'''Design pattern management / Generic Instantiation'''. Formal methods are applicable to various domains for constructing models of complex systems. However, often they lack some systematic methodological approaches, in particular in reusing existing models, for helping the development process. The objective in introducing design patterns within formal methods in general, and in Event-B in particular, is to overcome this limitation.<br>

imported>Tommy: /* Overview */

2012-04-20T20:47:49Z

Overview

← Older revision		Revision as of 20:47, 20 April 2012
Line 1:		Line 1:
	= Overview =		= Overview =
	'''Improved Performance''' According to the refocus mentioned in the General Platform Maintenance chapter, much of the reworking efforts performed on the core platform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed in a separate chapter.<br>		Three main domains concerned the scalability task during the last year of the project:
	'''Design pattern management / Generic Instantiation''' Formal methods are applicable to various domains for constructing models of complex systems. However, often they lack some systematic methodological approaches, in particular in reusing existing models, for helping the development process. The objective in introducing design patterns within formal methods in general, and in Event-B in particular, is to overcome this limitation.<br>		'''Improved Performance'''. According to the refocus mentioned in the General Platform Maintenance chapter, much of the reworking efforts performed on the core platform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed in a separate chapter.<br>
	'''Editors''' Along DEPLOY, edition became a central concern. Indeed, many usability issues appeard the models involved in pilots became "industrial" sized:		'''Design pattern management / Generic Instantiation'''. Formal methods are applicable to various domains for constructing models of complex systems. However, often they lack some systematic methodological approaches, in particular in reusing existing models, for helping the development process. The objective in introducing design patterns within formal methods in general, and in Event-B in particular, is to overcome this limitation.<br>
			'''Editors'''. Along DEPLOY, edition became a central concern. Indeed, many usability issues appeard the models involved in pilots became "industrial" sized:
	:*The legacy structured editor based on a form edition specific architecture reached its limits in editing such complex models. Industrial partners found this issue significant regarding the adoption of the Rodin platform in industry and providing a new structured editor correcting this issue became an important task during this last year of the DEPLOY project.		:*The legacy structured editor based on a form edition specific architecture reached its limits in editing such complex models. Industrial partners found this issue significant regarding the adoption of the Rodin platform in industry and providing a new structured editor correcting this issue became an important task during this last year of the DEPLOY project.
	:*Camille textual editor had to tackle challenges related to resources mapping and management for projects of industrial size mentioned above or even the design of extension capabilities. Extension capabilities became a major concern since the grammar could be extended with theories.		:*Camille textual editor had to tackle challenges related to resources mapping and management for projects of industrial size mentioned above or even the design of extension capabilities. Extension capabilities became a major concern since the grammar could be extended with theories.

imported>Tommy: /* Available Documentation */

2012-04-19T14:54:16Z

Available Documentation

← Older revision		Revision as of 14:54, 19 April 2012
Line 59:		Line 59:

	= Available Documentation =		= Available Documentation =
	* Links for Improved Performance		Links for Improved Performance
	:*[http://wiki.event-b.org/index.php/Rodin_Performances Rodin Performance]		:*[http://wiki.event-b.org/index.php/Rodin_Performances Rodin Performance]
	* Links for Design Pattern Management / Generic Instantiation		Links for Design Pattern Management / Generic Instantiation
	:* Silva, Renato and Butler, Michael (2009) "Supporting reuse of Event-B developments through generic instantiation"<ref name="genInst1">Silva, Renato and Butler, Michael (2009) "Supporting reuse of Event-B developments through generic instantiation". In, International Conference on Formal Engineering Methods (ICFEM 09), Rio de Janeiro, Brazil, 09 - 12 Dec 2009. 19pp. (Submitted) http://eprints.soton.ac.uk/68737/</ref>		:* Silva, Renato and Butler, Michael (2009) "Supporting reuse of Event-B developments through generic instantiation"<ref name="genInst1">Silva, Renato and Butler, Michael (2009) "Supporting reuse of Event-B developments through generic instantiation". In, International Conference on Formal Engineering Methods (ICFEM 09), Rio de Janeiro, Brazil, 09 - 12 Dec 2009. 19pp. (Submitted) http://eprints.soton.ac.uk/68737/</ref>
	:*The article about Pattern Management on the wiki[http://wiki.event-b.org/index.php/Pattern]		:*The article about Pattern Management on the wiki[http://wiki.event-b.org/index.php/Pattern]
	:*The article about Generic Instantiation on the wiki[http://wiki.event-b.org/index.php/Generic_Instantiation]		:*The article about Generic Instantiation on the wiki[http://wiki.event-b.org/index.php/Generic_Instantiation]
	* Links for Edition		Links for Edition
	:Two documentation pages have been created for the Rodin Editor:		:Two documentation pages have been created for the Rodin Editor:
	:* A general page describing the editor and how it works <ref name="RodinEditorPage">http://wiki.event-b.org/index.php/Rodin_Editor</ref>		:* A general page describing the editor and how it works <ref name="RodinEditorPage">http://wiki.event-b.org/index.php/Rodin_Editor</ref>

imported>Tommy: /* Editors */

2012-04-19T14:49:09Z

Editors

← Older revision		Revision as of 14:49, 19 April 2012
Line 51:		Line 51:
	''' Rodin Editor '''<br>		''' Rodin Editor '''<br>

	The Rodin Editor, has been built on the basis of ~~the idea put in practice in~~ the Proving UI. In fact, by using the same kind of textual component every model element is ~~described~~ as text, as would a pretty print do. The edition is made possible through the use of a unique additional graphical component that overlays the presentation of the element to ~~edit~~. It ~~lightened~~ the presentation, but also side ~~stepped~~ the use of a significant amount of greedy graphical elements. ~~There were only~~ two elements needed: the model viewer and its overlay editor!<br>		The Rodin Editor has been built on the basis of enhancements brought to the Proving UI. In fact, by using the same kind of textual component, every model element is presented as text, as would a pretty print do. The edition is made possible through the use of a unique additional graphical component that overlays the presentation of the element (to be edited). It lighten the presentation, but also side steps the use of a significant amount of greedy graphical elements. Only two graphical elements are needed for presentation and edition: the model viewer and its overlay editor!<br>
	The first public version (0.5.0) of the Rodin Editor has been released on the 13/07/2011 as a plug-in of the Rodin platform. This decision has been made in order to let the plug-in incubation for the time it is being tested and stated that no regression is introduced. The Rodin Editor since its version 0.6.1 is part of the Rodin core platform.		The first public version (0.5.0) of the Rodin Editor has been released on the 13/07/2011 as a plug-in of the Rodin platform. This decision has been made in order to let the plug-in incubation for the time it is being tested and stated that no regression is introduced. The Rodin Editor since its version 0.6.1 is part of the Rodin core platform.

imported>Tommy: /* Editors */

2012-04-19T13:54:54Z

Editors

← Older revision		Revision as of 13:54, 19 April 2012
Line 51:		Line 51:
	''' Rodin Editor '''<br>		''' Rodin Editor '''<br>

	The Rodin Editor, has been built on the basis of the ~~improvements made to~~ the Proving UI. In fact, the textual component ~~used, the SWT StyledText, allowed to describe~~ every model element as text, as would a pretty print do. The edition is made possible through the use of a unique additional graphical component that overlays the presentation of the element to edit. It lightened the presentation, but also side stepped the use of a significant amount of greedy graphical ~~because at most~~ two ~~of them are~~ needed: the model viewer and its overlay editor!<br>		The Rodin Editor, has been built on the basis of the idea put in practice in the Proving UI. In fact, by using the same kind of textual component every model element is described as text, as would a pretty print do. The edition is made possible through the use of a unique additional graphical component that overlays the presentation of the element to edit. It lightened the presentation, but also side stepped the use of a significant amount of greedy graphical elements. There were only two elements needed: the model viewer and its overlay editor!<br>
	The first public version (0.5.0) of the Rodin Editor as been released on the 13/07/2011 as a plug-in of the Rodin platform. This decision has been made in order to let the plug-in incubation for the time it is being tested and stated that no regression is introduced. The Rodin Editor since its version 0.6.1 is part of the Rodin core platform.		The first public version (0.5.0) of the Rodin Editor has been released on the 13/07/2011 as a plug-in of the Rodin platform. This decision has been made in order to let the plug-in incubation for the time it is being tested and stated that no regression is introduced. The Rodin Editor since its version 0.6.1 is part of the Rodin core platform.

	''' Camille '''<br>		''' Camille '''<br>

	Camille was quite successful, but due to the limited suitability for editing models using plug-ins, an architectural overhaul has been planned. The course of action was not obvious, however, as there are a number of possible ~~architecture~~ with varying advantages and disadvantages. Therefore, Ingo Weigelt at the University of Düsseldorf created a technical report<ref name="camille-arch-tech-report">http://cobra.cs.uni-duesseldorf.de/w/Special:Publication/Weigelt2012</ref> that analyzes the needs of the users and suggests a number of possible solutions. In the FP7 project ADVANCE, a solution will be decided upon and implemented.		Camille was quite successful, but due to the limited suitability for editing models using plug-ins, an architectural overhaul has been planned. The course of action was not obvious, however, as there are a number of possible architectures with varying advantages and disadvantages. Therefore, Ingo Weigelt at the University of Düsseldorf created a technical report<ref name="camille-arch-tech-report">http://cobra.cs.uni-duesseldorf.de/w/Special:Publication/Weigelt2012</ref> that analyzes the needs of the users and suggests a number of possible solutions. In the FP7 project ADVANCE, a solution will be decided upon and implemented.

	= Available Documentation =		= Available Documentation =

imported>Tommy: /* Improved Performance */

2012-04-19T13:51:40Z

Improved Performance

← Older revision		Revision as of 13:51, 19 April 2012
Line 34:		Line 34:
	= Choices / Decisions =		= Choices / Decisions =
	== Improved Performance ==		== Improved Performance ==
	SYSTEREL lead a two phase investigation to have a better idea of the work to be done. Each phase being followed by some refactoring of the code. Out of the early investigation, a cause and effect relationship has been found between performance loss and the various reported bugs, such as "platform hanging" bugs. Indeed, it appeared that solving the performance issues sometimes solved induced bugs as well ~~which made~~ the scalability improvement tasks encompass the maintenance goals.<br>		SYSTEREL lead a two phase investigation to have a better idea of the work to be done. Each phase being followed by some refactoring of the code. Out of the early investigation, a cause and effect relationship has been found between performance loss and the various reported bugs, such as "platform hanging" bugs. Indeed, it appeared that solving the performance issues sometimes solved induced bugs as well, making the scalability improvement tasks encompass the maintenance goals.<br>
	Later, a deeper investigation was performed where profiling and code review were the two techniques used to tackle the issues left. The profiling strategy allowed to get a better localisation of the performance loss in both UI and core code while the code review helped to understand the intrinsic misuses or drawbacks of particular components and/or architectures. The proving UI was refactored in order to use a light textual representation.		Later, a deeper investigation was performed where profiling and code review were the two techniques used to tackle the issues left. The profiling strategy allowed to get a better localisation of the performance loss in both UI and core code while the code review helped to understand the intrinsic misuses or drawbacks of particular components and/or architectures. The proving UI was refactored in order to use a light textual representation.

imported>Tommy: /* Editors */

2012-04-19T13:45:14Z

Editors

← Older revision		Revision as of 13:45, 19 April 2012
Line 89:		Line 89:
	== Editors ==		== Editors ==

	~~===~~ Rodin Editor ~~===~~		''' Rodin Editor '''

	The Rodin Editor is part of the Rodin platform since Rodin 2.4 released by end of January 2012.		The Rodin Editor is part of the Rodin platform since Rodin 2.4 released by end of January 2012.

	~~===~~ Camille ~~===~~		''' Camille '''

	Camille has been quite successful, and besides a number of bug fixes and some performance profiling and tuning, the code base has not changed much.		Camille has been quite successful, and besides a number of bug fixes and some performance profiling and tuning, the code base has not changed much.