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>Pascal
 
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 was put on correcting usability issues. Indeed, during the annual 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 (initially to Ada). 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
+
|-
 +
|Editors || SYSTEREL/Düsseldorf
 
|-
 
|-
−
|Parameter Type
 
−
|ActualIn, ActualOut, FormalIn, FormalOut
 
 
|}
 
|}
−
</center>
+
{{SimpleHeader}}
−
 
+
|-
−
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.
+
! scope=col | Group 2 || Responsible
−
 
+
|-
−
=== Tasking Machines ===
+
| 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
−
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.
+
|-
−
 
+
|Scalability <br /> - Decomposition <br /> - Modularisation plug-in <br /> - Team-based development || <br /> Southampton <br /> Newcastle <br /> Southampton
−
* Tasking Machines may be characterised by the following types:
+
|-
−
** AutoTasks - Singleton Tasks.
+
|Plug-in incompatibilities || Newcastle
−
** 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.
+
|Model-based testing || Pitesti/Düsseldorf
−
** Priority - An integer value is supplied, the task with the highest value priority takes precedence when being scheduled.
+
|-
−
 
+
|ProR || Düsseldorf
−
=== Shared Machines ===
+
|}
−
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.
+
{{SimpleHeader}}
−
 
+
|-
−
* Applied to the Shared Machine we have:
+
! scope=col | Group 3 || Responsible
−
** A SharedMachine ''keyword'' that identifies a machine as a Shared Machine.
+
|-
−
 
+
|Scalability <br /> - Generic instantiation <br /> - UML-B maintenance <br /> || <br /> Southampton <br /> ETH Zürich/Southampton
−
=== Tasks and Events ===
+
|-
−
==== Control Constructs ====
+
|Code Generation || Southampton
−
Each Tasking Machine has a ''task body'' which contains the flow control, or algorithmic, constructs.  
+
|}
−
 
+
{{SimpleHeader}}
−
* We have the following constructs available in the Tasking Machine body:
+
|-
−
** Sequence - for imposing an order on events.
+
! scope=col | Group 4
−
** Branch - choice between a number of mutually exclusive events.
+
|-
−
** Loop - event repetition while it's guard remains true.
+
|Prover Integrity
−
** Event Synchronisation - synchronization between an event in a Tasking Machine and an event in a Shared Machine. Synchronization corresponds to an subroutine call with atomic (with respect to an external viewer) updates. The updates in the protected resource are implemented by a procedure call to a protected object, and tasks do no share state.  The synchronization construct also provides the means to specify parameter passing, both in and out of the task.
+
|-
−
** Event wrappers - The event 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 synchronizing). 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.
+
|Integrity of Code Generation
−
 
+
|}
−
==== Implementing Events ====
+
== Platform maintenance ==
−
An event's role in the implementation is identified using the following extensions which are added to the event. Events used in task bodies are 'references' that make use of existing event definitions from the abstract development. The events are extended. to assist with translation, with a keyword indicating their role in the implementation.
+
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).
−
* Event implementation.
+
Hence we review below the motivations of some noteworthy implemented features:
−
** Branch - In essence a task's event is split in the implementation; guards are mapped to branch conditions and actions to the branch body. If the branch refers to a Shared Machine event (procedureDef) then this is mapped to a simple procedure call.  
+
* A Possibility to highlight patterns in the ProverUI.
−
** Loop - The task's event guard maps to the loop condition and actions to to loop body. If the loop refers to a Shared Machine event then it is mapped to a simple procedure call.  
+
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.
−
** ProcedureSych - This usually indicates to the translator that the event maps to a subroutine, but an event in a task may not require a subroutine implementation if its role is simply to provide parameters for a procedure call.
+
* A better output providing warning and errors in case of wrong or missing building configurations.
−
** ProcedureDef - Identifies an event that maps to a (potentially blocking) subroutine definition. Event guards are implemented as a conditional wait; in Ada this is an entry barrier, and in C may use a pthread condition variable .
+
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.
−
In an implementation, when an subroutine is defined, its formal parameters are replaced by actual parameter values at run-time. To assist the code generator we extend the Event-B parameters. We identify formal and actual parameters in the implementation, and add the following keywords to the event parameters, as follows:
+
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.
−
* Event parameter types
+
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.
−
** FormalIn FormalOut - event parameters are extended with the ParameterType construct. Extension with formal parameters indicates a mapping to formal parameters in the implementation.
 
−
** ActualIn, ActualOut - Extension with an actual parameter indicates a mapping to an actual parameter in the implementation.
 
−
 
 
−
=== Other Technical Issues ===
 
−
==== Translation Technology ====
 
−
In order to provide a structured extensible code generation tool it was decided to use a multi-stage translation approach. The Event-B EMF model provided by the Event-B EMF Framework is extended to accommodate the tasking constructs as described above. The Tasking model is then translated to an intermediate model, the Common Language Model. The Common Language Meta-model is an abstraction of some useful generic programming constructs such as sequence, loop, branch and subroutine call/definition and so on. The translation of the Common Language Model to programme source code is then a relatively small step. The main translation activity takes place in the step between Tasking and Common Language models.
 
−
 
 
−
The decision was made to use Epsilon <ref name = "Epsilon"> </ref> to facilitate model to model translation for this stage. It was felt that an extensible, easily maintainable solution was required for this. Various model-to-model technologies (Java code, ATL, Epsilon) were appraised and it was judged that the Epsilon tool best matched our requirements. It proved to be a good choice initially for the specification of translations, especially in simpler areas of the project where the correspondence between models were simple. However the lack of debugging facilities, and productivity enhancements that are found in more mature tools, somewhat hindered rapid development as the project increased in complexity.
 
