D45 Scalability

Overview

Three main domains concerned the scalability task during the last year of the project:
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. 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.
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.
• 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.

Motivations

Improved Performance

Many issues concerning stability and performance were related to the core code of the Rodin platform, causing crashes, loss of data, corruption in models. Other issues 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. Addressing these issues before the end of DEPLOY was mandatory.

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.

Editors

This section concerns the actual editors that user work with to view and modify models.

Editor of the core platform

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 situation 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 were 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.

Camille

Camille was developed as an alternative editor in 2009. In contrast to the existing editor, this was a pure textual editor that supported standard features like copy and paste, auto-completion, color highlighting and many more. In addition, it performed better than the existing structural editor.

While successful, Camille offered only limited support for models with extended elements contributed by plug-ins. Also, the underlying EMF Compare framework was problematic due to bugs and performance issues.

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, making 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

In our notion of design patterns, a pattern is just a development in Event-B including an abstract model called specification and a refinement. During development there might be the possibility of applying a pattern that was already developed to the current development. The steps of using the tool are as follows.

Matching The developer the starts the design pattern plug-in and manually matches the specification of the pattern with the current development. In this linking of pattern and problem the developer has to define the which variable in the current development corresponds to each variable in the pattern specification. Furthermore the developer has to ensure the consistency of the variable matching by matching the events of the pattern specification with events in the development.

Renaming Once the matching is done, the developer has the possibility to adapt the pattern refinement such as renaming the variables and events or merging events of the pattern refinement with uninvolved events of the development. Renaming can become mandatory there are name clashes, meaning the pattern refinement includes variable or events having the same name as existing elements in the development.

After adaptation of the pattern refinement the tool generates automatically a new Event-B machine as a refinement of the machine where the developer started the design pattern tool. The correctness of the generated machine being a refinement is guaranteed by the generation process of the tool.

Design Patterns in Event-B are nothing else than ordinary Event-B models and are not restricted with respect to their size. Due to the fact that pattern and development have to be matched manually by the developer, the size of a pattern effects the usability. Furthermore, if the pattern is too specific either the pattern cannot be used in most situations or the developer is forced to tune its development such that a further appliance of the pattern is possible. A pattern-driven development could thus lead to models including needless elements that would have been avoided when developing without patterns.

Editors

Rodin Editor

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!
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

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 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

Links for Improved Performance

• There is a wiki page concerning the Rodin Performance.

Links for Design Pattern Management / Generic Instantiation

• A paper concerning the generic instantiation is available
• An article about Pattern Management is published on the wiki.
• The article about Generic Instantiation on the wiki

Links for Edition

Two documentation pages have been created for the Rodin Editor:

• A general page describing the editor and how it works .
• A user guide page .

Moreover, a special category has been created on both SourceForge feature request and bug trackers.

Camille Documentation

• As the Camille text editor is based on the standard Eclipse editor, that documentation applies fully as well.
• Additional information is available in the Text Editor section on the wiki.
• The Rodin Handbook provides some basic usage information in a few places.
• The technical report describes analysis of user's needs and possible solutions.

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

The Generic Instantiation plug-in is available in version 0.2.1 for Rodin 2.4 and above from the main Rodin Update Site in the Composition and Decomposition category.

Editors

Rodin Editor

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

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.