imported>Tommy |
imported>Tommy |
| Line 1: |
Line 1: |
| − | = Overview =
| + | The DEPLOY's D32 deliverable is composed of: |
| − | 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 Rodin core platform and plug-ins (i.e. the DEPLOY tools). |
| | + | * This document. |
| | + | The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]). |
| | | | |
| − | The terse list below gives an overwiew of the noteworthy features added in the main platform during the past year:
| + | This document gives a description of the work that was carried on during the second year of the DEPLOY project (Feb 2009-Jan 2010), in the course of the WP9 ''Tooling research and development'' work package, and brings new perspectives for the coming 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<ref>https://sourceforge.net/tracker/?func=detail&aid=2949606&group_id=108850&atid=651672</ref>. See <ref>http://wiki.event-b.org/index.php/Proof_Obligation_Commands</ref>.
| |
| − | * 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<ref>http://wiki.event-b.org/index.php/Rodin_Proving_Perspective#Rule_Details_View</ref> displaying such details has been added.
| |
| − | * Refactory plug-in (since release 1.2)
| |
| − | : The Refactory<ref>http://wiki.event-b.org/index.php/Refactoring_Framework</ref> 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 <ref>http://wiki.event-b.org/index.php/D32_Mathematical_Extensions</ref>.
| |
| − | * Documentation
| |
| − | : Plug-in developers expressed their need to get a detailed documentation about Rodin extension ability. A dedicated tutorial<ref>http://wiki.event-b.org/index.php/Plug-in_Tutorial </ref><ref name="documentation">http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Available_Documentation</ref> has been written accordingly, and was the support of a full-day tutorial session given at the Rodin User and Developer Workshop<ref>http://www.event-b.org/rodin10.html </ref> in Düsseldorf this year.
| |
| − | : The user manual, user tutorial and other developer documentation on the wiki<ref>http://wiki.event-b.org</ref> 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<ref name="documentation">http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Available_Documentation</ref> and the SourceForge<ref name=documentation>http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Available_Documentation</ref> databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
| + | In particular, the WP9 partners have strovin to meet the following objectives: |
| | + | * Improved scalability of the Rodin platform to support industrial deployments, through GUI enhancements (smart completion, renaming, text editing, etc), decomposition support and design-pattern management. |
| | + | * Prover integrity and performance, to enhance the confidence in provers and to enlarge their proving capabilities. To this aim, the existing provers have been improved and a new rule-based prover plug-in has been implemented. |
| | + | * Model animation and testing, to validate Event-B models. More precisely, the ProB or AnimB plug-ins allow a domain expert to detect errors in a model and ensure the presence of desired functionalities. Moreover, it is very important for many industrial applications to be able to completely hide the underlying formal specification. |
| | + | * Model checking (ProB), to enable users to find sequences of events that prevent safety properties or proof obligations to be fulfilled. |
| | + | * UML integration. UML-B provides a diagrammatic, formal modelling notation based on UML. |
| | + | * Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An initial definition of language support for code generation has been put forward. |
| | | | |
| − | = Motivations =
| + | This document covers the following items: general platform maintenance, UML-B improvements, ProB improvements, text editor plug-in, decomposition plug-in, initial definition of language support for code generation, improvements to existing provers, rule-based prover, pattern plug-in, flow plug-in and modularisation plug-in. |
| − | 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<ref name="bugTracker">http://sourceforge.net/tracker/?group_id=108850&atid=651669</ref><ref name="frTracker">http://sourceforge.net/tracker/?group_id=108850&atid=651672</ref>,
| |
| − | : - platform mailing lists <ref>http://sourceforge.net/mail/?group_id=108850</ref>
| |
| − | : - 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:
| + | For each of these newly implemented features or improvements, the document is structured as follows: |
| − | {{SimpleHeader}}
| + | * Overview. The involved partners are identified and an overview of the contribution is given. |
| − | |-
| + | * Motivations. The motivations for each tool extension and improvement are expressed. |
| − | ! scope=col | Origin || Maintenance Task || Done in 2010 || Scheduled in 2011
| + | * Choices / decisions. The decisions (e.g. design decisions) are justified. |
| − | |-
| + | * Available documentation. Some pointers to the Event-B wiki or related publications are listed. |
| − | | DoW / WP1-4 partners || Prover efficiency and integrity || x || x
| + | * Planning. A timeline and the current status (as of 29 Jan 2010) is given. |
| − | |-
| |
| − | | Deliverable D25 || 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 <ref>https://sourceforge.net/tracker/index.php?func=detail&aid=3007797&group_id=108850&atid=651672</ref> || || x
| |
| − | |-
| |
| − | | WP1-4 partners|| Plug-in incompatibilities || || x
| |
| − | |-
| |
| − | | WP1-4 partners|| Search in goal window <ref>https://sourceforge.net/tracker/?func=detail&atid=651672&aid=3092835&group_id=108850</ref> || || x
| |
| − | |-
| |
| − | | WP1-4 partners|| Preferences for the automatic tactics <ref>http://sourceforge.net/tracker/index.php?func=detail&aid=1581775&group_id=108850&atid=651672</ref> || || x
| |
| − | |-
| |
| − | | WP1-4 partners|| Hierarchy / refinement view<ref>http://wiki.event-b.org/index.php/Project_Diagram</ref> || x || x
| |
| − | |-
| |
| − | | Plug-in developers|| API to extend the Pretty Printer view <ref>http://sourceforge.net/tracker/?func=detail&aid=2926238&group_id=108850&atid=651672</ref> || x ||
| |
| − | |-
| |
| − | | Plug-in developers|| View the error log <ref>http://sourceforge.net/tracker/?func=detail&aid=2990974&group_id=108850&atid=651672</ref> || 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 <ref>http://sourceforge.net/tracker/?func=detail&aid=2949606&group_id=108850&atid=651672</ref> || x ||
| |
| − | |-
| |
| − | | End Users|| Having auto-completion in proof control <ref>http://sourceforge.net/tracker/?func=detail&aid=2979367&group_id=108850&atid=651672</ref> || x ||
| |
| − | |-
| |
| − | | End Users|| Displaying instantiated hypotheses <ref>http://sourceforge.net/tracker/?func=detail&aid=3008636&group_id=108850&atid=651672</ref> || x ||
| |
| − | |-
| |
| − | | End Users || Displaying the inherited elements || || x
| |
| − | |}
| |
| | | | |
| − | = Choices / Decisions =
| + | [[Category:D23 Deliverable]] |
| − | * 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<ref>http://wiki.event-b.org/index.php/Using_Rodin_as_Target_Platform</ref> 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<ref>http://wiki.event-b.org/index.php/Rodin_Platform_Releases</ref>.
| |
| − | * Bugs<ref>http://sourceforge.net/tracker/?atid=651669&group_id=108850</ref>.
| |
| − | * Feature requests<ref>http://sourceforge.net/tracker/?group_id=108850&atid=651672</ref>.
| |
| − | | |
| − | = Planning =
| |
| − | For the coming year, the following topics pointed out at the last plenary meeting by the WP1-WP4 partners and encompassing end-user requests (see scheduled tasks in <ref>http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Motivations</ref>) will be favoured by the WP9 partners:
| |
| − | * Platform stability and performances
| |
| − | : Currently, users struggle with editing or proving a model due to performance issues in the Rodin platform. Solving these issues represents a real challenge for the coming year and is mandatory for the industrial adoption of the Event-B methodology and Rodin platform.
| |
| − | * Prover efficiency and integrity
| |
| − | : Having all models automatically proved is the ideal goal. Thus, enhancing provers is a continuous task to be performed until the end of the DEPLOY project. Ensuring provers correctness and improving confidence in them is another important goal that will be pursued in the coming year.
| |
| − | * Plug-in incompatibilities
| |
| − | : When several plug-ins are installed, conflicts between them can arise. The cumbersome behaviour spawned by such incompatibilities leads to users' disappointment or can render the platform unusable. Special efforts will be made to identify the source of incompatibilities among plug-ins. Moreover, necessary corrective maintenance tasks and assignments will be coordinated and executed.
| |
| − | | |
| − | == References ==
| |
| − | <references/>
| |
| − | | |
| − | [[Category:D32 Deliverable]] | |
The DEPLOY's D32 deliverable is composed of:
- The Rodin core platform and plug-ins (i.e. the DEPLOY tools).
- This document.
The Rodin platform can be downloaded from SourceForge site ([1]). The tool documentation is provided within the Event-B wiki ([2]).
This document gives a description of the work that was carried on during the second year of the DEPLOY project (Feb 2009-Jan 2010), in the course of the WP9 Tooling research and development work package, and brings new perspectives for the coming year.
In particular, the WP9 partners have strovin to meet the following objectives:
- Improved scalability of the Rodin platform to support industrial deployments, through GUI enhancements (smart completion, renaming, text editing, etc), decomposition support and design-pattern management.
- Prover integrity and performance, to enhance the confidence in provers and to enlarge their proving capabilities. To this aim, the existing provers have been improved and a new rule-based prover plug-in has been implemented.
- Model animation and testing, to validate Event-B models. More precisely, the ProB or AnimB plug-ins allow a domain expert to detect errors in a model and ensure the presence of desired functionalities. Moreover, it is very important for many industrial applications to be able to completely hide the underlying formal specification.
- Model checking (ProB), to enable users to find sequences of events that prevent safety properties or proof obligations to be fulfilled.
- UML integration. UML-B provides a diagrammatic, formal modelling notation based on UML.
- Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An initial definition of language support for code generation has been put forward.
This document covers the following items: general platform maintenance, UML-B improvements, ProB improvements, text editor plug-in, decomposition plug-in, initial definition of language support for code generation, improvements to existing provers, rule-based prover, pattern plug-in, flow plug-in and modularisation plug-in.
For each of these newly implemented features or improvements, the document is structured as follows:
- Overview. The involved partners are identified and an overview of the contribution is given.
- Motivations. The motivations for each tool extension and improvement are expressed.
- Choices / decisions. The decisions (e.g. design decisions) are justified.
- Available documentation. Some pointers to the Event-B wiki or related publications are listed.
- Planning. A timeline and the current status (as of 29 Jan 2010) is given.
