Difference between pages "D32 Code generation" and "D45 General Platform Maintenance"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Tommy
 
Line 1: Line 1:
−
'''THIS DOCUMENT IS NOT YET COMPLETE !!!'''
+
= 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).
  
−
== General Overview ==
+
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.
  
−
The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as ''Shared Event Decomposition'' <ref name = "SharedEventDecomp">http://wiki.event-b.org/index.php/Event_Model_Decomposition</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">http://wiki.event-b.org/index.php/EMF_framework_for_Event-B</ref>. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in <ref name = "flow">http://wiki.event-b.org/index.php/Flows </ref> and the algorithmic structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' <ref name = "Epsilon"> http://www.eclipse.org/gmt/epsilon/</ref> model-to-model transformation technology.
+
* 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.
  
−
== Motivations ==
+
* {{TODO}} An overview of the contribution about Mathematical extensions / Theory Plug-in (Issam Maamria)
  
−
The decision was taken in 2009 to include code generation as a project goal <ref name = "d23"> http://wiki.event-b.org/index.php/D23_Code_Generation </ref>. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.
+
* {{TODO}} An overview of the contribution about Plug-in Incompatibilities (All partners)  
  
−
== Choices / Decisions ==
+
* {{TODO}} An overview of the contribution about Modularisation (Alexei Illiasov)
−
=== Strategic Overview ===
 
−
During the last year we have focussed on supporting the generation of code for typical real-time embedded control software. To this end we have evolved a multi-tasking approach which is conceptually similar to that of the Ada tasking model. Individual tasks are treated as sequential programs; these tasks are modelled by an extension to Event-B, called ''Tasking Machines''.  Tasks have mutually exclusive access to state variables through the use of protected resources. The protected resources correspond to Event-B machines. For real-time control, periodic and one-shot activation is currently supported; and it is planned to support aperiodic tasks in the near future. Tasks have priorities to ensure appropriate responsiveness of the control software. For the DEPLOY project, it was regarded as sufficient to support construction of programs with a fixed number of tasks and a fixed number of shared variables – no dynamic creation of processes or objects has been accommodated.
 
  
−
Our main goal this year has been to devise an approach for, and provide tool support for, code generation. In accord with the resources available during the year it was decided to limit the provision of tool support to that of a demonstrator tool. The tool is a proof-of-concept only, and lacks the productivity enhancements expected in a more mature tool. Nevertheless much insight has been gained in undertaking this work; it lays a foundation for future research, and will be useful since it will allow interested parties to explore the approach.
+
* {{TODO}} An overview of the contribution about Decomposition (Renato Silva)
  
−
=== The Tasking Extension for Event-B ===
+
* {{TODO}} An overview of the contribution about Team-based Development (Colin Snook, Vitaly Savicks)
  
−
The following text can be read in conjunction with the slides<ref name = "Zurich2010Slides">http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d108734/Andy%20Edmunds%20-%20Code%20Generation%20Slides.pdf</ref> from the Deploy Plenary Meeting - Zurich 2010.
+
* {{TODO}} An overview of the contribution about UML-B (Colin Snook, Vitaly Savicks)
  
