User:Nicolas/Collections/ADVANCE D3.4 General Platform Maintenance

This part describes the general maintenance performed on the Rodin toolset within the last year of the ADVANCE project. As the maintenance is a task that concerns the whole toolset, and to ease the reading of this part of the deliverable, the maintenance section has been decomposed in a list of subsections corresponding to scopes of the toolset. All these subsections maintain the template previously defined in the introduction.

Core Rodin platform

Overview

During the last period of the ADVANCE project, the following versions of the Rodin platform have been released:

• 3.0.0 (2014-03-20)
• 3.0.1 (2014-06-11)
• 3.1.0 (2014-11-28)

The main part of the work was targeting improvements of

• stability of the platform,
• prover capabilities,
• theory support

Other running tasks consisted in answering questions on mailing lists, and processing bug tickets and feature requests.

Motivations / Decisions

The core API has been improved. In particular, the interface with the theory plug-in has been enriched so as to keep track of language changes over time, thus enforcing model and proof consistency.

New proof rules have been implemented (SIMP_EMPTY_PARTITION and SIMP_SINGLE_PARTITION). The proving experience has been enhanced with HMI that provide quick access to user-defined tactics.

The Rodin Editor stability has been improved, by fixing bugs pointed out by users.

The underlying Eclipse Platform has been upgraded to the most recent version (Eclipse 4.4.1 as of Rodin 3.1). This was required by plug-in developers who wanted to take advantage of the newest Eclipse features. While also bringing fixes to some Eclipse bugs, it prepares for future developments based on the latest technology.

For the same reasons, the code has been ported to Java 7, while remaining compatible with Java 6.

The source code is now distributed in a more developer-friendly format, so it's easier for plug-in implementers to extend Rodin as a target platform.

Available Documentation

The release notes, that appear and are maintained on the wiki, and that accompany each release, give useful information about the changes introduced by each. Moreover, two web trackers list and detail the known bugs and open feature requests:

• a sourceforge bug tracker,
• a sourceforge feature requests tracker.

Conclusion

The Rodin Platform has made significant steps in throughout the ADVANCE project. Improvements concern stability, dependability, extensibility, modeling and proving capability and, globally, convergence towards user expectancies.

UML-B Improvements

Overview

UML-B provides Class diagrams and State-machine diagrams for Event-B modelling. There are two versions of UML-B. The first, Classic UML-B, generates a complete Event-B project and all modelling is diagrammatic. The second, iUML-B, integrates diagrams inside Event-B machines and contexts and a mixture of diagrams and Event-B can be used in modelling.

During the last period of ADVANCE,

• Classic UML-B has been migrated to Rodin 3.x. During this release some improvements and bug fixes were made.
• iUML-B State-machines have undergone major functional and structural improvements including new diagram features requested by users (in particular, Critical Software in WP2) and a new Event-B generator that significantly improves performance. State-machine Animation has been integrated with BMotion Studio so that both can be run in parallel.
• iUML-B Class diagrams have been released as a prototype and are under evaluation by industrial collaborators for use in their development process.

Motivations / Decisions

While Classic UML-B is still maintained and used by some industrial collaborators, most new development focusses on the more popular iUML-B.

The iUML-B Statemachine to Event-B translator was implemented in the QVTo declarative language. This suffered performance problems due to the need to recompile on each invocation. The translation was re-written using our own Java based generator framework which greatly improves performance.

For valiation purposes users find visual animations very powerful and we have used both the State-machine animation and BMotionStudio in our collaborations with industry. However, previously, only one or the other could be launched at any particular time. A facility to also automatically launch any associated and open BMotionStudio editor was added to the launch process of the state-machine editor. Both animations run from the same ProB animation instance. This provides an extremely strong visualisation of the model for validation purposes as the image representations of BMotion Studio complement the state-machine visualisation and vice versa.

The iUML-B class diagram plug-in was delayed as it was not the highest priority for ADVANCE partners. However, other industrial users (e.g. Thales, Austria) are interested in switching away from the Classic UML-B tool. A prototype release of iUML-B Class diagrams has now been made available to these industrial collaborators for evaluation purposes. A full release will be made by the end of 2014. During recent development of the plug-in, the mechanism for data elaboration has been rationalised and additional modelling features have been added which make the modelling tool more effective.

Available Documentation

An overview and tutorial of both Classic UML-B and iUML-B can be found on the Event-B wiki.

Conclusion

iUML-B state-machines and animation have been significantly improved throughout ADVANCE and now represent a mature and popular tool. iUML-B class diagrams promise to be equally successful as early indications are that the approach to data elaboration is effective.

Classic UML-B will continued to be maintained but no new features are being added unless specifically requested by an industrial partner.

ProR/Rodin Integration Plugin

Overview

