Difference between pages "Code Generation Activity" and "D32 Mathematical Extensions"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Nicolas
 
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 ===
 
−
Sensing and actuating events, and an Environ Machine have been added to allow simulation of the environment and implementation using memory mapped IO.
 
  
−
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
+
Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language, by defining his own mathematical operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (prover extensions).
  
−
The example/tutorial projects, and also and a Bundled Windows version, are available in the [http://deploy-eprints.ecs.soton.ac.uk/304/ e-prints archive].  
+
A theory is a file that gathers of new algebraic types, new operators/predicates and new proof rules. It is developed in the Rodin workspace. When it is complete, the user makes it available to his models (this action is called the deployment of a theory). He can then start using his own operators, datatypes and proof rules for the development of his models.
  
−
The projects are also available from the [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/HeatingController_Tutorial_v0.1.4/ Examples SVN site].
+
=== Motivations ===
  
−
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].
 
  
−
=== The Code Generation Demonstrator for Rodin 2.1.x ===
 
  
−
Released 24 January 2011.
+
This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.
  
−
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
 
  
−
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
 
  
−
The update-site is available through the Rodin update site in the ''Utilities'' category.
+
=== Choices / Decisions ===
  
−
The code generation tutorial examples are available for download at:
+
On the Core Rodin Platform side, implementing mathematical extensions required to make some parts of the code extensible, that were not designed to be so, namely the lexer and the parser. We were using tools that automatically generated them from a fixed grammar description, so we had to change to other technologies. A [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser study] has been made on available technologies. The Pratt algorithm was selected for its adequation with the purpose and it did not have the drawbacks of other technologies:
 +
* foreign language integration
 +
* overhead due to over generality
  
−
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
+
After a mocking up phase to verify feasibility, the Pratt algorithm has been confirmed as the chosen option and implemented in the Rodin Platform.
  
−
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:
+
Besides, we wanted to set up a way to publish and share theories for Rodin users, in order to constitute a database of pre-built theories for everyone to use and contribute. This has been realised by adding a new tracker on SourceForge site ([http://sourceforge.net/tracker/?group_id=108850&atid=1558661]).
  
−
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
+
=== Available Documentation ===
  
−
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
{{TODO|add pdf mathextn from BSCW}}
  
−
== Code Generation Status ==
+
* Requirements.
−
=== Latest Developments ===
+
* Pre-studies (states of the art, proposals, discussions).
−
* Demonstrator plug-in feature version 0.1.0
+
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser#Design_Alternatives]
−
** for Rodin 2.1.x version is available.
+
* Technical details (specifications).
 +
** [http://wiki.event-b.org/index.php/Mathematical_Extensions]
 +
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Lexer]
 +
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser]
 +
** [http://wiki.event-b.org/index.php/Theory_Plug-in]
 +
* Teaching materials (tutorials).
 +
* User's guides.  
 +
** [http://wiki.event-b.org/images/Theory_UM.pdf]
  
−
* The Code Generation feature consists of,
+
=== Planning ===
−
** a tasking Development Generator.
+
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
−
** 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]]
+
[[Category:D32 Deliverable]]
−
** 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:58, 23 November 2010

Overview

Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language, by defining his own mathematical operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (prover extensions).

A theory is a file that gathers of new algebraic types, new operators/predicates and new proof rules. It is developed in the Rodin workspace. When it is complete, the user makes it available to his models (this action is called the deployment of a theory). He can then start using his own operators, datatypes and proof rules for the development of his models.

Motivations

This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.


Choices / Decisions

On the Core Rodin Platform side, implementing mathematical extensions required to make some parts of the code extensible, that were not designed to be so, namely the lexer and the parser. We were using tools that automatically generated them from a fixed grammar description, so we had to change to other technologies. A study has been made on available technologies. The Pratt algorithm was selected for its adequation with the purpose and it did not have the drawbacks of other technologies:

  • foreign language integration
  • overhead due to over generality

After a mocking up phase to verify feasibility, the Pratt algorithm has been confirmed as the chosen option and implemented in the Rodin Platform.

Besides, we wanted to set up a way to publish and share theories for Rodin users, in order to constitute a database of pre-built theories for everyone to use and contribute. This has been realised by adding a new tracker on SourceForge site ([1]).

Available Documentation

TODO: add pdf mathextn from BSCW

  • Requirements.
  • Pre-studies (states of the art, proposals, discussions).
  • Technical details (specifications).
  • Teaching materials (tutorials).
  • User's guides.

Planning

This paragraph shall give a timeline and current status (as of 28 Jan 2011).

Retrieved from ‘https://wiki.event-b.org/index.php?title=Code_Generation_Activity&oldid=2452’