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

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Pascal
 
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 purpose of the platform corrective and evolutive maintenance is to address bugs and feature requests.
Version 0.1.5. Sensing and actuating events, and an Environ Machine have been added to allow simulation of the environment and implementation using memory mapped IO.
 
  
Available from the Rodin Update Site in the Utilities Category.
+
The outstanding new features in the main platform for the past year are listed below:
 +
* Mathematical Language V2 (releases 1.0 and upper)
 +
: The new version of the mathematical language is supported.
 +
: See [http://wiki.event-b.org/index.php/Event-B_Mathematical_Language http://wiki.event-b.org/index.php/Event-B_Mathematical_Language].
 +
* Theorems everywhere (releases 1.0 and upper)
 +
: It is possible to mix theorems and regular predicates in axioms, invariants and guards.
 +
* Auto-completion (releases 1.0 and upper)
 +
: When entering a predicate or expression in the Event-B machine / context editor, it is possible to type <tt>C-Space</tt> to see a list of possible identifiers that could be entered at the cursor position.
 +
* Entering mathematical symbols (releases 1.1 and upper)
 +
: The Rodin platform provides many more ways to enter mathematical symbols:
 +
: - either type the ASCII shortcut (as in previous releases),
 +
: - or type the LaTeX command (as defined in style <tt>bsymb</tt>),
 +
: - or click in the ''Symbol Table'' view which displays the symbols graphically,
 +
: - or directly enter the Unicode value of the symbol (for advanced users).
 +
: See [http://wiki.event-b.org/index.php/Rodin_Keyboard http://wiki.event-b.org/index.php/Rodin_Keyboard].
 +
* Camille Text Editor (releases 1.0 and upper)
 +
: See [http://wiki.event-b.org/index.php/Text_Editor http://wiki.event-b.org/index.php/Text_Editor].
  
As in previous releases, the code generation plug-in relies on the Epsilon tool suite. Add the following Epsilon interim update site to the list of available update sites in the Eclipse menu ''help/install new software'': http://download.eclipse.org/modeling/gmt/epsilon/interim/
+
See the [[#Available%20Documentation | Release Notes]] and the [[#Available%20Documentation | SourceForge]] databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
  
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
= Motivations =
 +
The main evolutions of the Rodin platform are driven by the description of work for the DEPLOY project and the requirements expressed by industrial WP1 to WP5 partners or by consultants during the lifecycle of the project.
  
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
+
Beyond that, any user registered on SourceForge may record any encountered bug on the Rodin platform or request a new feature, using the dedicated [[#Available documentation | trackers]]. Depending on the category, the bug / feature is assigned to the WP9 partner who is in charge of its treatment:
 +
{{SimpleHeader}}
 +
|-
 +
! scope=col | Category || Partner
 +
|-
 +
|AnimB || Christophe METAYER
 +
|-
 +
|B2LaTeX || University of Southampton
 +
|-
 +
|Decomposition || Systerel
 +
|-
 +
|Event-B core || Systerel
 +
|-
 +
|Event-B interface || Systerel
 +
|-
 +
|Event-B POG || Systerel
 +
|-
 +
|Event-B provers || Systerel
 +
|-
 +
|Event-B static checker || Systerel
 +
|-
 +
|PRO-B || Dusseldorf
 +
|-
 +
|Renaming || University of Southampton
 +
|-
 +
|Requirements || Dusseldorf
 +
|-
 +
|Rodin platform || Systerel
 +
|-
 +
|Text editor || Dusseldorf
 +
|-
 +
|U2B || Southampton
 +
|}
  
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].  
+
The priorities are discussed during the WP9 meetings.
  
The projects are also available from the [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/HeatingController_Tutorial_v0.1.4/ Examples SVN site].
+
= Choices / Decisions =
 +
The WP9 partners have agreed on a release policy (see the [[#Available%20Documentation | Rodin Platform Releases]] wiki page). In particular, a new version of the Rodin platform is released every 3 months, a wiki page is dedicated to each release, and the code is frozen during the 2 weeks preceding each release.
  
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/trunk/CodeGeneration Rodin SVN site].
+
The main advantages, for both developers and end-users, are summarized below:
 +
* Information. The wiki page dedicated to each release provides instant information on the new features and improvements, which may be discussed if necessary.
 +
* Validation. The period of code freeze is more especially devoted to bug fixes, and the frequency of the stable releases is ensured.
 +
* Integration. A synchronization between the optional plug-ins and other plug-ins is now possible.
  
=== The Code Generation Demonstrator for Rodin 2.1.x ===
+
= Available Documentation =
 +
The following pages give useful information about the Rodin platform releases:
 +
* Release notes.
 +
: See [http://wiki.event-b.org/index.php/Rodin_Platform_Releases http://wiki.event-b.org/index.php/Rodin_Platform_Releases].
 +
: More details are provided in the notes distributed with each release (eg. [http://sourceforge.net/project/shownotes.php?release_id=693928 http://sourceforge.net/project/shownotes.php?release_id=693928]).
 +
* Bugs.
 +
: See [http://sourceforge.net/tracker/?atid=651669&group_id=108850 http://sourceforge.net/tracker/?group_id=108850&atid=651669].
 +
* Feature requests.
 +
: See [http://sourceforge.net/tracker/?group_id=108850&atid=651672 http://sourceforge.net/tracker/?group_id=108850&atid=651672].
  
Released 24 January 2011.
+
= Planning =
 +
The [[#Available%20Documentation | Rodin Platform Releases]] wiki page lists in particular the upcoming releases and give the scheduled release dates.
  
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
+
Special efforts will be made on the following topics:
 +
* Team-based development.
 +
: The purpose is to perform simultaneous developments.
 +
: In order to understand the problem properly, some usage scenarios (see [http://wiki.event-b.org/index.php/Scenarios_for_Team-based_Development http://wiki.event-b.org/index.php/Scenarios_for_Team-based_Development]) for team-based Development have already been written, and a page has also been started to express merging proofs scenarios (see [http://wiki.event-b.org/index.php/Scenarios_for_Merging_Proofs http://wiki.event-b.org/index.php/Scenarios_for_Merging_Proofs]).
 +
: A prototype plug-in is available, which enables the use of the EMF compare editor for machines and contexts. The DEPLOY partners will try out this plug-in and gather requirements for the teamwork plug-in.
 +
: See [http://wiki.event-b.org/index.php/EMF_Compare_Editor_Investigation http://wiki.event-b.org/index.php/EMF_Compare_Editor_Investigation] (Implementation issues).
 +
: See [http://wiki.event-b.org/index.php/EMF_Compare_Editor_installation http://wiki.event-b.org/index.php/EMF_Compare_Editor_installation] (How to install the EMF Compare editor).
 +
: See [http://wiki.event-b.org/index.php/Teamwork_Requirements http://wiki.event-b.org/index.php/Teamwork_Requirements] (Feedback page / Requirements).
  
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
+
* Documentation.
 +
: The purpose is to continuously increase the available documentation on the Wiki. It may contains requirements, pre-studies (states of the art, proposals, discussions), technical details (specifications), teaching materials (tutorials), user's guides, etc. The intended audience may be the developers or the end-users.
  
The update-site is available through the Rodin update site in the ''Utilities'' category.
+
[[Category:D23 Deliverable]]
 
 
The code generation tutorial examples are available for download at:
 
 
 
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
 
 
 
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:
 
 
 
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
 
 
 
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
 
 
 
== Code Generation Status ==
 
=== Latest Developments ===
 
* Demonstrator plug-in feature version 0.1.0
 
** for Rodin 2.1.x version is available.
 
 
 
* The Code Generation feature 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.
 
 
 
* A tutorial is available [[Code Generation Tutorial]]
 
** Step 1 - Create the tasking development.
 
** Step 2 - Add annotations.
 
** Step 3 - Invoke translators.
 
 
 
=== Ongoing Work ===
 
 
 
* Full Rodin Integration
 
* Sensed Variables
 
* Branching in Shared Machines
 
 
 
=== Future Work ===
 
* 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 09:30, 16 November 2009

Overview

The purpose of the platform corrective and evolutive maintenance is to address bugs and feature requests.

The outstanding new features in the main platform for the past year are listed below:

  • Mathematical Language V2 (releases 1.0 and upper)
The new version of the mathematical language is supported.
See http://wiki.event-b.org/index.php/Event-B_Mathematical_Language.
  • Theorems everywhere (releases 1.0 and upper)
It is possible to mix theorems and regular predicates in axioms, invariants and guards.
  • Auto-completion (releases 1.0 and upper)
When entering a predicate or expression in the Event-B machine / context editor, it is possible to type C-Space to see a list of possible identifiers that could be entered at the cursor position.
  • Entering mathematical symbols (releases 1.1 and upper)
The Rodin platform provides many more ways to enter mathematical symbols:
- either type the ASCII shortcut (as in previous releases),
- or type the LaTeX command (as defined in style bsymb),
- or click in the Symbol Table view which displays the symbols graphically,
- or directly enter the Unicode value of the symbol (for advanced users).
See http://wiki.event-b.org/index.php/Rodin_Keyboard.
  • Camille Text Editor (releases 1.0 and upper)
See http://wiki.event-b.org/index.php/Text_Editor.

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

Motivations

The main evolutions of the Rodin platform are driven by the description of work for the DEPLOY project and the requirements expressed by industrial WP1 to WP5 partners or by consultants during the lifecycle of the project.

Beyond that, any user registered on SourceForge may record any encountered bug on the Rodin platform or request a new feature, using the dedicated trackers. Depending on the category, the bug / feature is assigned to the WP9 partner who is in charge of its treatment:

Category Partner
AnimB Christophe METAYER
B2LaTeX University of Southampton
Decomposition Systerel
Event-B core Systerel
Event-B interface Systerel
Event-B POG Systerel
Event-B provers Systerel
Event-B static checker Systerel
PRO-B Dusseldorf
Renaming University of Southampton
Requirements Dusseldorf
Rodin platform Systerel
Text editor Dusseldorf
U2B Southampton

The priorities are discussed during the WP9 meetings.

Choices / Decisions

The WP9 partners have agreed on a release policy (see the Rodin Platform Releases wiki page). In particular, a new version of the Rodin platform is released every 3 months, a wiki page is dedicated to each release, and the code is frozen during the 2 weeks preceding each release.

The main advantages, for both developers and end-users, are summarized below:

  • Information. The wiki page dedicated to each release provides instant information on the new features and improvements, which may be discussed if necessary.
  • Validation. The period of code freeze is more especially devoted to bug fixes, and the frequency of the stable releases is ensured.
  • Integration. A synchronization between the optional plug-ins and other plug-ins is now possible.

Available Documentation

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

  • Release notes.
See http://wiki.event-b.org/index.php/Rodin_Platform_Releases.
More details are provided in the notes distributed with each release (eg. http://sourceforge.net/project/shownotes.php?release_id=693928).
  • Bugs.
See http://sourceforge.net/tracker/?group_id=108850&atid=651669.
  • Feature requests.
See http://sourceforge.net/tracker/?group_id=108850&atid=651672.

Planning

The Rodin Platform Releases wiki page lists in particular the upcoming releases and give the scheduled release dates.

Special efforts will be made on the following topics:

  • Team-based development.
The purpose is to perform simultaneous developments.
In order to understand the problem properly, some usage scenarios (see http://wiki.event-b.org/index.php/Scenarios_for_Team-based_Development) for team-based Development have already been written, and a page has also been started to express merging proofs scenarios (see http://wiki.event-b.org/index.php/Scenarios_for_Merging_Proofs).
A prototype plug-in is available, which enables the use of the EMF compare editor for machines and contexts. The DEPLOY partners will try out this plug-in and gather requirements for the teamwork plug-in.
See http://wiki.event-b.org/index.php/EMF_Compare_Editor_Investigation (Implementation issues).
See http://wiki.event-b.org/index.php/EMF_Compare_Editor_installation (How to install the EMF Compare editor).
See http://wiki.event-b.org/index.php/Teamwork_Requirements (Feedback page / Requirements).
  • Documentation.
The purpose is to continuously increase the available documentation on the Wiki. It may contains requirements, pre-studies (states of the art, proposals, discussions), technical details (specifications), teaching materials (tutorials), user's guides, etc. The intended audience may be the developers or the end-users.