ADVANCE D3.2 General Platform Maintenance

Core Rodin platform

Overview

The Rodin platform versions concerned by this deliverable are:

• 2.4 (released on 31.01.2012),
• 2.5 (released on 02.05.2012),
• 2.6 (released on 31.07.2012).

The core Rodin platform maintenance task focused on fixing the identified bugs and rectifying usability issues. During DEPLOY, many features and contributions were added to the toolset as users wishes and requests were collected along. At the same time, the Event-B models and proof got bigger and bigger, in the same way as the experience of the users involved constantly increased ergo the size of the systems they modelled. Scalability issues occured at some point when feature addition was favoured to design refactorings. As the DEPLOY project was nearing its end, it appeared mandatory for the developpment team, to address the specific bugs and issues reported by the DEPLOY partners and related to scalability or usability, and wished resolved by the end of the project. The various tasks to be performed were scheduled, prioritized and regularly updated during bi-weekly teleconferences.

The following paragraphs will give an overview of the the work that has been performed concerning maintenance on the existing platform components (i.e. core platform and plug-ins). Release Notes and the SourceForge trackers (bugs and feature requests) are available for more details about the previous and upcoming releases of the Rodin platform.

Motivations / Decisions

Provide 64-bit versions of the Rodin platform on Linux and Windows systems
End users asked the Rodin team to provide 32-bit and 64-bit versions of the Rodin platform for Linux and Windows operating systems. Before Rodin 2.4, the only 64-bit version of Rodin was available on Mac platforms as 32-bit Mac (early 2006) platforms are no longer maintained by Apple. The motivation that would push forward 64-bit architectures is the possibility to increase the available java heap size which is, for example, extensively used during the automated proof. After a phase of testing on Rodin 2.4 and despite the drawbacks of assembling and maintaining five platforms instead of three, Linux and Windows 64-bit as well as 32-bit platforms are now made available.

The Rodin Editor and the Theory plug-in in the Rodin core platform
According to their role in the Rodin toolset, and their stabilization, the Rodin Editor, and later the Theory plug-in were reintegrated into the core platform. The Rodin Editor was released in the core platform since Rodin 2.4, and the Theory plug-in since Rodin 2.6.

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.

Planning

The platforms 2.7 and 3.0 have been scheduled, and their contents have been set. The platform 2.7 is intended to be released by the end of October 2012, and will be a corrective release. Indeed, the coming release 3.0, is an evolutive release that will be prepared since the release 2.6 but would require too much time to be scheduled in place of the release 2.7. Here is a non exaustive list of the main improvements and refactorings that will be part of the Rodin 3.0 release:

• Binders will be allowed in extensions.
• The platform will be based on Eclipse 4.
• The AST will be made stronger.
• The sequent prover will be enhanced.
• Parent-child element relationship extension points will be moved from the UI plug-in to the EventB core plug-in.
• The Event-B keyboard plug-in will be refactored to separate the UI code from the ASCI/Math translation mechanism.
• The statistics view will be refactored to handle other kinds of "ElementNode"s (than just Context and Machine Root).

UML-B Improvements

Overview

The UML-B plug-in and associated frameworks are developed and maintained by Dr Colin Snook at the University of Southampton. Significant contributions (to the latest version) have been made by Vitaly Savicks (State-machines) and Gintautas Sulskus (Class Diagrams). The UML-B plugin provides UML-like diagrammatic modelling as an extension to Event-B and the Rodin platform. UML-B is an established plug-in which will be developed and improved to support the aims of the ADVANCE project. UML-B was redeveloped during the DEPLOY project to provide closer integration with Event-B. A state-machine diagram editor is already released in this integrated version and a class diagram editor is now being developed as a prototype. Other improvements will include new diagrammatic notations which are directly related to the aims of ADVANCE, such as component diagrams, as well as more general improvements, such as usability, and any features required by the projects industrial partners.

Motivations / Decisions

The implementation of the UML-B tool is structured to provide re-usable features as much as possible. To achieve this, wherever possible, generic frameworks are developed and the implementation of specific diagram tools is minimised by utilising these frameworks. The following frameworks are now in use by UML-B and available as a basis for future diagrammatic modelling notations.

• The Event-B EMF framework provides an EMF basis for Event-B models (developed during the DEPLOY project).
  • Provides an EMF representation of Event-B models with persistance into the Rodin database.
• The Event-B EMF Support for Modelling Extensions framework provides support for extending Event-B with new modelling features (initially developed during the DEPLOY project and now being extended in the ADVANCE project).
  • Provides Navigator support for EMF-only model elements
  • Provides a persistence mechanism for model extensions that are not needed to be processed by Rodin.
  • A Generic Refiner for modelling extensions has recently been added.
• The Event-B GMF Diagrams Generic Support framework provides support for developing new diagram notations (started in the DEPLOY project but mostly developed during the ADVANCE project).
  • Provides Generic support for diagrammatic aspects of modelling extensions
  • A generic Validation and Event-B generation service has recently been added

A new release of the State-machine diagram editor has been made. This release corrected some problems and improved use of the generic framework features.

Work is in progress on a new version of the UML-B Class Diagram editor. This takes the same approach as the State-machines editor in that the models are contained within Machines (and, in this case, also Contexts) and that diagrammatic model features link to and enhance existing Event-B elements rather than generate everything. The Class diagram editor is currently a prototype and has not been released.