−
Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structure a development that is suitable for construction of a Tasking Development. At some point during the modelling phase parameters may have to be introduced to facilitate decomposition. This constitutes a natural part of the refinement process as it moves towards decomposition and on to the implementation level. During decomposition parameters form part of the interface that enables event synchronization. We make use of this interface and add information (see [[#Events For Tasking]]) to facilitate code generation.
+
* {{TODO}} An overview of the contribution about ProR (Michael Jastram)
  
−
A Tasking Development is generated programmatically, at the direction of the user; the Tasking Development consists of a number of machines (and perhaps associated contexts). In our approach we make use of the Event-B EMF extension mechanism which allows addition of new constructs to a model. The tasking extension consists of the constructs in the following table.
+
= 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.
  
−
<center>
+
{{SimpleHeader}}
−
{| border="1"
 
−
|Construct
 
−
|Options
 
 
|-
 
|-
−
|Machine Type
+
! scope=col | Group 1 (highest priority) || Responsible
−
|DeclaredTask, AutoTask, SharedMachine
 
 
|-
 
|-
−
|Control
+
|Performance <br /> - Core (large models, etc.) <br /> - GUI (incl. prover UI, edition, etc.) || SYSTEREL
−
|Sequence, Loop, Branch, EventSynch
 
 
|-
 
|-
−
|Task Type
+
|Prover Performances <br /> - New rewriting rules / inference rules <br /> - Automatic tactics (preferences, timeout, etc.) || SYSTEREL
−
|Periodic(n), Triggered, Repeating, OneShot
 
 
|-
 
|-
−
|Priority
+
|ProB Disprover (incl. counter examples to DLF POs) || Düsseldorf
−
| -
 
 
|-
 
|-
−
|Event Type
+
|Stability (crash, corruption, etc.)  || SYSTEREL
−
|Branch, Loop, ProcedureDef, ProcedureSynch
 
 
|-
 
|-
−
|Parameter Type
+
|Editors || SYSTEREL/Düsseldorf
−
|ActualIn, ActualOut, FormalIn, FormalOut
+
|-
 +
|}
 +
{{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
 
|}
 
|}
−
</center>
+
{{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 <ref name="documentationoverhaul>http://wiki.event-b.org/index.php/User_Documentation_Overhaul</ref>. Losts of efforts to improve the documentation were performed and coordinated by Düsseldorf, and took form of a handbook<ref name="RodinHandbook">http://handbook.event-b.org/</ref>. 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, user oriented, were originated by the contents of the Event-B wiki, which have been finally migrated from the wiki to the Rodin handbook.
  
−
The machines in the Tasking Development are extended with the constructs shown in the table, and may be viewed as keywords in a textual representation of the language. With extensions added, a Tasking Development can be translated to a common language model for mapping to implementation source code. There is also a translator that constructs new machines/contexts modelling the implementation, and these should refine/extend the existing elements of the Event-B project.
+
== 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''
  
−
=== Tasking Machines ===
+
= Choices / Decisions =
−
The following constructs relate only to Tasking Machines, and provide implementation details. Timing of periodic tasks is not modelled formally. Tasking Machines are related to the concept of an Ada task. These can be implemented in Ada using tasks, in C using the pthread library C, or in Java using threads.
+
== Platform maintenance ==
 +
* Revisited task priority
 +
This year, the process of giving priority to maintenance tasks was revisited according the the refocus mentionned above. The aim was address all the major scalability issues before the end of DEPLOY. 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
 +
It has been decided in concertation with all the WP9 partners to find better ways to address the plug-in incompatibility issues. First of all, the various partners refined the concept of "plug-in incompatibility". Hence, various aspects could be identified and some specific answers were given to each of them. The user could then defined more clearly the incompatibility faced. Plug-in incompatibilities can be separated in two categories:
 +
:* Rodin/plug-in incompatibilities, due to some wrong match between Rodin included packages and the plug-in dependencies (i.e. needed packages). These incompatibilities when reported allowed the plug-in developpers to contact SYSTEREL in charge of managing the packages shipped with a given version of Rodin. It could also allow tracability of incompatibilities and information to the user through a specific and actualized table on each Rodin release notes page on the Wiki<ref name="incompTableA">http://wiki.event-b.org/index.php/Rodin_Platform_Releases#Current_plug-ins</ref>.
 +
:* plug-in/plug-in incompatibilities, due to some wrong match between needed/installed packages, or API/ressources incompatible usage. A table was created on each release notes wiki page, and a procedure was defined<ref name="incompTableB">http://wiki.event-b.org/index.php/Rodin_Platform_Releases#Known_plug-in_incompatibilities</ref> so that identified incompatibilities are listed and corrected by the concerned developers.
 +
It appeared that cases of using a model which references some missing plug-ins were formerly often seen as compatibility issues although they are not.
  
−
* Tasking Machines may be characterised by the following types:
+
* Keep 32-bit versions of the Rodin platform on linux and windows systems
−
** AutoTasks - Singleton Tasks.
+
It was asked by end users to make both 32-bit and 64-bit versions of the Rodin platform available for Linux and Windows platforms. Only a 64-bit version of Rodin is available on Mac platforms as 32-bit Mac (early 2006) platforms are no longer maintained. The request to offer 64-bit was motivated by the possibility to increase for them the available java heap size for some memory greedy platforms (these before 2.3). However, the drawbacks of maintaining more platforms (5 instead of 3) and the corrections brought to the database which improved the memory consumption, made this request no longer relevant.
−
** Declared tasks - (Not currently used) A task template relating to an Ada ''tasktype'' declaration.
 
−
** TaskType - Defines the scheduling, cycle and lifetime of a task. i.e. one-shot periodic or triggered.
 
−
** Priority - An integer value is supplied, the task with the highest value priority takes precedence when being scheduled.
 
  
−
=== Shared Machines ===
+
== Mathematical extensions / Theory Plug-in ==
−
A Shared Machine corresponds to the concept of a protected resource, such as a monitor. They may be implemented in Ada as a Protected Object, in C using mutex locking, or in Java as a monitor.
+
{{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''
  
−
* Applied to the Shared Machine we have:
+
= Available Documentation =
−
** A SharedMachine ''keyword'' that identifies a machine as a Shared Machine.
+
* 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>.
 +
*The Rodin handbook is proposed as a PDF version and a HTML version and a dedicated plug-in makes it available as help within Rodin<ref>http://handbook.event-b.org/</ref>.
  
−
=== More Details ===
+
*{{TODO}}  Links for Mathematical extensions / Theory Plug-in
−
==== Control Constructs ====
+
*{{TODO}}  Links for Plug-in Incompatibilities
−
Each Tasking Machine has a ''task body'' which contains the flow control, or algorithmic, constructs.
+
*{{TODO}}  Links for Modularisation
 +
*{{TODO}}  Links for Decomposition
 +
*{{TODO}}  Links for Team-based Development
 +
*{{TODO}}  Links for UML-B
 +
*{{TODO}}  Links for ProR
  
−
* We have the following constructs available in the Tasking Machine body:
+
= Status =
−
** Sequence - for imposing an order on events.
+
== Platform maintenance ==
−
** Branch - choice between a number of mutually exclusive events.
+
By the end of the project, there are :
−
** Loop - event repetition while it's guard remains true.
+
* xx bugs reported and open. All with a priority lower or equal to 5.
−
** Event Synchronisation - synchronization between an event in a Tasking Machine and an event in a Shared Machine.
+
* xx feature requests expressed and still open.
−
** Event-wrappers - The synchronization construct is contained in an event wrapper. The wrapper may also contain a single event (we re-use the synchronization construct, but do not use it for this purpose). The event may belong to the Tasking Machine, or to a Shared Machine that is visible to the task. Single events in a wrapper correspond to a subroutine call in an implementation.
 
  
−
==== Events In Tasking Developments ====
+
== Mathematical extensions / Theory Plug-in ==
−
Event implementation. Branch, Loop, ProcedureSych, ProcedureDef
+
{{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''
  
−
Event parameter types. FormalIn FormalOut, ActualIn, ActualOut
 
  
−
* In Shared Machines:
+
= References =
−
** events can only be designated as ProcedureDef or ProcedureSynch.
+
<references/>
−
** parameters of ProcedureSynch can only be FormalIn or FormalOut
 
−
 
 
−
* In procedureDef
 
−
** parameters are not allowed.
 
−
 
 
−
=== Other Technical Issues ===
 
−
 
 
−
Meta-models: The use of Epsilon for translation.
 
−
 
 
−
=== The Deliverable ===
 
−
The demonstrator tool was released on 30 November 2010, and is available as an update site, or bundled Rodin package from:
 
−
https://sourceforge.net/projects/codegenerationd/files
 
−
 
 
−
Sources are available from:
 
−
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
 
−
 
 
−
The tool is based on a build of Rodin 1.3.1 (not Rodin 2.0.0 due to dependency conflicts).
 
−
 
 
−
* The Code Generation tool consists of,
 
−
** a Tasking Development Generator.
 
−
** a Tasking Development Editor (Based on an EMF Tree Editor).
 
−
** a translator, from Tasking Development to Common Language Model (IL1).
 
−
** a translator, from the Tasking Development to Event-B model of the implementation.
 
−
** a pretty-printer for the Tasking Development.
 
−
** a pretty-printer for Common Language Model, which generates Ada Source Code.
 
−
 
 
−
== Available Documentation ==
 
−
 
 
−
 
 
−
Much insight was gained during the work on code generation reported in the thesis ''Providing Concurrent Implementations for Event-B Developments'' <ref name="aeThesis">http://eprints.ecs.soton.ac.uk/20826/</ref>
 
−
 
 
−
Tooling issues were reported in a paper ''Tool Support for Event-B Code Generation''
 
−
<ref name = "toolSupport">http://eprints.ecs.soton.ac.uk/20824/</ref>
 
−
which was presented at ''Workshop on Tool Building in Formal Methods'',
 
−
http://abzconference.org/
 
  
−
There are technical notes available <ref name = "techNotes">http://wiki.event-b.org/images/Translation.pdf</ref>, that give more precise details of the approach and the mapping between Event-B and the common language meta-model, and its corresponding Event-B model.
+
[[Category:D45 Deliverable]]
−
 
 
−
=== For users ===
 
−
 
 
−
There is a wiki page at http://wiki.event-b.org/index.php/Code_Generation_Activity
 
−
 
 
−
There is a tutorial at http://wiki.event-b.org/index.php/Code_Generation_Tutorial
 
−
 
 
−
== Planning ==
 
−
 
 
−
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
 
−
 
 
−
== References ==
 
−
 
 
−
<references/>
 

Revision as of 09:28, 21 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 [3]. Losts of efforts to improve the documentation were performed and coordinated by Düsseldorf, and took form of a handbook[4]. 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, user oriented, were originated by the contents of the Event-B wiki, which have been finally migrated from the wiki 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 of giving priority to maintenance tasks was revisited according the the refocus mentionned above. The aim was address all the major scalability issues before the end of DEPLOY. 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

It has been decided in concertation with all the WP9 partners to find better ways to address the plug-in incompatibility issues. First of all, the various partners refined the concept of "plug-in incompatibility". Hence, various aspects could be identified and some specific answers were given to each of them. The user could then defined more clearly the incompatibility faced. Plug-in incompatibilities can be separated in two categories:

  • Rodin/plug-in incompatibilities, due to some wrong match between Rodin included packages and the plug-in dependencies (i.e. needed packages). These incompatibilities when reported allowed the plug-in developpers to contact SYSTEREL in charge of managing the packages shipped with a given version of Rodin. It could also allow tracability of incompatibilities and information to the user through a specific and actualized table on each Rodin release notes page on the Wiki[5].
  • plug-in/plug-in incompatibilities, due to some wrong match between needed/installed packages, or API/ressources incompatible usage. A table was created on each release notes wiki page, and a procedure was defined[6] so that identified incompatibilities are listed and corrected by the concerned developers.

It appeared that cases of using a model which references some missing plug-ins were formerly often seen as compatibility issues although they are not.

  • Keep 32-bit versions of the Rodin platform on linux and windows systems

It was asked by end users to make both 32-bit and 64-bit versions of the Rodin platform available for Linux and Windows platforms. Only a 64-bit version of Rodin is available on Mac platforms as 32-bit Mac (early 2006) platforms are no longer maintained. The request to offer 64-bit was motivated by the possibility to increase for them the available java heap size for some memory greedy platforms (these before 2.3). However, the drawbacks of maintaining more platforms (5 instead of 3) and the corrections brought to the database which improved the memory consumption, made this request no longer relevant.

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[7].
  • Bugs[8].
  • Feature requests[9].
  • The Rodin handbook is proposed as a PDF version and a HTML version and a dedicated plug-in makes it available as help within Rodin[10].
  • 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/User_Documentation_Overhaul
  4. ↑ http://handbook.event-b.org/
  5. ↑ http://wiki.event-b.org/index.php/Rodin_Platform_Releases#Current_plug-ins
  6. ↑ http://wiki.event-b.org/index.php/Rodin_Platform_Releases#Known_plug-in_incompatibilities
  7. ↑ http://wiki.event-b.org/index.php/Rodin_Platform_Releases
  8. ↑ https://sourceforge.net/tracker/?group_id=108850&atid=651669
  9. ↑ https://sourceforge.net/tracker/?group_id=108850&atid=651672
  10. ↑ http://handbook.event-b.org/
Retrieved from ‘https://wiki.event-b.org/index.php?title=D32_Code_generation&oldid=2829’