ADVANCE D3.3 General Platform Maintenance

This part describes 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

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

• 2.7 (2012-11-05),
• 2.8 (2013-06-20),
• 3.0 (2013-09-30).

The main focus of the maintenance activities was twofold : firstly, to accommodate the needs of the case-study workpackages WP1 and WP2, and secondly to improve the soundness of the core tools and to ease the development of external plug-ins by providing easier to use Application Programming Interface (API). Thus, releases 2.7 and 2.8 mainly contain bug fixes and small improvements, while version 3.0 is a clean up of the core mechanisms preparing for the future.

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

Motivations / Decisions

Besides implementing the features needed and fixing the bugs detected by the case studies, which always have top priority, the maintenance of the core platform in the second period of the project was devoted to fixing soundness bugs in the core platform, cleaning up the API and providing structure to the Rodin database.

Starting from a usability issue reported by the WP2 case study, we dug into the roots of the reported problem. This led us to find out that the core platform, although working well in general, was too permissive as concerns mathematical extensions. It was possible to declare meaningless empty data types, to freely mix incompatible mathematical extensions and several other oddities. In all these cases, the invariants normally guaranteed by the core platform and on which the soundness of the proofs rely were violated. Although the Rodin editors did not allow the users to input such invalid entries, these API weaknesses were a major concern as regards overall platform reliability. It was therefore needed to strengthen the way mathematical extensions could be added to the mathematical language to ensure that proofs are always sound.

The latest major version of the Rodin platform was Rodin 2.0, released in October 2010. Since that release, a lot of new features have been developed, but always keeping the API backward compatible, to comply with the Eclipse standard of release numbering. Consequently, old versions of features, marked as deprecated, had to be kept along with new ones. The middle of the ADVANCE project was considered the best time for performing a clean up of old API parts by releasing a new major version.

Finally, the Rodin database up to Rodin 3.0 was not enforcing any database schema. This seemed a good idea initially, but in retrospect, this lack of schema made life unnecessarily difficult for plug-in developers. Firstly, it was difficult to find out which database items were considered by each plug-in, as the only place where this information was present was in either the plug-in documentation (if present) or buried into the plug-in code. Moreover, if by chance a plug-in wrote database elements in the wrong place, nothing would indicate it, which led to nasty and difficult to analyse bugs. We have therefore added a notion of schema in the database of Rodin 3.0.

Concerning model editors, we have improved readability in Event-B editor by moving a few buttons outside the editing area. This enhancement originated from a user who has contributed a patch for it. The stability of the newer generic Rodin editor has also been improved.

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.

Specially for Rodin 3.0 which introduces incompatible changes, a Plug-in Migration Guide has been written.

The Event-B wiki, basic source of documentation for the users and developers of the Rodin toolset, is completed by the Rodin handbook, an ultimate source of documentation which reached completion by the end of the DEPLOY project. The handbook aims at overcomimg 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 in PDF and HTML format, as well as integrated in the on-line help within the Rodin platform. 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. It provides video tutorials about using the platform.

Planning

The plans for the third and last period of the ADVANCE project are to come back to a four month schedule between releases:

• 3.1 in January 2014,
• 3.2 in May 2014 and
• 3.3 in September 2014.

As usual the main driver for the maintenance activity will be the feedback provided by the case studies.

UML-B Improvements

Overview

UML-B provides a diagrammatic front end to Event-B to assist in constructing models. UML-B is UML-like. It is semantically and syntactically different from UML but should feel familiar to UML users. There are two variants of UML-B. Classic UML-B is self contained (i.e. all modelling is done on the diagram) and a read-only Event-B project is automatically generated for verification. Classic UML-B provides project diagrams to show the machine refinement structure, class diagrams to provide object oriented lifting and state-machine diagrams to provide event sequencing. The more recent iUML-B (i for integrated) consists of a collection of diagrams which contribute additional modelling aspects to an extant Event-B machine (i.e. some of the modelling is still done in an Event-B machine). iUML-B currently provides a project diagram, and state-machine diagram. iUML-B class diagrams are currently under development and component diagrams are planned for future developemnt. The University of Southampton is responsible for UML-B.

