Difference between pages "Code Generation Activity" and "D45 General Platform Maintenance"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Tommy
 
Line 1: Line 1:
−
Tasking Event-B is the extension of Event-B for defining concurrent systems sharing data, for details see the [[Tasking Event-B Overview]] page. For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk
+
= Overview =
−
=== Sensing and Actuating for Tasking Event-B ===
+
The Rodin platform versions concerned by this deliverable are:
−
Sensing and actuating events, and an Environ Machine have been added to allow simulation of the environment and implementation using memory mapped IO.
+
* 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 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).
  
−
A new case study has been produced that makes use of these new features, details available at http://wiki.event-b.org/index.php/Event-B_Examples
+
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 example/tutorial projects, and also and a Bundled Windows version, are available in the [http://deploy-eprints.ecs.soton.ac.uk/304/ Deploy E-Prints archive].  
+
* Core platform maintenance (Thomas Muller)
 +
According to the previously mentionned refocus, the maintenance tasks performed on the core plateform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The performance was enhanced by core implementation and user interface refactorings. The proving usability was enhanced by the possibility to customize, combine, and parameterize tactics and the addition of new inference and rewriting rules.
  
−
The projects are also available from the [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/HeatingController_Tutorial_v0.1.4/ Examples SVN site].
+
* {{TODO}} An overview of the contribution about Mathematical extensions / Theory Plug-in (Issam Maamria)
  
−
Sources for Tasking Event-B and Code Generators are available from a branch on the [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/branches/CodeGeneration/0.1.4 Rodin SVN site].
+
* {{TODO}} An overview of the contribution about Plug-in Incompatibilities (All partners)
  
−
=== The Code Generation Demonstrator for Rodin 2.1.x ===
+
* {{TODO}} An overview of the contribution about Modularisation (Alexei Illiasov)
  
−
Released 24 January 2011.
+
* {{TODO}} An overview of the contribution about Decomposition (Renato Silva)
  
−
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
+
* {{TODO}} An overview of the contribution about Team-based Development (Colin Snook, Vitaly Savicks)
  
−
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
+
* {{TODO}} An overview of the contribution about UML-B (Colin Snook, Vitaly Savicks)
  
−
The update-site is available through the Rodin update site in the ''Utilities'' category.
+
* {{TODO}} An overview of the contribution about ProR (Michael Jastram)
  
−
The code generation tutorial examples are available for download at:
+
= Motivations =
 +
The DEPLOY partners raised issues that appeared mandatory to address by the end of the project. The tasks to solve these issues have been listed and grouped according to their priority. This grouping appears below. 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. 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.
  
−
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
+
{{SimpleHeader}}
 +
|-
 +
! scope=col | Group 1 (highest priority) || Responsible
 +
|-
 +
|Performance <br /> - Core (large models, etc.) <br /> - GUI (incl. prover UI, edition, etc.) || Systerel
 +
|-
 +
|Prover Performances <br /> - New rewriting rules / inference rules <br /> - Automatic tactics (preferences, timeout, etc.) || Systerel
 +
|-
 +
|ProB Disprover (incl. counter examples to DLF POs) || Düsseldorf
 +
|-
 +
|Stability (crash, corruption, etc.)  || Systerel
 +
|-
 +
|Editors || Systerel/Düsseldorf
 +
|-
 +
|}
 +
{{SimpleHeader}}
 +
|-
 +
! scope=col | Group 2 || Responsible
 +
|-
 +
| Prover Performances <br /> - SMT provers integration <br /> - connection with Isabelle  <br /> - Mathematical extensions <br /> - ProB || <br />Systerel <br /> ETH Zurich <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 Zurich/Southampton
 +
|-
 +
|Code Generation || Southampton
 +
|}
 +
{{SimpleHeader}}
 +
|-
 +
! scope=col | Group 4
 +
|-
 +
|Prover Integrity
 +
|-
 +
|Integrity of Code Generation
 +
|}
 +
== Platform maintenance ==
 +
The platform maintenance, as it can be deduced from the above tables, concerned stability and performance improvement. The prover performance improvement will be discussed and detailed in a separate chapter. SYSTEREL found out, from early investigation on performance, a relation of cause and effect between perfomance loss and various reported bugs, such as "platform hanging" bugs or "no more handles" bugs related to Windows platforms.
  
−
The code generation plug-in relies on the Epsilon tool suite. Install Epsilon manually, since the automatic install utility does not seem to work for this feature. We currently use the Epsilon interim update site available at:
+
== 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''
  
−
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
+
= Choices / Decisions =
 +
== Platform maintenance ==
 +
{{TODO}} ''To be completed by Thomas Muller''
 +
== 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''
  
−
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
= 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>.
  
−
== Code Generation Status ==
+
*{{TODO}}  Links for Mathematical extensions / Theory Plug-in
−
=== Latest Developments ===
+
*{{TODO}}  Links for Plug-in Incompatibilities
−
* Demonstrator plug-in feature version 0.1.0
+
*{{TODO}}  Links for Modularisation
−
** for Rodin 2.1.x version is available.
+
*{{TODO}}  Links for Decomposition
 +
*{{TODO}}  Links for Team-based Development
 +
*{{TODO}}  Links for UML-B
 +
*{{TODO}}  Links for ProR
  
