Difference between pages "D32 Introduction" and "D45 Scalability"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
(Initial commit)
 
imported>Tommy
 
Line 1: Line 1:
The DEPLOY's D32 deliverable is composed of:
+
= Overview =
* The Rodin core platform and plug-ins (i.e. the DEPLOY tools).
+
* '''Improved Performance''' According to the refocus mentionned in the [[D45_General_Platform_Maintenance#Motivations| General Platform Maintenance]] chapter, much of the reworking efforts performed on the core plateform 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.
* This document.
+
* '''Design pattern management / Generic Instantiation''' {{TODO}} An overview of the contribution about the design pattern management / Generic Instantiation (Thai Son Hoang)  
The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]).
+
* '''Edition''' It appeard along DEPLOY, the models defined by pilots becoming industrial sized due to the level of complexity reached, that the edition became a central concern.  
 +
:*The legacy structured editor based on a form edition specific achitecture reach its limits in responsivness and hence in usability when being constrained to display a huge amount of graphical elements. Industrial partners found this issue significant regarding the adoption of the rodin platform in industry and that is why providing a new editor that would solve them has been a main task during this last year of the DEPLOY project.
 +
:*Camille textual editor had to tackle challenges related to ressources mapping and management for projects of industrial size mentionned above or even the design of extension capabilities, that became a major concern since the grammar could be extended with theories.
  
This document gives a description of the work that was carried on during the second year of the DEPLOY project (Feb 2009-Jan 2010), in the course of the WP9 ''Tooling research and development'' work package, and brings new perspectives for the coming year.
+
= Motivations =
  
In particular, the WP9 partners have strovin to meet the following objectives:
+
== Improved Performance ==
* Improved scalability of the Rodin platform to support industrial deployments, through GUI enhancements (smart completion, renaming, text editing, etc), decomposition support and design-pattern management.
+
It appeared that the various DEPLOY partners encountered several major issues while editing large models. Some were related to the core code of the Rodin platform, causing crashes, loss of data, corruption in models. Some other were related to the UI causing platform hanging, and sometimes leading to its freezing which required sometimes to kill the Rodin process, thus also leading to potential loss of data and corruption in models. Hence, it appeared necessary to solve such issues before the end of DEPLOY.
* Prover integrity and performance, to enhance the confidence in provers and to enlarge their proving capabilities. To this aim, the existing provers have been improved and a new rule-based prover plug-in has been implemented.
 
* Model animation and testing, to validate Event-B models. More precisely, the ProB or AnimB plug-ins allow a domain expert to detect errors in a model and ensure the presence of desired functionalities. Moreover, it is very important for many industrial applications to be able to completely hide the underlying formal specification.
 
* Model checking (ProB), to enable users to find sequences of events that prevent safety properties or proof obligations to be fulfilled.
 
* UML integration. UML-B provides a diagrammatic, formal modelling notation based on UML.
 
* Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An initial definition of language support for code generation has been put forward.
 
  
This document covers the following items: general platform maintenance, UML-B improvements, ProB improvements, text editor plug-in, decomposition plug-in, initial definition of language support for code generation, improvements to existing provers, rule-based prover, pattern plug-in, flow plug-in and modularisation plug-in.  
+
== Design Pattern Management / Generic Instantiation  ==
 +
{{TODO}} ''To be completed by Thai Son Hoang''
 +
== Edition ==
 +
* The motivations behind the creation of the new textual structured editor mainly concern performance but not only. From the growing size of complexity reached in models inducing a growing of their physical size lead the platform to its limits. Two major kinds of failures were faced when developing such models:
 +
:* failures occuring on windows platforms, the mostly used system, when reaching the operating system limit number of graphical elements in memory allowed to be displayed at once. This bug used to crash the Rodin platform, and it appeared necessary to control the number of graphical elements needed to display the model elements. Architectures sparing these graphical elements should be thus favoured.
 +
:* failures due to the high consumption of memory by the heavy graphical elements used by the forms of legacy editor.
 +
:Moreover, it appeared important to visualize some elements that are not part of the current level of modelling, but are linked to it, for exemple, the actions in an abastract event, or its guards. Such elements are called the "inherited" elements, or "implicit children". The legacy structured editor being directly interfaced with the underlying Event-B models in database, it was difficult and tricky to modify it in order to display inherited elements. This was one more argument to go for a new editor based on a intermediary representation of the models.
 +
:Another motivation to go for another editor was to get a more modest and ergonomic way to visualize and edit the models. The models being presented through styled text pretty printing and the edition thightly derived from a textual edition.
  
