Difference between pages "D32 Teamwork" and "D45 General Platform Maintenance"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Renato
 
imported>Tommy
 
Line 1: Line 1:
−
=== Overview ===
+
= Overview =
−
Teamwork consists of
+
The Rodin platform versions concerned by this deliverable are:
−
* SVN enabling teamwork plug-in
+
* 2.1(08.02.2011),
−
* Decomposition methods
+
* 2.2(01.06.2011),
 +
* 2.2.2(01.08.2011),
 +
* 2.3(04.10.2011),
 +
* 2.4(31.01.2011),
 +
* 2.5(30.04.2011).
 +
This year, the maintenance carried on fixing identified bugs, although an emphasis has been put on correcting usability issues. Indeed, during the meeting in Nice, the WP9 members agreed to refocus on the needed tasks to address some specific bugs and issues reported by DEPLOY partners, and wished resolved by the end of DEPLOY. Thus, no new features were implemented but those appearing in the description of work. The tasks to be performed by the WP9 members were then scheduled, prioritized and regularly updated during the WP9 bi-weekly meetings. The updates allowed to capture and integrate rapidly some minor changes to enhance the usability of the platform which were required by the DEPLOY partners. 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).
  
 +
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/D45_General_Platform_Maintenance#Available_Documentation</ref> databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
  
−
* Team-working Plug-in is a new feature developed by University of Southampton in request to industrial partners who required support of Rodin project management and team development using Subversion system. Having this support would bring the benefit of centralised model storage and versioning, as well as parallel development. Despite a few functional limitations, derived by specific nature of the Rodin projects, the implemented plug-in gives support for Subversion-based project sharing and collaborative development.
+
* General platform maintenance (Thomas Muller)
 +
The maintenance done to overcome Rodin scalability weaknesses and enhance the proving experience will be detailed in a separate chapter. However, some features initially planned and some other which were later added and prioritized are worth to mention:
 +
:*Possibility to highlight patterns in the ProverUI,
 +
:*A better output providing warning and errors in case of wrong or missing building configurations,
 +
:*The switch to Eclipse 3.7
 +
:*A Handbook to complete and enhance the existing documentation.
 +
These items will be detailed hereafter in this chapter.
  
−
* Decomposition plug-in was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: ''shared event'' (studied initially by Michael Butler) and ''shared variable'' (studied initially by Jean-Raymond Abrial). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.
+
* {{TODO}} An overview of the contribution about Mathematical extensions / Theory Plug-in (Issam Maamria)
  
−
=== Motivations ===
+
* {{TODO}} An overview of the contribution about Plug-in Incompatibilities (All partners)
−
Main reasons for implementing teamwork are:
 
−
* SVN Teamwork
 
−
: The reason to support compatibility of Rodin projects with Subversion was to allow Rodin users to share their projects and work on them together, as well as have the benefits of versioning and revision control, provided by the SVN system. It was difficult to work on models in parallel and manage changes made by different parties, especially for big and complex models. Other users expressed a concern on safety aspect of collaborative development, thus pointing out the benefits of centralised repository storage of the models under development on SVN.
 
  
−
* Decomposition
+
* {{TODO}} An overview of the contribution about Modularisation (Alexei Illiasov)
−
: Difficulties in managing complex models (in particular for a large number of proof obligations) fed the idea of decomposing a model in a way that the resulting sub-models could be developed by different individuals. The decomposition process should be seen as a refinement step where the original properties and respective proof obligations should remain valid. With shared event and shared variable decomposition, these requirements are preserved, with the advantage of simplifying the overall development by dealing with sub-parts of the model at once in each sub-model.
 
  
−
=== Choices / Decisions ===
+
* {{TODO}} An overview of the contribution about Decomposition (Renato Silva)
−
* SVN Teamwork
 