Motivations / Decisions

In general, classic UML-B is maintained but not substantially developed. Some improvements have been made in response to user requests. These include improved property fields for text entry and fixing a handles leak that causes problems on the Windows platform.

The development of iUML-B comprises improvement of the State-machines plug-in and development of a new class diagram plug-in.

The following improvements have been made to the state-machines plug-in:

• It is now possible to animate several state-machines simultaneously within the same machine.
• It is often necessary to have several editors open on the same machine which can lead to conflicting changes. The default option has been changed to save automatically whenever the diagram editor loses focus.
• Often, it is desired to change or delete an event while working on transitions. A property sheet button to remove an event from a transition and delete it at the same time has been added.
• If a diagram is deleted from a machine, any associated diagram files are now deleted at the same time.
• A number of inconsistencies in the translation to Event-B have been corrected

The following improvements are currently being implemented:

• It is sometimes needed to elaborate several events but apply a common guard and/or action to them all. Transitions may now own guards and actions which are generated into all of its elaborated events.
• The current translations require a new enumeration for every state-machine. Often, it would be convenient to have several state-machines with the same type or to utilise an existing enumeration for type. A special case of this is a 2-state state machine that would most naturally be represented as a single Boolean value. This will be done by allowing a state machine to be linked to an existing variable.
• In some cases it would be useful to split a state-machine into several overlaid diagrams, for example, to segregate some kinds of transitions. This will be done by allowing a state machine to be linked to an existing variable.
• There is sometimes a requirement for a transition to originate from a group of source states and it is not always possible to deal with this via hierarchical states. This will be implemented via a pseudo-state that represents the merging of the source transitions.

The major features of the class-diagram plug-in are:

• Classes, attributes and associations link to (elaborate) existing data items (sets, constants or variables) that are in scope of the containing machine or context (via refines, sees or extends). This allows further attributes and associations to be added to an existing class which may be based in another machine or context.
• Class methods are linked to existing Event-B events in a many-many relationship providing a flexible mechanism to allocate parts of an event to classes based on responsibility.

Available Documentation

Documentation on classic UML-B: http://wiki.event-b.org/index.php/Original_UML-B

Documentation on iUML-B: http://wiki.event-b.org/index.php/IUML-B

Tutorial on iUML-B statemachines: http://www.youtube.com/watch?v=nz7ZpL2JtAM

Planning

The current aims are to complete the remaining improvements to the statemachines plug-in and complete the release of the Class diagrams plug-in. It is hoped that these plug-ins will provide a very flexibly diagrammatic modelling notation. The plug-ins will then be evaluated on a case study.

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.

The following significant contributions to the latest version of the ProR/Rodin integration plugin have been made during the second period of the ADVANCE project:

• Phenomena support (maintaining a glossary and tracing phenomena)
• Integration of the tracing method for producing a high quality system description

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, 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 specification elements and platform 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 requriements analyzer 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 requriements analyzer 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

The following work is planned:

• Further work on the development of the system description for the requriements analyzer tool that supports the user by maintaining a consistent system description
• Applying the tracing method on the case studies of the industrial partners

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.

The latest release finally supports the full core Event-B language as it is supported by the built-in editors too.

Motivations / Decisions

A new version of the editor has been published to support the full feature of the core Event-B language. Event guards can now be defined as theorems as it is possible in the other Rodin editors. With this version all core Event-B models can be edited solely with Camille. It is no longer necessary to switch between different Editors.

To further improve the user experience, the syntax was slightly modified. With the new syntax all model elements now occur in the same order in every editor and pretty print. This finally lead to a more consistent modelling experience within the Rodin platform.

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.

Planning

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. A new version of Camille will be implemented during the ADVANCE project. Plug-in Developers will be able to provide syntax contributions and parsers for their extensions. By this users will be able to edit extended Event-B models solely through a text editor.