For each of these newly implemented features or improvements, the document is structured as follows:
+
* The motivations about Camille evolution {{TODO}} Ingo Weigelt.
* Overview. The involved partners are identified and an overview of the contribution is given.
 
* Motivations. The motivations for each tool extension and improvement are expressed.
 
* Choices / decisions. The decisions (e.g. design decisions) are justified.
 
* Available documentation. Some pointers to the Event-B wiki or related publications are listed.
 
* Planning. A timeline and the current status (as of 29 Jan 2010) is given.
 
  
[[Category:D23 Deliverable]]
+
= Choices / Decisions =
 +
== 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 perfomance loss and the various reported bugs, such as "platform hanging" bugs or even "no more handle" bugs related to the high consumption of graphical elements on Windows platforms. Indeed, it appeared that solving the performance issues sometimes solved induced bugs as well which made the scalability improvement tasks emcompass the maintenance goals.<br>
 +
Later, a deeper investigation was performed, to indentify and tackle the remaining performance issues. Profiling and code review were the two techniques used. 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.
 +
A good example, was the Event-B built-in editor based on form editors with a high use of greedy graphical components. Such architecture appeard to be weak when it was needed to display industrial size models. This affected the modelling experience with some long, and really annoying to the user, reaction lags. To solve such issue, it has been chosen to refactor the editors using a textual representation which was a light-weight graphical alternative to lower the number of needed components.
 +
 
 +
== Design Pattern Management / Generic Instantiation  ==
 +
{{TODO}} ''To be completed by Thai Son Hoang''
 +
== Edition ==
 +
* Rodin Editor
 +
As previously said, the legacy editor drawbacks mainly come from its greedy components and structure. However, a structured way to edit the models (based on a database storage) seams still particularly appropriate. This mainly explains why a new structured editor, the Rodin Editor, has been build to keep a structured edition of the model contents on the basis of the improvements made to the Proving UI.  In fact, the textual component, the SWT StyledText, used in this latter UI element significantly improved the modelling experience. Hence, every element modelled in the Rodin editor is described as text. Not only this lightened the presentation, but also side stepped the use of a significant amount of greedy graphical components. Although using this technique makes models look like plain text, it is just a sort of pretty printing and they remain edited and stored by the database. The edition is then possible through the use of a unique additional graphical component that overlays the presentation of the element to edit. This drastically reduces the memory consumption as well as the number of needed graphical components because at most two of them are needed!<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 in incubation for the time it is being tested and stated that no regression is introduced. The Rodin Editor since its version xx is part of the Rodin Core Platform.
 +
* Camille
 +
{{TODO}} Ingo Weigelt
 +
 
 +
= Available Documentation =
 +
* {{TODO}} Links for Improved Performance
 +
* {{TODO}} Links for Design Pattern Management / Generic Instantiation
 +
* Links for Edition
 +
:Rodin Editor
 +
:Two documentation pages have been created :
 +
::* 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>
 +
:: 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
 +
 
 +
= Status =
 +
== Improved Performance ==
 +
The refactoring made on both core code and UI code allowed to gain up to 25 times speed-up on the UI, and almost a 2 times speed-up in the core code, making the platform usable in an industrial sized context.<br>
 +
 
 +
== Design Pattern Management / Generic Instantiation  ==
 +
{{TODO}} ''To be completed by Thai Son Hoang''
 +
== Edition ==
 +
{{TODO}} ''To be completed by Thomas Muller, Ingo Weigelt''
 +
 
 +
 
 +
= References =
 +
<references/>
 +
 
 +
[[Category:D45 Deliverable]]

Revision as of 09:57, 23 November 2011

Overview

  • Improved Performance According to the refocus mentionned in the General Platform Maintenance chapter, much of the reworking efforts performed on the core plateform 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.
  • Design pattern management / Generic Instantiation TODO An overview of the contribution about the design pattern management / Generic Instantiation (Thai Son Hoang)
  • Edition It appeard along DEPLOY, the models defined by pilots becoming industrial sized due to the level of complexity reached, that the edition became a central concern.
  • The legacy structured editor based on a form edition specific achitecture reach its limits in responsivness and hence in usability when being constrained to display a huge amount of graphical elements. Industrial partners found this issue significant regarding the adoption of the rodin platform in industry and that is why providing a new editor that would solve them has been a main task during this last year of the DEPLOY project.
  • Camille textual editor had to tackle challenges related to ressources mapping and management for projects of industrial size mentionned above or even the design of extension capabilities, that became a major concern since the grammar could be extended with theories.