ProR is a tool for working with requirements in natural language. It is part of the Eclipse Requirements Modeling Framework (RMF). The goal of the ProR/Rodin integration plugin is to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. The ProR/Rodin integration plugin supports the user by maintaining a traceability between natural language requirements and Event-B models.

A requirements Meta-Model for the WP-1 and WP-2 industrial case studies has been developed during the last period of the ADVANCE project. Moreover, several requested features were added. For instance, when the user selects a linked element (guard, invariant, etc.) in the requirements document, the tool takes the user directly to the corresponding element in the Event-B model. First experiments have been made towards a feature to automatically generate reports from ProR. Beside this, general improvements, such as usability improvements have been made on the ProR/Rodin integration plugin during the last period of the ADVANCE project.

Motivations / Decisions

The ProR/Rodin integration plugin provides a default Meta-Model for requirements documents. However, this Meta-Model does not support all specific needs and characteristics of the industrial case studies. As a consequence, we decided to create a new requirements Meta-Model that supports the specific needs of both industrial case studies.

In order to improve the usability and the integration between the ProR tool and the Rodin platform, a new feature has been added to switch between the requirements document and the Event-B model. Whenever the user selects a linked element (guard, invariant, etc.) in the requirements document, the tool takes the user directly to the corresponding element in the Event-B model.

The ability to generate reports is important. For instance, it is desirable to see statistics (the number of requirements currently covered by the model) so that this can be presented to a customer during progress meetings. In order to meet this goal, first experiments towards a reporting tool for ProR have been made during the ADVANCE Project.

Available Documentation

• A Method and Tool for Tracing Requirements into Specifications. Accepted for Science of Computer Programming.
• Requirements Traceability between Textual Requirements and Formal Models Using ProR. The paper has been accepted for iFM'2012 & ABZ'2012.

• A Tutorial for the Rodin/ProR integration can be found on the Event-B wiki.
• The User Guide contains additional tutorials for ProR.

Conclusion

The customized Meta-Models facilitated the requirements maintenance process of both industrial case studies. Moreover, the new Meta-Model is expandable so that new features can be easily added later in the project.

Camille

Overview

The Camille plug-in provides a textual editor for Rodin. This editor provides the same look and feel as a typical Eclipse text editor, including features most text editors provide, such as copy, paste, syntax highlighting and code completion.

During the last period of the ADVANCE project, three new versions of Camille have been released:

• 3.0.0 - Initial release for version 3 of the Core Rodin platform. This release has been based on Camille 2.1.4.
• 3.0.1 - Port of the changes done in Camille 2.2.0 to version 3. This includes theorems in guards as well as other bugfixes. See D3.3 for details.
• 3.0.2 - Camille's structure parser has been moved to ProB's parser library. A fully automatic build process featuring continuous integration has been set up. This is the first release build by it.

One of the main goals of the last period was the support of Rodin's extensibility in Camille.

Motivations / Decisions

Move to Git / GitHub

The source files for Camille have been moved from the old Rodin SVN repository to their own repository at GitHub. The old source files have been marked deprecated. Furthermore, the move to GitHub allows us to use GitHub's infrastructure for bug tracking and feature requests. We moved old feature requests from the wiki pages to the bug / feature tracking systems at GitHub.

Build Process

Before version 3.0.2 was released, the Camille build was mostly done by hand. This turned out to be slowing down development during the last period of the ADVANCE project. Starting with release 3.0.2 we completely revamped the build process. Camille is now build automatically on each commit using a Jenkins continuous integration server . This facilitates the build as well as the release process for Camille. Furthermore, it should ease collaborative development.

Move Structure Parser to ProB's Parser Library

Camille's internal parser for the structure of Event-B machines and contexts has been split off of Camille and moved to ProB's general parsers library. Hence, the parser is now a completely separate project that can be developed independently of Camille. This further decouples Camille's core, ui and parsers. Externalising the parser is the first step to making Camille more modular in oder to be able to replace the parser by the upcoming block parser. In addition, externalising the parser makes it available for other projects as well.

Available Documentation

• Architectures for an Extensible Text Editor for Rodin. Bachelor thesis analysing the problem and discussing possible solutions.
• An earlier version of the thesis has been published as a technical report that has been discussed on the Roding Developers Mailing List and the ADVANCE Progress Meeting in May 2012 in Paris.
• Camille GitHub Repository and Bugtracker: https://github.com/hhu-stups/camille
• Camille Wiki: http://wiki.event-b.org/index.php/Camille_Editor

Conclusion

Camille still has the drawback of not supporting extensibility. It only supports the core Event-B language and plug-in-specific additions are simply ignored. Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions. However, Camille was extended in oder to preserve plug-in specific additions. This change allows switching between Camille and the other editors without loosing plugin specific information that Camille can not display. The changes and improvements to the development process performed in the last period should finally allow for a new and completely overhauled version of Camille to be implemented.