D32 General Platform Maintenance: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Tommy
imported>Tommy
mNo edit summary
 
(45 intermediate revisions by 4 users not shown)
Line 3: Line 3:


The terse list below gives an overwiew of the noteworthy features added in the main platform during the past year:
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 (releases 1.3 and upper)
* Proof replay on undischarged POs (since release 1.3)
: It often happens, while modifying a model, that a set of previously manually discharged POs are slightly changed and need to be discharged again. However, replaying the proof for those 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 was expressed by [https://sourceforge.net/tracker/?func=detail&aid=2949606&group_id=108850&atid=651672 end users]. See [http://wiki.event-b.org/index.php/Proof_Obligation_Commands].
: 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 (releases 2.0 and upper)
* 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 informations about the rules being involved in a proof, such as instantiation details, used hypotheses, etc. The [http://wiki.event-b.org/index.php/Rodin_Proving_Perspective#Rule_Details_View Rule Details View] displaying such details has been added.
: 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.
* Refactoring plug-in (releases 1.2 and upper)
* 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
* Documentation
: Plug-in developers expressed their need to get a detailed documentation about Rodin extension ability. A dedicated [http://wiki.event-b.org/index.php/Plug-in_Tutorial tutorial][http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation] has been written accordingly, and was the support of a training session given at the [http://www.event-b.org/rodin10.html Rodin User and Developer Workshop] in Düsseldorf this year.
: 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 [http://wiki.event-b.org 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([http://wiki.event-b.org/index.php/Proof_Obligation_Commands] is an example).
: 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 [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Release Notes] and the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation SourceForge] databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
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.


= Motivations =
= Motivations =
The evolutive maintenance (resp. corrective maintenance) has its origin in the DEPLOY project's description of work, and the various requests (resp. bug reports) listed by WP1-4 partners, developers and users. Since the DEPLOY project's birth, various streams can be used to express feature requests or track an encountered bug :
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:
: - [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation dedicated trackers],
: - 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>,
: - DEPLOY mailing lists.
: - 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.
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 performed or scheduled tasks motivating the evolutive maintenance:
The following table describes the main tasks (either performed or scheduled) motivating the evolutive maintenance:
 
{{SimpleHeader}}
{{SimpleHeader}}
|-
|-
! scope=col | Origin || Maintenance Task || Done in 2010 || Scheduled in 2011
! scope=col | Origin || Maintenance Task || Done in 2010 || Scheduled in 2011
|-
| DoW / WP1-4 partners || Prover efficiency and integrity || x || x
|-
| Deliverable D25 || Test reports and test coverage ||  || x
|-  
|-  
| WP1-4 partners|| Updating fields of records || x ||  
| WP1-4 partners|| Updating fields of records || x ||  
Line 35: Line 41:
| WP1-4 partners|| Increase platform stability ||  || x
| WP1-4 partners|| Increase platform stability ||  || x
|-
|-
| WP1-4 partners / DoW || Prover integrity and performances || x || 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|| Comments everywhere ||  || x
|-
|-
| WP1-4 partners|| Plug-in incompatibilities ||  || x
| WP1-4 partners|| Plug-in incompatibilities ||  || x
|-
|-
| WP1-4 partners|| Search in goal window ||  || 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 ||  || 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
|-
|-
| DoW || Qualoss assessment : release policy & test coverage || ||  
| 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 || 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 || 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|| 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|| 64-bit Rodin for Mac || x ||
|-
|-
| End Users|| Adding a replay proof command in the Event-B explorer || 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 || 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 || 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
| End Users || Displaying the inherited elements || || x
Line 66: Line 72:
= Choices / Decisions =
= Choices / Decisions =
* Task priority
* Task priority
: Listed tasks are being given a priority during WP9 bi-weekly meetings, and then assigned to partners in charge of their processing. It has been decided to give a higher priority to WP1-4 partner's requests.
: 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
* 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.
: 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.
: 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
* Rodin sources
: The sources of Rodin releases are now packed with the platform. It has been decided to ship the sources in every platform release. It is, for developers, a convenient alternative to the available sources on SourceForge (See [http://wiki.event-b.org/index.php/Using_Rodin_as_Target_Platform]).
: 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
* 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.
: 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.
Line 77: Line 83:
= Available Documentation =
= Available Documentation =
The following pages give useful information about the Rodin platform releases:
The following pages give useful information about the Rodin platform releases:
* Release notes.
* Release notes<ref>http://wiki.event-b.org/index.php/Rodin_Platform_Releases</ref>.
: See [http://wiki.event-b.org/index.php/Rodin_Platform_Releases Rodin Platform Releases].
* Bugs<ref>http://sourceforge.net/tracker/?atid=651669&group_id=108850</ref>.
* Bugs.
* Feature requests<ref>http://sourceforge.net/tracker/?group_id=108850&atid=651672</ref>.
: See [http://sourceforge.net/tracker/?atid=651669&group_id=108850].
* Feature requests.
: See [http://sourceforge.net/tracker/?group_id=108850&atid=651672].


= Planning =
= Planning =
During the coming year, special efforts will be made on the following topics, which where pointed out at the last plenary meeting by the WP1-WP4 and encompass end-user requests:
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
* Platform stability and performances
: Currently, users struggle through performance flows in the Rodin platform while editing or proving a model. Solving these issues represents a real challenge for the coming year and will be mandatory for the industrial adoption of Rodin and Event-B.
: 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 integrity
* Prover efficiency and integrity
: Reaching a state where POs are hundred percent automatically proved is the wager that Rodin developers aim. Getting close to this ideal will increase the satisfaction of industrial users and decrease costs. Enhancing prover facilities are as well, one significant help given to the person in charge of the proving. Enhancing prover is then a continuous task that will be performed until the DEPLOY project's end. However, such automatic or manual pieces of program are main points of integrity concerns. Ensuring their correctness and getting more confidence into them, will thus be a task conducted during the coming year.
: 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
* 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 lead to identify the sources of incompatibilities among plug-ins and coordinate the assignment and processing of the necessary corrective maintenance tasks.
: 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]]
[[Category:D32 Deliverable]]

Latest revision as of 16:28, 14 November 2011

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[1]. See [2].
  • 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[3] displaying such details has been added.
  • Refactory plug-in (since release 1.2)
The Refactory[4] 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 [5].
  • Documentation
Plug-in developers expressed their need to get a detailed documentation about Rodin extension ability. A dedicated tutorial[6][7] has been written accordingly, and was the support of a full-day tutorial session given at the Rodin User and Developer Workshop[8] in Düsseldorf this year.
The user manual, user tutorial and other developer documentation on the wiki[9] 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[7] and the SourceForge[7] 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[10][11],
- platform mailing lists [12]
- 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
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 [13] x
WP1-4 partners Plug-in incompatibilities x
WP1-4 partners Search in goal window [14] x
WP1-4 partners Preferences for the automatic tactics [15] x
WP1-4 partners Hierarchy / refinement view[16] x x
Plug-in developers API to extend the Pretty Printer view [17] x
Plug-in developers View the error log [18] 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 [19] x
End Users Having auto-completion in proof control [20] x
End Users Displaying instantiated hypotheses [21] 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[22] 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:

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 [26]) 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

  1. https://sourceforge.net/tracker/?func=detail&aid=2949606&group_id=108850&atid=651672
  2. http://wiki.event-b.org/index.php/Proof_Obligation_Commands
  3. http://wiki.event-b.org/index.php/Rodin_Proving_Perspective#Rule_Details_View
  4. http://wiki.event-b.org/index.php/Refactoring_Framework
  5. http://wiki.event-b.org/index.php/D32_Mathematical_Extensions
  6. http://wiki.event-b.org/index.php/Plug-in_Tutorial
  7. 7.0 7.1 7.2 http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Available_Documentation
  8. http://www.event-b.org/rodin10.html
  9. http://wiki.event-b.org
  10. http://sourceforge.net/tracker/?group_id=108850&atid=651669
  11. http://sourceforge.net/tracker/?group_id=108850&atid=651672
  12. http://sourceforge.net/mail/?group_id=108850
  13. https://sourceforge.net/tracker/index.php?func=detail&aid=3007797&group_id=108850&atid=651672
  14. https://sourceforge.net/tracker/?func=detail&atid=651672&aid=3092835&group_id=108850
  15. http://sourceforge.net/tracker/index.php?func=detail&aid=1581775&group_id=108850&atid=651672
  16. http://wiki.event-b.org/index.php/Project_Diagram
  17. http://sourceforge.net/tracker/?func=detail&aid=2926238&group_id=108850&atid=651672
  18. http://sourceforge.net/tracker/?func=detail&aid=2990974&group_id=108850&atid=651672
  19. http://sourceforge.net/tracker/?func=detail&aid=2949606&group_id=108850&atid=651672
  20. http://sourceforge.net/tracker/?func=detail&aid=2979367&group_id=108850&atid=651672
  21. http://sourceforge.net/tracker/?func=detail&aid=3008636&group_id=108850&atid=651672
  22. http://wiki.event-b.org/index.php/Using_Rodin_as_Target_Platform
  23. http://wiki.event-b.org/index.php/Rodin_Platform_Releases
  24. http://sourceforge.net/tracker/?atid=651669&group_id=108850
  25. http://sourceforge.net/tracker/?group_id=108850&atid=651672
  26. http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Motivations