Motivations

Improved Performance

It appeared that the various DEPLOY partners encountered several major issues while editing large models. Some were related to the core code of the Rodin platform, causing crashes, loss of data, corruption in models. Some other were related to the UI causing platform hanging, and sometimes leading to its freezing which required sometimes to kill the Rodin process, thus also leading to potential loss of data and corruption in models. Hence, it appeared necessary to solve such issues before the end of DEPLOY.

Design Pattern Management / Generic Instantiation

TODO To be completed by Thai Son Hoang

Edition

  • The motivations behind the creation of the new textual structured editor mainly concern performance but not only. From the growing size of complexity reached in models inducing a growing of their physical size lead the platform to its limits. Two major kinds of failures were faced when developing such models:
  • failures occuring on windows platforms, the mostly used system, when reaching the operating system limit number of graphical elements in memory allowed to be displayed at once. This bug used to crash the Rodin platform, and it appeared necessary to control the number of graphical elements needed to display the model elements. Architectures sparing these graphical elements should be thus favoured.
  • failures due to the high consumption of memory by the heavy graphical elements used by the forms of legacy editor.
Moreover, it appeared important to visualize some elements that are not part of the current level of modelling, but are linked to it, for exemple, the actions in an abastract event, or its guards. Such elements are called the "inherited" elements, or "implicit children". The legacy structured editor being directly interfaced with the underlying Event-B models in database, it was difficult and tricky to modify it in order to display inherited elements. This was one more argument to go for a new editor based on a intermediary representation of the models.
Another motivation to go for another editor was to get a more modest and ergonomic way to visualize and edit the models. The models being presented through styled text pretty printing and the edition thightly derived from a textual edition.
  • The motivations about Camille evolution TODO Ingo Weigelt.

Choices / Decisions

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 perfomance loss and the various reported bugs, such as "platform hanging" bugs or even "no more handle" bugs related to the high consumption of graphical elements on Windows platforms. Indeed, it appeared that solving the performance issues sometimes solved induced bugs as well which made the scalability improvement tasks emcompass the maintenance goals.
Later, a deeper investigation was performed, to indentify and tackle the remaining performance issues. Profiling and code review were the two techniques used. 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. A good example, was the Event-B built-in editor based on form editors with a high use of greedy graphical components. Such architecture appeard to be weak when it was needed to display industrial size models. This affected the modelling experience with some long, and really annoying to the user, reaction lags. To solve such issue, it has been chosen to refactor the editors using a textual representation which was a light-weight graphical alternative to lower the number of needed components.

Design Pattern Management / Generic Instantiation

TODO To be completed by Thai Son Hoang

Edition

  • Rodin Editor

As previously said, the legacy editor drawbacks mainly come from its greedy components and structure. However, a structured way to edit the models (based on a database storage) seams still particularly appropriate. This mainly explains why a new structured editor, the Rodin Editor, has been build to keep a structured edition of the model contents on the basis of the improvements made to the Proving UI. In fact, the textual component, the SWT StyledText, used in this latter UI element significantly improved the modelling experience. Hence, every element modelled in the Rodin editor is described as text. Not only this lightened the presentation, but also side stepped the use of a significant amount of greedy graphical components. Although using this technique makes models look like plain text, it is just a sort of pretty printing and they remain edited and stored by the database. The edition is then possible through the use of a unique additional graphical component that overlays the presentation of the element to edit. This drastically reduces the memory consumption as well as the number of needed graphical components because at most two of them are needed!
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 in incubation for the time it is being tested and stated that no regression is introduced. The Rodin Editor since its version xx is part of the Rodin Core Platform.

  • Camille

TODO Ingo Weigelt

Available Documentation

  • TODO Links for Improved Performance
  • TODO Links for Design Pattern Management / Generic Instantiation
  • Links for Edition
Rodin Editor
Two documentation pages have been created :
  • A general page describing the editor and how it works [1]
  • A user guide page [2]
Moreover, a special category has been created on both sourceforge feature request[3] and bug[4] trackers.
Camille

Status

Improved Performance

The refactoring made on both core code and UI code allowed to gain up to 25 times speed-up on the UI, and almost a 2 times speed-up in the core code, making the platform usable in an industrial sized context.

Design Pattern Management / Generic Instantiation

TODO To be completed by Thai Son Hoang

Edition

TODO To be completed by Thomas Muller, Ingo Weigelt


References