−
: The desired objective of a plug-in that would bring support for Subversion in Rodin was to make a Rodin project compatible with standard SVN interface. Due to nature of the Rodin resource management, in particular the use of Rodin database and non-XMI serialisation, it turned out a hard task. A solution to this difficulty was to provide an alternative serialisation method, that would be compatible with Subversion interface. XMI serialisation has been chosen in the final plug-in, which together with Event-B EMF framework provides a shareable copy of the resources of a Rodin project and takes care of synchronisation between two.
 
  
−
=== Available Documentation ===
+
* {{TODO}} An overview of the contribution about Team-based Development (Colin Snook, Vitaly Savicks)
−
* SVN Team-based development documentation<ref>http://wiki.event-b.org/index.php/Team-based_development</ref>
 
  
−
=== Planning ===
+
* {{TODO}} An overview of the contribution about UML-B (Colin Snook, Vitaly Savicks)  
−
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
 
  
−
=References=
+
* {{TODO}} An overview of the contribution about ProR (Michael Jastram)
 +
 
 +
= Motivations =
 +
The tasks to solve the issues faced by the DEPLOY partners have been listed and being assigned to groups according to their priority. A high priority means a high need in the outcome of a given task. The group 1 has the highest priority, the group 2 has an intermediate priority, and the group 3 has the lowest priority. The group 4 concerns topics that could not be ressourced during the lifetime of DEPLOY.The prover integrity item although not being directly covered, has been partially addressed thanks to Isabelle and SMT integration. Unfortunately, the originally planned export of full proofs and integrity check is beyond the scope of DEPLOY.
 +
 
 +
{{SimpleHeader}}
 +
|-
 +
! scope=col | Group 1 (highest priority) || Responsible
 +
|-
 +
|Performance <br /> - Core (large models, etc.) <br /> - GUI (incl. prover UI, edition, etc.) || SYSTEREL
 +
|-
 +
|Prover Performances <br /> - New rewriting rules / inference rules <br /> - Automatic tactics (preferences, timeout, etc.) || SYSTEREL
 +
|-
 +
|ProB Disprover (incl. counter examples to DLF POs) || Düsseldorf
 +
|-
 +
|Stability (crash, corruption, etc.)  || SYSTEREL
 +
|-
 +
|Editors || SYSTEREL/Düsseldorf
 +
|-
 +
|}
 +
{{SimpleHeader}}
 +
|-
 +
! scope=col | Group 2 || Responsible
 +
|-
 +
| Prover Performances <br /> - SMT provers integration <br /> - connection with Isabelle  <br /> - Mathematical extensions <br /> - ProB || <br />SYSTEREL <br /> ETH Zürich <br /> Southampton/SYSTEREL <br /> Düsseldorf
 +
|-
 +
|Scalability <br /> - Decomposition <br /> - Modularisation plug-in <br /> - Team-based development || <br /> Southampton <br /> Newcastle <br /> Southampton
 +
|-
 +
|Plug-in incompatibilities || Newcastle
 +
|-
 +
|Model-based testing || Pitesti/Düsseldorf
 +
|-
 +
|ProR || Düsseldorf
 +
|}
 +
{{SimpleHeader}}
 +
|-
 +
! scope=col | Group 3 || Responsible
 +
|-
 +
|Scalability <br /> - Generic instantiation <br /> - UML-B maintenance <br /> || <br /> Southampton <br /> ETH Zürich/Southampton
 +
|-
 +
|Code Generation || Southampton
 +
|}
 +
{{SimpleHeader}}
 +
|-
 +
! scope=col | Group 4
 +
|-
 +
|Prover Integrity
 +
|-
 +
|Integrity of Code Generation
 +
|}
 +
== Platform maintenance ==
 +