−
* The Code Generation feature consists of,
+
= Status =
−
** a tasking Development Generator.
+
== Platform maintenance ==
−
** a tasking Development Editor (Based on an EMF Tree Editor).
+
By the end of the project, there are :
−
** a translator, from Tasking Development to Common Language Model (IL1).
+
* xx bugs reported and open. All with a priority lower or equal to 5.
−
** a translator, from the Tasking Development to Event-B model of the implementation.
+
* xx feature requests expressed and still open.
−
** a pretty-printer for the Tasking Development.
 
−
** a pretty-printer for Common Language Model, which generates Ada Source Code.
 
  
−
* A tutorial is available [[Code Generation Tutorial]]
+
== Mathematical extensions / Theory Plug-in ==
−
** Step 1 - Create the tasking development.
+
{{TODO}} ''To be completed by Issam Maamria''
−
** Step 2 - Add annotations.
+
== Plug-in Incompatibilities ==
−
** Step 3 - Invoke translators.
+
{{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''
  
−
=== Ongoing Work ===
 
  
−
* Full Rodin Integration
+
= References =
−
* Sensed Variables
+
<references/>
−
* Branching in Shared Machines
 
  
−
=== Future Work ===
+
[[Category:D45 Deliverable]]
−
* Support for Interrupts.
 
−
* Richer DataTypes.
 
−
* Accommodation of duplicate event names in tasking developments.
 
−
 
 
−
== Metamodels ==
 
−
* In the plug-in we define several meta-models:
 
−
** CompositeControl: for the control flow (algorithmic) constructs such as branch, loop and sequence etc. These constructs may be used in the specification of either  sequential or concurrent systems.
 
−
** Tasking Meta-model: defines the tasking model where we attach tasking specific details, such as task priority, task type. The tasking structures provide the ability to define single tasking or multi-tasking (concurrent) systems. We make use of the composite control plug-in to specify the flow of control.
 
−
** Common Language (IL1) Meta-model: defines an abstraction of common programming language constructs for use in translations to implementations.
 
−
 
 
−
== Translation Rules ==
 
−
* Tasking to IL1/Event-B translation rules [[http://wiki.event-b.org/images/Translation.pdf]]
 
−
 
 
−
== Release History ==
 
−
=== The Code Generation Demonstrator for Rodin 1.3.x ===
 
−
 
 
−
 
 
−
First release: 30 November 2010.
 
−
 
 
−
available from:
 
−
 
 
−
https://sourceforge.net/projects/codegenerationd/files/
 
−
 
 
−
The zip file contains a windows XP bundle, and a Windows V7 bundle. Alternatively, if you wish to build using an update-site, this is also included in the zip file, along with some notes on installation. However, note that the demonstrator tool is only compatible with Rodin 1.3.
 
−
 
 
−
A simple shared buffer example is provided. This will form the basis of a tutorial (which is work in progress). The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code Generation plug-ins, together with a patch plug-in. The patch plug-in is required to correct an inconsistency in the org.eventb.emf.persistence plug-in. For the bundles, simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed - the only configuration necessary may be to switch workspace to ''<installPath>\rodin1.3bWin7\workspace''. When using the update-site the example projects, and the project forming the basis of a simple tutorial, are provided in the accompanying zip file. These should be imported manually.
 
−
 
 
−
Mac users - no bundled version available at present, but use the update site in the 'advanced' folder.
 
−
 
 
−
'''A step-by-step [[Code Generation Tutorial]] is available'''
 
−
 
 
−
==== About the Initial Release ====
 
−
The Code Generation (CG) Feature in the initial release is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, therefore, there will be a heavy reliance on docs and dialogue to facilitate exploration of the tools and concepts.
 
−
 
 
−
==== Source Code ====
 
−
 
 
−
The sources are available from,
 
−
 
 
−
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
 
−
 
 
−
Note - I used Eclipse 3.5 Galileo, and you will need to install (or have sources from) Epsilon's interim update site. There is also dependency on Camille v2.0.0
 
−
 
 
−
 
 
−
 
 
−
[[Category:Work in progress]]
 

Revision as of 11:02, 16 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 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.

  • Core platform maintenance (Thomas Muller)

According to the previously mentionned refocus, the maintenance tasks performed on the core plateform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The performance was enhanced by core implementation and user interface refactorings. The proving usability was enhanced by the possibility to customize, combine, and parameterize tactics and the addition of new inference and rewriting rules.

  • 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 DEPLOY partners raised issues that appeared mandatory to address by the end of the project. The tasks to solve these issues have been listed and grouped according to their priority. This grouping appears below. 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. 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 Zurich
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 Zurich/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, concerned stability and performance improvement. The prover performance improvement will be discussed and detailed in a separate chapter. SYSTEREL found out, from early investigation on performance, a relation of cause and effect between perfomance loss and various reported bugs, such as "platform hanging" bugs or "no more handles" bugs related to Windows platforms.

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

TODO To be completed by Thomas Muller

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[2].
  • Bugs[3].
  • Feature requests[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

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. ↑ http://wiki.event-b.org/index.php/Rodin_Platform_Releases
  3. ↑ https://sourceforge.net/tracker/?group_id=108850&atid=651669
  4. ↑ https://sourceforge.net/tracker/?group_id=108850&atid=651672
Retrieved from ‘https://wiki.event-b.org/index.php?title=Code_Generation_Activity&oldid=2784’