ADVANCE D3.3 General Platform Maintenance

This part concerns the general maintenance performed on the Rodin toolset within the second 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

The Rodin platform versions concerned by this deliverable are:

• 2.7 (released on 2012-11-05),
• 2.8 (released on 2013-06-20),
• 3.0 (TODO: ?).

During this second period of the ADVANCE project, the core developments have been focused on stability and design improvement. Thus, releases 2.7 and 2.8 mainly contain bug fixes, while version 3.0 prepares for future evolutions.

TODO

Motivations / Decisions

Major version Rodin 3.0
As the platform has grown in complexity, internal architecture needed adjustments in order to remain maintainable. The number of external plug-ins has increased too, raising need for core API improvements. The new major version Rodin 3.0 addresses these expectations. The API of the AST, prover tactics, have thus been reviewed. The platform code is now fully compatible with Eclipse 4.

TODO

Available Documentation

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

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

The Event-B wiki, basic source of documentation for the users and developers of the Rodin toolset, was completed by the Rodin handbook, an ultimate source of documentation which reached completion by the end of the DEPLOY project. The handbook aimed to overcome the lack of a centralized source of information providing the necessary assistance to an engineer in the need to be productive using Event-B and minimize the access to an expert user. It is continuously maintained by the various actors involved in the environment of the Rodin toolset and is available as a PDF version, a HTML version, and help contents within Rodin. Both the Rodin handbook and the Event-B wiki represent the main source of documentation about Event-B and the Rodin toolset. Finally, a channel has been created on Youtube, in order to provide video tutorials about the use of the platform. TODO

Planning

TODO

UML-B Improvements

Overview

TODO

Motivations / Decisions

TODO

Available Documentation

TODO

Planning

TODO

Code generation

Overview

TODO

Motivations / Decisions

TODO

Available Documentation

TODO

Planning

TODO

ProR

Overview

The ProR/Rodin integration plugin is developed and maintained by Lukas Ladenberger and Michael Jastram at the University of Duesseldorf. 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 formal models.

Significant contributions to the latest version of the ProR/Rodin integration plugin have been made on phenomena support (maintaining a glossary and tracing phenomena) and the integration of the tracing method for producing a system description of high quality as presented in .

Other improvements will include more general improvements, such as usability, and any features required by the projects industrial partners.

Motivations / Decisions

Phenomena Support

System descriptions are composed of phenomena and artefacts: phenomena describe the state space and state transitions of an environment and a system, while artefacts describe constraints on the state space and the state transitions. A (concrete) collection of all phenomena of a system description is called glossary of phenomena. The user is now able to maintain a glossary of phenomena in the ProR/Rodin integration plugin. The phenomena are automatically available in the different artefacts. For instance, an auto complete feature is available to the user while editing an artefact. In addition the user can define synonyms for phenomena as well as custom colours for highlighting the different phenomena in the artefacts.

Tracing Method Integration

While all required data structures exist to support the tracing method presented in, the ProR/Rodin integration plugin would benefit from more sophisticated reporting. In particular, the tracing method lists a number of properties of a correct system description. For example, the existence of a trace between an artifact and its used phenomenon, or the fact that domain properties, requirement items and design decisions may only be expressed referring to phenomena that are visible in the environment, whereas design decisions and plaform properties may only be expressed referring to phenomena that are visible to the system. While the presence of such properties does not guarantee correctness, their absence indicates a problem. A reporting tool that lists all violations of those properties would be valuable to support the user by maintaining a system description of high quality. We developed a first system description for such reporting tool by means of the tracing method. We applied Event-B for modelling and validating the different artefacts of the system description and demonstrated how the formal model can be used as a first prototype in the early development phase.

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.

Planning

TODO

Camille

Overview

TODO

Motivations / Decisions

TODO

Available Documentation

TODO

Planning

TODO