−
 
 
−
==== Implementation - Source Code ====
 
−
Early in the current phase of work we identified the possibility of translating the Common Language Model to EMF models of programming languages such as Ada and C, in addition to producing textual source. While the EMF route still remains an option, it was decided that we would produce a PrettyPrinter for the Ada code. This allows a user to cut and paste the Ada source code from the PrettyPrinter window to an Ada editor, and was by far the optimal route for this phase of the code generation activity in DEPLOY.
 
−
 
 
−
==== Editing the Tasking Model ====
 
−
The editor for the Tasking Development is based on a EMF tree-editor. The tree editor provides a facility for adding the extensions to Event-B constructs. The readability of the editor is enhanced by a PrettyPrinter, which provides a textual version of the Tasking Development, which is easier to read. It is envisaged that the textual notation will be fully integrated as a Camille extension when the facility/resources become available.
 
−
 
 
−
=== The Tool 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,
+
== Mathematical extensions / Theory Plug-in ==
−
** a Tasking Development Generator.
+
{{TODO}} ''To be completed by Issam Maamria''
−
** a Tasking Development Editor (Based on an EMF Tree Editor).
+
== Plug-in Incompatibilities ==
−
** a translator, from Tasking Development to Common Language Model (IL1).
+
By its extensibility nature, the Rodin platform is susceptible to incompatibilities. Indeed, there are many ways in which incompatibilities could occur, and it occured in the liftime of DEPLOY. A good example, is the dependency management. Suppose that a bundle x_v1.0 is needed by a plug-in A (i.e. a dependency from A has been defined to x in at most the version 1.0) and installed in Rodin. Then the plug-in x_v1.1 is needed by a plug-in B. The both versions 1.0 and 1.1 of x could not be installed and used at the same time and create thus some usage incompatibility.
−
** 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 ==
+
== Modularisation ==
−
=== Technical Background ===
+
{{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''
  
−
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>
+
= 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. 
 +
* 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 assembling and maintaining more platforms (5 platforms instead of 3) and the corrections brought to the database which improved the memory consumption pushed away the limitations of the platform, made this request no longer relevant for now.
  
−
Tooling issues were reported in a paper ''Tool Support for Event-B Code Generation''
+
== Mathematical extensions / Theory Plug-in ==
−
<ref name = "toolSupport">http://eprints.ecs.soton.ac.uk/20824/</ref>
+
{{TODO}} ''To be completed by Issam Maamria''
−
which was presented at ''Workshop on Tool Building in Formal Methods'',
+
== Plug-in Incompatibilities ==
−
http://abzconference.org/
+
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.<br>
 +
After the incompatibilities have been identified, the developing counterparts being concerned assigned special tasks and coordination to solve issues the soonest as possible. Incompatibilities are often due to little glitches or missynchronisation and such direct coordination of counterpart appeared appropriate because quick and effective.
  
−
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.
+
== 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''
  
−
=== For users ===
+
= 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>.
 +
*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 name="RodinHandbook">http://handbook.event-b.org/</ref>.
  
−
There is a wiki page at http://wiki.event-b.org/index.php/Code_Generation_Activity
+
*{{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
  
−
There is a tutorial at http://wiki.event-b.org/index.php/Code_Generation_Tutorial
+
= 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.
  
−
== Planning ==
+
== Mathematical extensions / Theory Plug-in ==
 +
{{TODO}} ''To be completed by Issam Maamria''
 +
== Plug-in Incompatibilities ==
 +
As the time of writing this deliverable, no plug-in incompatibilities are left or known to exist between the platform and plug-ins or between plug-ins.
  
−
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
+
== 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/>
 
<references/>
  
−
[[Category:D32 Deliverable]]
+
[[Category:D45 Deliverable]]

Revision as of 15:12, 23 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 was put on correcting usability issues. Indeed, during the annual 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

By its extensibility nature, the Rodin platform is susceptible to incompatibilities. Indeed, there are many ways in which incompatibilities could occur, and it occured in the liftime of DEPLOY. A good example, is the dependency management. Suppose that a bundle x_v1.0 is needed by a plug-in A (i.e. a dependency from A has been defined to x in at most the version 1.0) and installed in Rodin. Then the plug-in x_v1.1 is needed by a plug-in B. The both versions 1.0 and 1.1 of x could not be installed and used at the same time and create thus some usage incompatibility.

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.

  • 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 assembling and maintaining more platforms (5 platforms instead of 3) and the corrections brought to the database which improved the memory consumption pushed away the limitations of the platform, made this request no longer relevant for now.

Mathematical extensions / Theory Plug-in

TODO To be completed by Issam Maamria

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.
After the incompatibilities have been identified, the developing counterparts being concerned assigned special tasks and coordination to solve issues the soonest as possible. Incompatibilities are often due to little glitches or missynchronisation and such direct coordination of counterpart appeared appropriate because quick and effective.

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[4].
  • 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

As the time of writing this deliverable, no plug-in incompatibilities are left or known to exist between the platform and plug-ins or between plug-ins.

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. ↑ 4.0 4.1 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
Retrieved from ‘https://wiki.event-b.org/index.php?title=D32_Code_generation&oldid=2836’