The platform maintenance, as it can be deduced from the above tables in section [[#Motivations | Motivations]], mainly concerned stability and performance improvement. These topics will be discussed and detailed in a separate chapter about scalability improvements.<br>
 +
However, other prioritary improvements were made on the platform. These improvements or came from DEPLOY partners specific needs, or were corresponding to previously identified needs (listed in D32 - Model Construction tools & Analysis III Deliverable).
 +
Hence we review below the motivations of some noteworthy implemented features:
 +
* A Possibility to highlight patterns in the ProverUI.
 +
This feature came from a request of DEPLOY partners<ref name="searchInPUI">https://sourceforge.net/tracker/?func=detail&atid=651672&aid=3092835&group_id=108850</ref>, often facing the need to find particular patterns such as expressions in long predicates (e.g. long goals). Since Rodin 2.2, and its new ProvingUI interface, a nice feature was added, allowing to search and highlight a string pattern into the whole ProvingUI views and editors. This function as also been enabled on direct selection of text in this UI.
 +
* A better output providing warning and errors in case of wrong or missing building configurations.
 +
This issue, often seen as a bug or a plug-in incompatibility, raises when a user imoprts and tries to use a model on a platform with some missing plug-ins needed on build. The user often use to think his models corrupted although Rodin just being not able to build them, and hiding this information to the user. This is why, since Rodin 2.3, an output in such case has been provided taking the form of warnings or errors that any user can review. This is a partial answer to Rodin plug-in incompatibilities issue.
 +
* The switch to Eclipse 3.7.
 +
Due to the major improvements made every year in every Eclipse releases and the continuously growing number of contributing projects which are for some of them used as basis for Rodin plug-ins, the Rodin platform follows the evolution and is adapted every year quickly to the latest Eclipse version available. This year, Rodin 2.3 originated the switch from Eclipse 3.6 to Eclipse 3.7.
 +
* A Handbook to complete and enhance the existing documentation.
 +
At the DEPLOY Plenary Meeting in Zürich in 2010, it has been stated that the current documentation, in its state at that time, would not support, a engineer starting using the tools without significant support of an expert. Losts of efforts to improve the documentation were performed and coordinated by Düsseldorf, and took form of the Rodin Handbook. The Rodin handbook has the aim to minimize the access to an expert, by providing the necessary assistance to an engineer in the need to be productive using Event-B and the Rodin toolset. The contents of the handbook were originated by the contents of the Event-B wiki, although these contents have now all been migrated to the Rodin handbook.
 +
 
 +
== Mathematical extensions / Theory Plug-in ==
 +
{{TODO}} ''To be completed by Issam Maamria''
 +
== Plug-in Incompatibilities ==
 +
{{TODO}} ''To be completed by all partners''
 +
== Modularisation ==
 +
{{TODO}} ''To be completed by Alexei Illiasov''
 +
== Decomposition ==
 +
{{TODO}} ''To be completed by Renato Silva'' 
 +
== Team-based Development ==
 +
{{TODO}} ''To be completed by Colin Snook, Vitaly Savicks''
 +
== UML-B ==
 +
{{TODO}} ''To be completed by Colin Snook, Vitaly Savicks''
 +
== ProR ==
 +
{{TODO}} ''To be completed by Michael Jastram''
 +
 
 +
= Choices / Decisions =
 +
== Platform maintenance ==
 +
* Revisited task priority
 +
This year, the process to give priority to maintenance tasks was revisited according the the refocus mentionned above. Thus not only the requests coming from DEPLOY partners were given high priorities, but they were prioritized against the already planned tasks coming from both DEPLOY partners and the Description of Work. This prioritization was performed or internally at each WP9 member site, if the task is short (i.e. less than one man-week), or during the WP9 bi-weekly telephone conferences otherwise. 
 +
* A way to tackle plug-in incompatibilities
 +
 
 +
* keeop 32-bit versions of Rodin on linux and windows systems
 +
 
 +
== Mathematical extensions / Theory Plug-in ==
 +
{{TODO}} ''To be completed by Issam Maamria''
 +
== Plug-in Incompatibilities ==
 +
{{TODO}} ''To be completed by all partners''
 +
== Modularisation ==
 +
{{TODO}} ''To be completed by Alexei Illiasov''
 +
== Decomposition ==
 +
{{TODO}} ''To be completed by Renato Silva'' 
 +
== Team-based Development ==
 +
{{TODO}} ''To be completed by Colin Snook, Vitaly Savicks''
 +
== UML-B ==
 +
{{TODO}} ''To be completed by Colin Snook, Vitaly Savicks''
 +
== ProR ==
 +
{{TODO}} ''To be completed by Michael Jastram''
 +
 
 +
= Available Documentation =
 +
* Core platform:
 +
: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>https://sourceforge.net/tracker/?group_id=108850&atid=651669</ref>.
 +
:* Feature requests<ref>https://sourceforge.net/tracker/?group_id=108850&atid=651672</ref>.
 +
 
 +
*{{TODO}}  Links for Mathematical extensions / Theory Plug-in
 +
*{{TODO}}  Links for Plug-in Incompatibilities
 +
*{{TODO}}  Links for Modularisation
 +
*{{TODO}}  Links for Decomposition
 +
*{{TODO}}  Links for Team-based Development
 +
*{{TODO}}  Links for UML-B
 +
*{{TODO}}  Links for ProR
 +
 
 +
= Status =
 +
== Platform maintenance ==
 +
By the end of the project, there are :
 +
* xx bugs reported and open. All with a priority lower or equal to 5.
 +
* xx feature requests expressed and still open.
 +
 
 +
== Mathematical extensions / Theory Plug-in ==
 +
{{TODO}} ''To be completed by Issam Maamria''
 +
== Plug-in Incompatibilities ==
 +
{{TODO}} ''To be completed by all partners''
 +
== Modularisation ==
 +
{{TODO}} ''To be completed by Alexei Illiasov''
 +
== Decomposition ==
 +
{{TODO}} ''To be completed by Renato Silva'' 
 +
== Team-based Development ==
 +
{{TODO}} ''To be completed by Colin Snook, Vitaly Savicks''
 +
== UML-B ==
 +
{{TODO}} ''To be completed by Colin Snook, Vitaly Savicks''
 +
== ProR ==
 +
{{TODO}} ''To be completed by Michael Jastram''
 +
 
 +
 
 +
= References =
 
<references/>
 
<references/>
  
−
[[Category:D32 Deliverable]]
+
[[Category:D45 Deliverable]]

Revision as of 14:49, 18 November 2011

Overview

The Rodin platform versions concerned by this deliverable are:

  • 2.1(08.02.2011),
  • 2.2(01.06.2011),
  • 2.2.2(01.08.2011),
  • 2.3(04.10.2011),
  • 2.4(31.01.2011),
  • 2.5(30.04.2011).

This year, the maintenance carried on fixing identified bugs, although an emphasis has been put on correcting usability issues. Indeed, during the meeting in Nice, the WP9 members agreed to refocus on the needed tasks to address some specific bugs and issues reported by DEPLOY partners, and wished resolved by the end of DEPLOY. Thus, no new features were implemented but those appearing in the description of work. The tasks to be performed by the WP9 members were then scheduled, prioritized and regularly updated during the WP9 bi-weekly meetings. The updates allowed to capture and integrate rapidly some minor changes to enhance the usability of the platform which were required by the DEPLOY partners. 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).

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

  • General platform maintenance (Thomas Muller)

The maintenance done to overcome Rodin scalability weaknesses and enhance the proving experience will be detailed in a separate chapter. However, some features initially planned and some other which were later added and prioritized are worth to mention:

  • Possibility to highlight patterns in the ProverUI,
  • A better output providing warning and errors in case of wrong or missing building configurations,
  • The switch to Eclipse 3.7
  • A Handbook to complete and enhance the existing documentation.

These items will be detailed hereafter in this chapter.

  • TODO An overview of the contribution about Mathematical extensions / Theory Plug-in (Issam Maamria)
  • TODO An overview of the contribution about Plug-in Incompatibilities (All partners)
  • TODO An overview of the contribution about Modularisation (Alexei Illiasov)
  • TODO An overview of the contribution about Decomposition (Renato Silva)
  • TODO An overview of the contribution about Team-based Development (Colin Snook, Vitaly Savicks)
  • TODO An overview of the contribution about UML-B (Colin Snook, Vitaly Savicks)
  • TODO An overview of the contribution about ProR (Michael Jastram)

Motivations

The tasks to solve the issues faced by the DEPLOY partners have been listed and being assigned to groups according to their priority. A high priority means a high need in the outcome of a given task. The group 1 has the highest priority, the group 2 has an intermediate priority, and the group 3 has the lowest priority. The group 4 concerns topics that could not be ressourced during the lifetime of DEPLOY.The prover integrity item although not being directly covered, has been partially addressed thanks to Isabelle and SMT integration. Unfortunately, the originally planned export of full proofs and integrity check is beyond the scope of DEPLOY.


Group 1 (highest priority) Responsible
Performance
- Core (large models, etc.)
- GUI (incl. prover UI, edition, etc.)		 SYSTEREL
Prover Performances
- New rewriting rules / inference rules
- Automatic tactics (preferences, timeout, etc.)		 SYSTEREL
ProB Disprover (incl. counter examples to DLF POs) Düsseldorf
Stability (crash, corruption, etc.) SYSTEREL
Editors SYSTEREL/Düsseldorf
Group 2 Responsible
Prover Performances
- SMT provers integration
- connection with Isabelle
- Mathematical extensions
- ProB
SYSTEREL
ETH Zürich
Southampton/SYSTEREL
Düsseldorf
Scalability
- Decomposition
- Modularisation plug-in
- Team-based development
Southampton
Newcastle
Southampton
Plug-in incompatibilities Newcastle
Model-based testing Pitesti/Düsseldorf
ProR Düsseldorf
Group 3 Responsible
Scalability
- Generic instantiation
- UML-B maintenance

Southampton
ETH Zürich/Southampton
Code Generation Southampton
Group 4
Prover Integrity
Integrity of Code Generation

Platform maintenance

The platform maintenance, as it can be deduced from the above tables in section Motivations, mainly concerned stability and performance improvement. These topics will be discussed and detailed in a separate chapter about scalability improvements.
However, other prioritary improvements were made on the platform. These improvements or came from DEPLOY partners specific needs, or were corresponding to previously identified needs (listed in D32 - Model Construction tools & Analysis III Deliverable). Hence we review below the motivations of some noteworthy implemented features:

  • A Possibility to highlight patterns in the ProverUI.

This feature came from a request of DEPLOY partners[2], often facing the need to find particular patterns such as expressions in long predicates (e.g. long goals). Since Rodin 2.2, and its new ProvingUI interface, a nice feature was added, allowing to search and highlight a string pattern into the whole ProvingUI views and editors. This function as also been enabled on direct selection of text in this UI.

  • A better output providing warning and errors in case of wrong or missing building configurations.

This issue, often seen as a bug or a plug-in incompatibility, raises when a user imoprts and tries to use a model on a platform with some missing plug-ins needed on build. The user often use to think his models corrupted although Rodin just being not able to build them, and hiding this information to the user. This is why, since Rodin 2.3, an output in such case has been provided taking the form of warnings or errors that any user can review. This is a partial answer to Rodin plug-in incompatibilities issue.

  • The switch to Eclipse 3.7.

Due to the major improvements made every year in every Eclipse releases and the continuously growing number of contributing projects which are for some of them used as basis for Rodin plug-ins, the Rodin platform follows the evolution and is adapted every year quickly to the latest Eclipse version available. This year, Rodin 2.3 originated the switch from Eclipse 3.6 to Eclipse 3.7.

  • A Handbook to complete and enhance the existing documentation.

At the DEPLOY Plenary Meeting in Zürich in 2010, it has been stated that the current documentation, in its state at that time, would not support, a engineer starting using the tools without significant support of an expert. Losts of efforts to improve the documentation were performed and coordinated by Düsseldorf, and took form of the Rodin Handbook. The Rodin handbook has the aim to minimize the access to an expert, by providing the necessary assistance to an engineer in the need to be productive using Event-B and the Rodin toolset. The contents of the handbook were originated by the contents of the Event-B wiki, although these contents have now all been migrated to the Rodin handbook.

Mathematical extensions / Theory Plug-in

TODO To be completed by Issam Maamria

Plug-in Incompatibilities

TODO To be completed by all partners

Modularisation

TODO To be completed by Alexei Illiasov

Decomposition

TODO To be completed by Renato Silva

Team-based Development

TODO To be completed by Colin Snook, Vitaly Savicks

UML-B

TODO To be completed by Colin Snook, Vitaly Savicks

ProR

TODO To be completed by Michael Jastram

Choices / Decisions

Platform maintenance

  • Revisited task priority

This year, the process to give priority to maintenance tasks was revisited according the the refocus mentionned above. Thus not only the requests coming from DEPLOY partners were given high priorities, but they were prioritized against the already planned tasks coming from both DEPLOY partners and the Description of Work. This prioritization was performed or internally at each WP9 member site, if the task is short (i.e. less than one man-week), or during the WP9 bi-weekly telephone conferences otherwise.

  • A way to tackle plug-in incompatibilities
  • keeop 32-bit versions of Rodin on linux and windows systems

Mathematical extensions / Theory Plug-in

TODO To be completed by Issam Maamria

Plug-in Incompatibilities

TODO To be completed by all partners

Modularisation

TODO To be completed by Alexei Illiasov

Decomposition

TODO To be completed by Renato Silva

Team-based Development

TODO To be completed by Colin Snook, Vitaly Savicks

UML-B

TODO To be completed by Colin Snook, Vitaly Savicks

ProR

TODO To be completed by Michael Jastram

Available Documentation

  • Core platform:
The following pages give useful information about the Rodin platform releases:
  • Release notes[3].
  • Bugs[4].
  • Feature requests[5].
  • TODO Links for Mathematical extensions / Theory Plug-in
  • TODO Links for Plug-in Incompatibilities
  • TODO Links for Modularisation
  • TODO Links for Decomposition
  • TODO Links for Team-based Development
  • TODO Links for UML-B
  • TODO Links for ProR

Status

Platform maintenance

By the end of the project, there are :

  • xx bugs reported and open. All with a priority lower or equal to 5.
  • xx feature requests expressed and still open.

Mathematical extensions / Theory Plug-in

TODO To be completed by Issam Maamria

Plug-in Incompatibilities

TODO To be completed by all partners

Modularisation

TODO To be completed by Alexei Illiasov

Decomposition

TODO To be completed by Renato Silva

Team-based Development

TODO To be completed by Colin Snook, Vitaly Savicks

UML-B

TODO To be completed by Colin Snook, Vitaly Savicks

ProR

TODO To be completed by Michael Jastram


References

  1. ↑ 1.0 1.1 http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Available_Documentation Cite error: Invalid <ref> tag; name "documentation" defined multiple times with different content
  2. ↑ https://sourceforge.net/tracker/?func=detail&atid=651672&aid=3092835&group_id=108850
  3. ↑ http://wiki.event-b.org/index.php/Rodin_Platform_Releases
  4. ↑ https://sourceforge.net/tracker/?group_id=108850&atid=651669
  5. ↑ https://sourceforge.net/tracker/?group_id=108850&atid=651672
Retrieved from ‘https://wiki.event-b.org/index.php?title=D32_Teamwork&oldid=2820’