Available Documentation

[reference Fontainebleau Rodin workshop paper on Generic frameworks]

Wiki pages for developers using the Generic extensions and Diagrams frameworks.

http://wiki.event-b.org/index.php/EMF_framework_for_Event-B

http://wiki.event-b.org/index.php/Generic_Event-B_EMF_extensions (Under Construction)

[reference Dusseldorf Rodin workshop paper on Event-B Statemachines]

Wiki pages for users of UML-B

http://wiki.event-b.org/index.php/UML-B

Planning

The following work is planned:

• Re-base the Event-B EMF framework on the EMF model of the Rodin database (which is now available as a result of the development of a new Rodin editor to replace the form based editor).
• Re-write the Event-B generator of the State-machine diagram editor so that it uses the generic generator from the Event-B GMF Support for Generic Diagrams framework. This will improve performance.
• Improve the State-machine diagram animation interface so that it supports animation of multiple diagrams.
• Complete the development of the new version of the UML-B Class Diagram editor.
• Develop Animation interface for the Class diagram editor.
• Develop a Component diagram editor and associated simulation tools.

Code generation

Overview

We released the latest Code generation Feature on 30th May 2012. New features include: Code generation from state-machine diagrams.

Motivations / Decisions

State machines are frequently used to describe the behaviour of embedded systems. It is a relatively new feature in Event-B, and we augment the tool with the ability to generate code from state-machine diagrams; in version 0.2.3 of the code generation feature plug-in. Implementation code is generated from the diagram itself, and no additional mark-up of the model is required; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-machines are created, using the existing state-machine plug-in, subject to the limitations described below.

Limitations

The current code generation tool is restricted to generating code for a single Event-B machine, which may contain one or more state-machines. We have yet to explore the decomposition/composition of machines containing state-machines. In principal we should be able to apply decomposition techniques to decompose the single Event-B machine with state-machines into a number of machines, with the state-machines, or the elements of state-machines, distributed between them. Another limitation is that we do not handle nested state-machines, although this should be feasible. Only the state-machines of tasking/environ machines generate code. State-machines of shared machines do not generate code. This should be explored further during research into decomposition.

The translation of the diagrammatic elements to code has been hard-coded in the code generation plug-in. We have introduced new types to the translator's common language model (IL1). We add case-statements, and a container for them (analogous to switch) since these are commonly used to implement state-machines. The code generator navigates through each state of a state-machine, generating an internal representation of the state-machine, which is used to create the IL1 model. The IL1 model is then used to generate code for the various target languages that may have been implemented. We have also updated the IL1-to-target code generators, to generate case/switch statements in Ada, C and Java. Each state-machine has an Enumerated type whose elements take the names of the states. A state variable is created in the target that keeps track of the current state, and has the type of the enumeration.

Available Documentation

Code Generation Updates

Planning

Investigate the use of new techniques, and techniques used in the existing code generator, for use in the simulation of cyber-physical systems.

ProR

Overview

The Rodin/ProR 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 following paragraphs will give an overview of the the work that has been performed concerning maintenance on the Rodin/ProR plugin.

Motivations / Decisions

The motivation of the Rodin/ProR integration plugin was to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. Especially, the traceability within a system description is a challenging problem of requirements engineering. In particular, formal models of the system are often based on informal requirements, but creating and maintaining the traceability between the two can be challenging. In , we presented an incremental approach for producing a system description from an initial set of requirements. The foundation of the approach is a classification of requirements into artefacts W (domain properties), R (requirements) and S (specification). In addition, the approach uses designated phenomena as the vocabulary employed by the artefacts. The central idea is that adequacy of the system description must be justified, meaning that W ∧ S ⇒ R. The approach establishes a traceability, and the resulting system description may consist of formal and informal artefacts. We created tool support for this approach by integrating Rodin and ProR. We designed it with the goal to support the approach described in , and to ease the integration of natural language requirements and Event-B.

Available Documentation

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

• Tutorial for the Rodin/ProR integration can be found here: .
• The User Guide containing an additional Tutorial for ProR can be found here: .

Planning

There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, lists a number of properties of a correct system description. While the presence of these properties does not guarantee correctness, their absence indicates a problem. Reporting on the state of these properties would be valuable.

Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.

Camille

Overview

The Camille plug-in provides a textual editor for Rodin. Though such a text editor is preffered by many users, Camille currently has the drawback of not supporting extensibility. It only supports the core Event-B language and plug-in-specific additions are simply ignored. Such extensions can not be edited through Camille. Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions. This has become a major issue during the last years, since many plug-ins have been developed in the meantime that are widely used by many users.

This issue is currently being adressed by Ingo Weigelt at the University of Duesseldorf.

Motivations / Decisions

A new version of Camille will be implemented during the ADVANCE project to enable users to edit extended Event-B models solely though a text editor. To plan the new version, the problem and a number of possible solutions have been analysed in . The results of this work have been dicussed in the Rodin community and one of the proposed solution (a blockparser) has been selected to be implemented during the next months. The dedicated solution promises to provide Camille extensibility with minimal extra workload required from plug-in developers while still being very flexible regarding future, yet unknown, requirements.

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

The new Camille version will be implemented at the University of Duesseldorf during 2012. The final version is expected in January or February 2013.