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

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
m
 
imported>Tommy
 
Line 1: Line 1:
−
= General Overview =
+
= Overview =
 +
The main goal of the platform corrective and evolutive maintenance is to fix the listed known bugs, and implement some new requested features. As in the previous years of DEPLOY, these bugs and features are reported either by mail or through dedicated SourceForge trackers.
  
−
The 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">[[Event_Model_Decomposition]]</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">[[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">[[Flows]]</ref> and the flow control 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.
+
The terse list below gives an overwiew of the noteworthy features added in the main platform during the past year:
 +
* Proof replay on undischarged POs (since release 1.3)
 +
: It often happens, while modifying a model, that a set of previously manually discharged POs have slightly changed and need to be discharged again. However, replaying the proof for these POs could most of the time be enough to discharge it. Hence, a command was added to manually try replaying the proofs for a set of undischarged POs. This request comes directly from end users<ref>https://sourceforge.net/tracker/?func=detail&aid=2949606&group_id=108850&atid=651672</ref>. See <ref>http://wiki.event-b.org/index.php/Proof_Obligation_Commands</ref>.
 +
* Rule Details View (since release 2.0)
 +
: When doing an interactive proof, one is guided by the proof tree appearing on the proof tree view. However, it is sometimes needed to get more information about the rules involved in a proof, such as instantiation details, used hypotheses, etc. The Rule Details View<ref>http://wiki.event-b.org/index.php/Rodin_Proving_Perspective#Rule_Details_View</ref> displaying such details has been added.
 +
* Refactory plug-in (since release 1.2)
 +
: The Refactory<ref>http://wiki.event-b.org/index.php/Refactoring_Framework</ref> plug-in allows users of the Rodin platform to rename modelling elements. With a unique operation, both declaration and occurrences of an element are renamed. Moreover, renaming an element also modifies the corresponding proof, so that renaming does not change the proof status (no loss of proof).
 +
* Mathematical extensions (since release 2.0)
 +
: The integration of mathematical extensions required a major rework of the deep internals of the platform (in particular all code related to the manipulation of mathematical formulas). See <ref>http://wiki.event-b.org/index.php/D32_Mathematical_Extensions</ref>.
 +
* Documentation
 +
: Plug-in developers expressed their need to get a detailed documentation about Rodin extension ability. A dedicated tutorial<ref>http://wiki.event-b.org/index.php/Plug-in_Tutorial </ref><ref name="documentation">http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Available_Documentation</ref> has been written accordingly, and was the support of a full-day tutorial session given at the Rodin User and Developer Workshop<ref>http://www.event-b.org/rodin10.html </ref> in Düsseldorf this year.
 +
: The user manual, user tutorial and other developer documentation on the wiki<ref>http://wiki.event-b.org</ref> are continuously, and collaboratively updated and enhanced. Moreover, as soon as a new feature is added to the platform, the corresponding user documentation is created on the Wiki.
 +
 
 +
See the Release Notes<ref name="documentation">http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Available_Documentation</ref> and the SourceForge<ref name=documentation>http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Available_Documentation</ref> databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
  
 
= Motivations =
 
= Motivations =
 +
The evolutive maintenance (resp. corrective maintenance) has its origin in the DEPLOY description of work, and the various requests (resp. bug reports) listed by WP1-4 partners, developers and users. Since the DEPLOY project inception, various streams have been used to request new features or track known bugs:
 +
: - dedicated trackers<ref name="bugTracker">http://sourceforge.net/tracker/?group_id=108850&atid=651669</ref><ref name="frTracker">http://sourceforge.net/tracker/?group_id=108850&atid=651672</ref>,
 +
: - platform mailing lists <ref>http://sourceforge.net/mail/?group_id=108850</ref>
 +
: - DEPLOY WP9 mailing list.
 +
Maintenance tasks to perform are collected from the aforementioned streams and scheduled during WP9 meetings. These tasks are processed in the same way as the task planned in the description of work.
  
−
The decision was taken in 2009 to include code generation as a project goal <ref name = "d23"> [[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.
+
The following table describes the main tasks (either performed or scheduled) motivating the evolutive maintenance:
−
 
+
{{SimpleHeader}}
−
= Choices / Decisions =
+
|-
−
== Strategic Overview ==
+
! scope=col | Origin || Maintenance Task || Done in 2011
−
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. Tasks are modelled by an extension to Event-B, called ''Tasking Machines''. Tasking Machines are an extension of the existing Event-B Machine component. In implementations such as Ada, tasks share the resources and have mutually exclusive access to shared state through the use of a protection mechanism. An Event-B machine can also be viewed as an abstraction of a shared resource, and the  mechanism protecting it. We use existing Event-B machines with minimal extensions (called Shared Machines) to represent shared resources.
 
−
 
 
−
For real-time control, periodic and one-shot activation is currently supported; and it is planned to support triggered 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.
 
−
 
 
−
== The Tasking Extension for Event-B ==
 
−
 
 
−
The following text can be read in conjunction with the slides<ref name = "Zurich2010Slides">http://deploy-eprints.ecs.soton.ac.uk/260/2/CGSlidesAndy%2520Edmunds%2520-%2520Code%2520Generation%2520Slides.pdf</ref> from the Deploy Plenary Meeting - Zurich 2010.
 
−
 
 
−
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 [[#Implementing Events]]) to facilitate code generation.
 
−
 
 
−
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.
 
−
 
 
−
<center>
 
−
{| border="1"
 
−
|Construct
 
−
|Options
 
 
|-
 
|-
−
|Machine Type
+
| DoW / WP1-4 partners || Prover efficiency and integrity || x
−
|DeclaredTask, AutoTask, SharedMachine
 
 
|-
 
|-
−
|Control
+
| WP1-4 partners|| Edition ||  || x
−
|Sequence, Loop, Branch, EventSynch
 
 
|-
 
|-
−
|Task Type
+
| WP1-4 partners|| Increase platform stability ||  || x
−
|Periodic(n), Triggered, Repeating, OneShot
 
 
|-
 
|-
−
|Priority
+
| WP1-4 partners|| Search in goal window <ref>https://sourceforge.net/tracker/?func=detail&atid=651672&aid=3092835&group_id=108850</ref> ||  || x
−
| -
 
 
|-
 
|-
−
|Event Type
+
| WP1-4 partners|| Preferences for the automatic tactics <ref>http://sourceforge.net/tracker/index.php?func=detail&aid=1581775&group_id=108850&atid=651672</ref> ||  || x
−
|Branch, Loop, ProcedureDef, ProcedureSynch
 
 
|-
 
|-
−
|Parameter Type
+
| End Users || Displaying the inherited elements || || x
−
|ActualIn, ActualOut, FormalIn, FormalOut
 
 
|}
 
|}
−
</center>
 
  
−
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.
+
= Choices / Decisions =
−
 
+
* Task priority
−
== Tasking Machines ==
+
: Listed tasks are being given a priority during WP9 bi-weekly meetings, and then assigned to partners in charge of their processing. A higher priority is given to requests originating from deployment parteners.
−
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.
+
* 64-bit release of Rodin for Mac platforms
−
 
+
: A major UI bug, due to some incompatibilities between Eclipse 3.5 and Java 1.6 on Mac platforms motivated the migration to the Eclipse 3.6 as basis for the Rodin 2.0 platform. In the meantime, as the 32-bit Java Virtual Machine is no longer supported on Mac platforms, Rodin migrated to Java 1.6, so that the release 2.0 of Rodin became a 64-bit Mac platform only.
−
* Tasking Machines may be characterised by the following types:
+
: The Rodin platforms family is then composed of three executables : 32-bit platforms for Linux and Windows environments and a 64-bit platform for Mac computers.
−
** AutoTasks - Singleton Tasks.
+
* Rodin sources
−
** Declared tasks - (Not currently used) A task template relating to an Ada ''tasktype'' declaration.
+
: The sources of Rodin are now bundled together with the binary platform. It provides developers with a convenient alternative to the available sources<ref>http://wiki.event-b.org/index.php/Using_Rodin_as_Target_Platform</ref> on SourceForge.
−
** TaskType - Defines the scheduling, cycle and lifetime of a task. i.e. one-shot periodic or triggered.
+
* Release notes
−
** Priority - An integer value is supplied, the task with the highest value priority takes precedence when being scheduled.
+
: The release notes contain information about the released plug-ins and centralise the requirements or existing issues which could not be stated at the main platform release date. Thus, since Rodin 2.0 release, it has been chosen to link the contents of the release notes text file included in Rodin releases, with the contents of the dedicated Wiki page.
−
 
 
−
== 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.
 
−
 
 
−
* Applied to the Shared Machine we have:
 
−
** A SharedMachine ''keyword'' that identifies a machine as a Shared Machine.
 
−
 
 
−
== Tasks and Events ==
 
−
=== Control Constructs ===
 
−
Each Tasking Machine has a ''task body'' which contains the flow control, or algorithmic, constructs.
 
−
 
 
−
* We have the following constructs available in the Tasking Machine body:
 
−
** Sequence - for imposing an order on events.
 
−
** Branch - choice between a number of mutually exclusive events.
 
−
** Loop - event repetition while it's guard remains true.
 
−
** 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.
 
−
 
 
−
=== Implementing Events ===
 
−
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.
 
−
 
 
−
* Event implementation.
 
−
** Branch - In essence a task's event is split in the implementation; guards are mapped to branch conditions and actions are mapped to the branch body. If the branch refers to a Shared Machine event (procedureDef) then this is mapped to a simple procedure call.
 
−
** 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.
 
−
** 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.
 
−
** 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 .
 
−
 
 
−
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:
 
−
 
 
−
* Event parameter types
 
−
** FormalIn or FormalOut - event parameters are extended with the ParameterType construct. Extension with formal parameters indicates a mapping to formal parameters in the implementation.
 
−
** ActualIn or 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 the optimal route to code 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,
 
−
** 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 =
 
= Available Documentation =
−
== Technical Background ==
+
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>.
−
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>
+
* Bugs<ref>http://sourceforge.net/tracker/?atid=651669&group_id=108850</ref>.
−
 
+
* Feature requests<ref>http://sourceforge.net/tracker/?group_id=108850&atid=651672</ref>.
−
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.
 
−
 
 
−
== For Users ==
 
−
 
 
−
There is an overview at [[Tasking Event-B Overview ]]
 
−
 
 
−
There is a wiki page at [[Code_Generation_Activity]]
 
−
 
 
−
There is a tutorial at [[Code_Generation_Tutorial]]
 
  
 
= Planning =
 
= Planning =
 +
For the coming year, the following topics pointed out at the last plenary meeting by the WP1-WP4 partners and encompassing end-user requests (see scheduled tasks in <ref>http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Motivations</ref>) will be favoured by the WP9 partners:
 +
* Platform stability and performances
 +
: Currently, users struggle with editing or proving a model due to performance issues in the Rodin platform. Solving these issues represents a real challenge for the coming year and is mandatory for the industrial adoption of the Event-B methodology and Rodin platform.
 +
* Prover efficiency and integrity
 +
: Having all models automatically proved is the ideal goal. Thus, enhancing provers is a continuous task to be performed until the end of the DEPLOY project. Ensuring provers correctness and improving confidence in them is another important goal that will be pursued in the coming year.
 +
* Plug-in incompatibilities
 +
: When several plug-ins are installed, conflicts between them can arise. The cumbersome behaviour spawned by such incompatibilities leads to users' disappointment or can render the platform unusable. Special efforts will be made to identify the source of incompatibilities among plug-ins. Moreover, necessary corrective maintenance tasks and assignments will be coordinated and executed.
  
−
During 2011 we plan to develop the code generation tools further, taking on board any feedback from interested parties. The tool support should advance to the prototype stage, with improvements in the tool's usability in terms of features and user experience.
+
== References ==
−
 
 
−
=== References ===
 
−
 
 
 
<references/>
 
<references/>
  
 
[[Category:D32 Deliverable]]
 
[[Category:D32 Deliverable]]

Revision as of 16:23, 14 November 2011

Overview

The main goal of the platform corrective and evolutive maintenance is to fix the listed known bugs, and implement some new requested features. As in the previous years of DEPLOY, these bugs and features are reported either by mail or through dedicated SourceForge trackers.

The terse list below gives an overwiew of the noteworthy features added in the main platform during the past year:

  • Proof replay on undischarged POs (since release 1.3)
It often happens, while modifying a model, that a set of previously manually discharged POs have slightly changed and need to be discharged again. However, replaying the proof for these POs could most of the time be enough to discharge it. Hence, a command was added to manually try replaying the proofs for a set of undischarged POs. This request comes directly from end users[1]. See [2].
  • Rule Details View (since release 2.0)
When doing an interactive proof, one is guided by the proof tree appearing on the proof tree view. However, it is sometimes needed to get more information about the rules involved in a proof, such as instantiation details, used hypotheses, etc. The Rule Details View[3] displaying such details has been added.
  • Refactory plug-in (since release 1.2)
The Refactory[4] plug-in allows users of the Rodin platform to rename modelling elements. With a unique operation, both declaration and occurrences of an element are renamed. Moreover, renaming an element also modifies the corresponding proof, so that renaming does not change the proof status (no loss of proof).
  • Mathematical extensions (since release 2.0)
The integration of mathematical extensions required a major rework of the deep internals of the platform (in particular all code related to the manipulation of mathematical formulas). See [5].
  • Documentation
Plug-in developers expressed their need to get a detailed documentation about Rodin extension ability. A dedicated tutorial[6][7] has been written accordingly, and was the support of a full-day tutorial session given at the Rodin User and Developer Workshop[8] in Düsseldorf this year.
The user manual, user tutorial and other developer documentation on the wiki[9] are continuously, and collaboratively updated and enhanced. Moreover, as soon as a new feature is added to the platform, the corresponding user documentation is created on the Wiki.

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

Motivations

The evolutive maintenance (resp. corrective maintenance) has its origin in the DEPLOY description of work, and the various requests (resp. bug reports) listed by WP1-4 partners, developers and users. Since the DEPLOY project inception, various streams have been used to request new features or track known bugs:

- dedicated trackers[10][11],
- platform mailing lists [12]
- DEPLOY WP9 mailing list.

Maintenance tasks to perform are collected from the aforementioned streams and scheduled during WP9 meetings. These tasks are processed in the same way as the task planned in the description of work.

The following table describes the main tasks (either performed or scheduled) motivating the evolutive maintenance:

Origin Maintenance Task Done in 2011
DoW / WP1-4 partners Prover efficiency and integrity x
WP1-4 partners Edition x
WP1-4 partners Increase platform stability x
WP1-4 partners Search in goal window [13] x
WP1-4 partners Preferences for the automatic tactics [14] x
End Users Displaying the inherited elements x

Choices / Decisions

  • Task priority
Listed tasks are being given a priority during WP9 bi-weekly meetings, and then assigned to partners in charge of their processing. A higher priority is given to requests originating from deployment parteners.
  • 64-bit release of Rodin for Mac platforms
A major UI bug, due to some incompatibilities between Eclipse 3.5 and Java 1.6 on Mac platforms motivated the migration to the Eclipse 3.6 as basis for the Rodin 2.0 platform. In the meantime, as the 32-bit Java Virtual Machine is no longer supported on Mac platforms, Rodin migrated to Java 1.6, so that the release 2.0 of Rodin became a 64-bit Mac platform only.
The Rodin platforms family is then composed of three executables : 32-bit platforms for Linux and Windows environments and a 64-bit platform for Mac computers.
  • Rodin sources
The sources of Rodin are now bundled together with the binary platform. It provides developers with a convenient alternative to the available sources[15] on SourceForge.
  • Release notes
The release notes contain information about the released plug-ins and centralise the requirements or existing issues which could not be stated at the main platform release date. Thus, since Rodin 2.0 release, it has been chosen to link the contents of the release notes text file included in Rodin releases, with the contents of the dedicated Wiki page.

Available Documentation

The following pages give useful information about the Rodin platform releases:

Planning

For the coming year, the following topics pointed out at the last plenary meeting by the WP1-WP4 partners and encompassing end-user requests (see scheduled tasks in [19]) will be favoured by the WP9 partners:

  • Platform stability and performances
Currently, users struggle with editing or proving a model due to performance issues in the Rodin platform. Solving these issues represents a real challenge for the coming year and is mandatory for the industrial adoption of the Event-B methodology and Rodin platform.
  • Prover efficiency and integrity
Having all models automatically proved is the ideal goal. Thus, enhancing provers is a continuous task to be performed until the end of the DEPLOY project. Ensuring provers correctness and improving confidence in them is another important goal that will be pursued in the coming year.
  • Plug-in incompatibilities
When several plug-ins are installed, conflicts between them can arise. The cumbersome behaviour spawned by such incompatibilities leads to users' disappointment or can render the platform unusable. Special efforts will be made to identify the source of incompatibilities among plug-ins. Moreover, necessary corrective maintenance tasks and assignments will be coordinated and executed.

References

  1. ↑ https://sourceforge.net/tracker/?func=detail&aid=2949606&group_id=108850&atid=651672
  2. ↑ http://wiki.event-b.org/index.php/Proof_Obligation_Commands
  3. ↑ http://wiki.event-b.org/index.php/Rodin_Proving_Perspective#Rule_Details_View
  4. ↑ http://wiki.event-b.org/index.php/Refactoring_Framework
  5. ↑ http://wiki.event-b.org/index.php/D32_Mathematical_Extensions
  6. ↑ http://wiki.event-b.org/index.php/Plug-in_Tutorial
  7. ↑ 7.0 7.1 7.2 http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Available_Documentation
  8. ↑ http://www.event-b.org/rodin10.html
  9. ↑ http://wiki.event-b.org
  10. ↑ http://sourceforge.net/tracker/?group_id=108850&atid=651669
  11. ↑ http://sourceforge.net/tracker/?group_id=108850&atid=651672
  12. ↑ http://sourceforge.net/mail/?group_id=108850
  13. ↑ https://sourceforge.net/tracker/?func=detail&atid=651672&aid=3092835&group_id=108850
  14. ↑ http://sourceforge.net/tracker/index.php?func=detail&aid=1581775&group_id=108850&atid=651672
  15. ↑ http://wiki.event-b.org/index.php/Using_Rodin_as_Target_Platform
  16. ↑ http://wiki.event-b.org/index.php/Rodin_Platform_Releases
  17. ↑ http://sourceforge.net/tracker/?atid=651669&group_id=108850
  18. ↑ http://sourceforge.net/tracker/?group_id=108850&atid=651672
  19. ↑ http://wiki.event-b.org/index.php/D32_General_Platform_Maintenance#Motivations
Retrieved from ‘https://wiki.event-b.org/index.php?title=D32_Code_generation&oldid=2435’