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

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 (planned for release on 2013-09-30).

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

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.

Code generation

Overview

The code generation feature provides the support for the generation of code from refined Event-B models. Target languages include Ada, Java, and OpenMP C. The approach, and the tools to support it, was created by a team from the University of Southampton. The top-down structuring allows abstract specification of multi-tasking controller software, together with its environment. Using refinement, decomposition and Tasking Event-B, Event-B models can be annotated and used to generate code. Tasking Machines are an extension of the existing Event-B Machine component, and are used to specify tasks (thread-like behaviours). The last Code Generation feature was released on 30th May 2012, an updated version is expected soon. The last version of Tasking Event-B was a demonstrator tool, used as a proof of concept. The methodology included a large number of manual tasks. The new version has seen the introduction of some productivity enhancements and bug fixes, and a shift in focus from generating Ada source code to Java. Much of the code generation process has now been automated, thus relieving the burden on the developer. The new release also includes important changes to the Java code generator, to allow generated code to run in Eclipse without significant editing.

Motivations / Decisions

Many of the tool improvements in this area have been achieved in tandem (50-50 split) with a separate, but parallel running, piece of work. The tandem project was a feasibility study with an industrial partner (Thales Transportation - Germany). The study involved the modelling of controller software, and of the hardware environment, of a small fan controller. It is the first significant analysis of Tasking Event-B by anyone in industry; since the code generation feature had not matured to the point where it was of interest in previous projects. The aim of the feasibility study was to evaluate the complete Event-B methodology, from abstract specification to Java implementation. This was done as part of an assessment of the tool-set, to judge if Event-B was suitable for use in a large-scale railway signalling project. Details of this work are included in a paper, yet to be submitted. One result of the study was a list of feature requests, which have been added to the Rodin SourceForge repository at.

In separate work, the generation of code from Event-B models for use as Functional Mock-up Units (FMUs), has been evaluated. Hand coded versions of would-be generated code has been produced, in order to understand what is required to be done.

Available Documentation

A specific page on the Event-B wiki is dedicated to Code Generation Updates.

Planning

Efforts will continue with extending the existing code generation approach, developing new techniques, and building a stable platform. The automatic generation of code for FMUs, from Event-B will be investigated.

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