D32 General Platform Maintenance

Overview

The main goal of the platform corrective and evolutive maintenance is to fix the listed known bugs, and implement some new requested features. As in the previous years of DEPLOY, these bugs and features are reported either by mail or through dedicated SourceForge trackers.

The terse list below gives an overwiew of the noteworthy features added in the main platform during the past year:

• Proof replay on undischarged POs (since release 1.3)

It often happens, while modifying a model, that a set of previously manually discharged POs have slightly changed and need to be discharged again. However, replaying the proof for these POs could most of the time be enough to discharge it. Hence, a command was added to manually try replaying the proofs for a set of undischarged POs. This request comes directly from end users. See .

• Rule Details View (since release 2.0)

When doing an interactive proof, one is guided by the proof tree appearing on the proof tree view. However, it is sometimes needed to get more information about the rules involved in a proof, such as instantiation details, used hypotheses, etc. The Rule Details View displaying such details has been added.

• Refactory plug-in (since release 1.2)

The Refactory plug-in allows users of the Rodin platform to rename modelling elements. With a unique operation, both declaration and occurrences of an element are renamed. Moreover, renaming an element also modifies the corresponding proof, so that renaming does not change the proof status (no loss of proof).

• Mathematical extensions (since release 2.0)

The integration of mathematical extensions required a major rework of the deep internals of the platform (in particular all code related to the manipulation of mathematical formulas). See .

• Documentation

Plug-in developers expressed their need to get a detailed documentation about Rodin extension ability. A dedicated tutorial has been written accordingly, and was the support of a full-day tutorial session given at the Rodin User and Developer Workshop in Düsseldorf this year.

The user manual, user tutorial and other developer documentation on the wiki are continuously, and collaboratively updated and enhanced. Moreover, as soon as a new feature is added to the platform, the corresponding user documentation is created on the Wiki.

See the Release Notes and the SourceForge databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.

Motivations

The evolutive maintenance (resp. corrective maintenance) has its origin in the DEPLOY description of work, and the various requests (resp. bug reports) listed by WP1-4 partners, developers and users. Since the DEPLOY project inception, various streams have been used to request new features or track known bugs:

- dedicated trackers,

- platform user mailing listTODO: Need reference here

- DEPLOY WP9 mailing list.

Maintenance tasks to perform are collected from the aforementioned streams and scheduled during WP9 meetings. These tasks are processed in the same way as the task planned in the description of work.

The following table describes the main tasks (either performed or scheduled) motivating the evolutive maintenance:

Origin	Maintenance Task	Done in 2010	Scheduled in 2011
DoW / WP1-4 partners	Prover efficiency and integrity	x	x
Qualoss assessment TODO: Put Deliverable number, rather	Test reports and test coverage		x
WP1-4 partners	Updating fields of records	x
WP1-4 partners	Team work	x
WP1-4 partners	Edition		x
WP1-4 partners	Increase platform stability		x
WP1-4 partners	Comments everywhere		x
WP1-4 partners	Plug-in incompatibilities		x
WP1-4 partners	Search in goal window		x
WP1-4 partners	Preferences for the automatic tactics		x
WP1-4 partners	Hierarchy / refinement view		x
Plug-in developers	API to extend the Pretty Printer view	x
Plug-in developers	View the error log	x
Plug-in developers	Prover API	x
Plug-in developers	A different update site for unstable plug-ins		x
End Users	64-bit Rodin for Mac	x
End Users	Adding a replay proof command in the Event-B explorer	x
End Users	Having auto-completion in proof control	x
End Users	Displaying instantiated hypotheses	x
End Users	Displaying the inherited elements		x

Choices / Decisions

• Task priority

Listed tasks are being given a priority during WP9 bi-weekly meetings, and then assigned to partners in charge of their processing. A higher priority is given to requests originating from deployment parteners.

• 64-bit release of Rodin for Mac platforms

A major UI bug, due to some incompatibilities between Eclipse 3.5 and Java 1.6 on Mac platforms motivated the migration to the Eclipse 3.6 as basis for the Rodin 2.0 platform. In the meantime, as the 32-bit Java Virtual Machine is no longer supported on Mac platforms, Rodin migrated to Java 1.6, so that the release 2.0 of Rodin became a 64-bit Mac platform only.

The Rodin platforms family is then composed of three executables : 32-bit platforms for Linux and Windows environments and a 64-bit platform for Mac computers.

• Rodin sources

The sources of Rodin are now bundled together with the binary platform. It provides developers with a convenient alternative to the available sources on SourceForge.

• Release notes

The release notes contain information about the released plug-ins and centralise the requirements or existing issues which could not be stated at the main platform release date. Thus, since Rodin 2.0 release, it has been chosen to link the contents of the release notes text file included in Rodin releases, with the contents of the dedicated Wiki page.

Available Documentation

The following pages give useful information about the Rodin platform releases:

• Release notes.
• Bugs.
• Feature requests.

Planning

During the coming year, WP9 partners will favour work on the following topics, which were pointed out at the last plenary meeting by the WP1-WP4 partners and encompass end-user requests (see scheduled tasks in ):

• Platform stability and performances

Currently, users struggle through performance flows in the Rodin platform while editing or proving a model. Solving these flows represents a real challenge for the coming year and will be mandatory for the industrial adoption of the Event-B methodology and Rodin.

• Prover efficiency and integrity

Having all models automatically proved is the ideal to get close to. Thus, enhancing provers is a continuous task that will be performed until the DEPLOY project's end. However, ensuring their correctness and getting more confidence into them, will be a necessary task performed during this coming year.

• Plug-in incompatibilities

The problem occurs when several plug-ins are installed and conflicts exist between them. The cumbersome behaviour often spawned by such incompatibilities leads to user's disappointment, or even to the impossility to use the platform. Particular efforts will be given to identify the sources of incompatibilities among plug-ins and coordinate the assignment and processing of the necessary corrective maintenance tasks.