D45 Scalability: Difference between revisions
imported>Tommy |
imported>Tommy |
||
| Line 12: | Line 12: | ||
== Design Pattern Management / Generic Instantiation == | == Design Pattern Management / Generic Instantiation == | ||
The idea of design patterns in software engineering is to have a general and reusable solution to commonly occurring problems. In general, a design pattern is not necessarily a finished product, but rather a template on how to solve a problem which can be used in many different situations. The idea is to have some predefined solutions, and incorporate them into the development with some modification and/or instantiation. With the design pattern tool we provide a semi-automatical way of reusing developed models in | The idea of design patterns in software engineering is to have a general and reusable solution to commonly occurring problems. In general, a design pattern is not necessarily a finished product, but rather a template on how to solve a problem which can be used in many different situations. The idea is to have some predefined solutions, and incorporate them into the development with some modification and/or instantiation. With the design pattern tool we provide a semi-automatical way of reusing developed models in Event-B. Moreover, the typical elements that we are able to reuse are not only the models themselves, but also (more importantly) their correctness in terms of proofs associated with the models. | ||
== Edition == | == Edition == | ||
Two major kinds of failures were faced when developing industrial sized models: | Two major kinds of failures were faced when developing industrial sized models: | ||
Revision as of 15:56, 28 November 2011
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.
- Design pattern management / Generic Instantiation TODO An overview of the contribution about the design pattern management / Generic Instantiation (Thai Son Hoang)
- Edition It appears 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 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 a 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, that became a major concern since the grammar could be extended with theories.
Motivations
Improved Performance
Some of the several major stability and performance issues faced 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. It was necessary to solve such issues before the end of DEPLOY.
Design Pattern Management / Generic Instantiation
The idea of design patterns in software engineering is to have a general and reusable solution to commonly occurring problems. In general, a design pattern is not necessarily a finished product, but rather a template on how to solve a problem which can be used in many different situations. The idea is to have some predefined solutions, and incorporate them into the development with some modification and/or instantiation. With the design pattern tool we provide a semi-automatical way of reusing developed models in Event-B. Moreover, the typical elements that we are able to reuse are not only the models themselves, but also (more importantly) their correctness in terms of proofs associated with the models.
Edition
Two major kinds of failures were faced when developing industrial sized models:
- Failures occurring 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 example, the actions in an abstract 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 tightly 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 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.
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.
Design Pattern Management / Generic Instantiation
TODO To be completed by Thai Son Hoang
Edition
- Rodin Editor
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!
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 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
- Two documentation pages have been created for the Rodin Editor:
- Moreover, a special category has been created on both SourceForge feature request[3] and bug[4] trackers.
- TODO Ingo 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 (as described below),
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
The Rodin Editor is part of the Rodin plateform since. As the time of writing this document, the current version is xx.
