Difference between pages "ADVANCE D3.2 General Platform Maintenance" and "Code Generation Activity"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
 
imported>Andy
 
Line 1: Line 1:
−
This part concerns the general maintenance performed on the Rodin toolset within the first ten months of the ADVANCE project. As the maintenance is a task that concerns the whole toolset, and to ease the reading of this part of the deliverable, the maintenance section has been decomposed in a list of subsections corresponding to scopes of the toolset. These sections are: core Rodin platform, UML-B improvements, code generation, ProR and Camille. All these subsections maintain the template previously defined in the introduction.
+
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, or Chris Lovell mailto:cjl3@ecs.soton.ac.uk
  
−
= Core Rodin platform =
 
  
−
== Overview ==
 
−
The Rodin platform versions concerned by this deliverable are:
 
−
* 2.4 (released on 31.01.2012),
 
−
* 2.5 (released on 02.05.2012),
 
−
* 2.6 (released on 31.07.2012).
 
  
−
The core Rodin platform maintenance task focused on fixing the identified bugs and mitigating usability issues. During DEPLOY, many features and contributions were added to the toolset as users wishes and requests were collected along. At the same time, the Event-B models and proof got bigger and bigger, in the same way as the experience of the users involved constantly increased ergo the size of the systems they modelled. Scalability issues occured at some point when feature addition was favoured to design refactorings. As the DEPLOY project was nearing its end, it appeared mandatory for the development team, to address the specific bugs and issues reported by the DEPLOY partners and related to scalability or usability, and wished resolved by the end of the project. The various tasks to be performed were scheduled, prioritized and regularly updated during bi-weekly teleconferences.
+
== Code Generation Feature - Version 0.2.3 For Rodin 2.5==
 +
A new release of the tool is imminent.
  
−
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).
+
The main new features are:
−
Release Notes<ref name="relNotes">http://wiki.event-b.org/index.php/Rodin_Platform_Releases</ref> and the SourceForge trackers<ref>http://sourceforge.net/projects/rodin-b-sharp/</ref> (bugs and feature requests) are available for more details about the previous and upcoming releases of the Rodin platform.
 
  
−
== Motivations / Decisions ==
+
* Code generation from [http://wiki.event-b.org/index.php/State-Machines_and_Code_Generation state-machine] diagrams.
−
'''Provide 64-bit versions of the Rodin platform on Linux and Windows systems'''<br>
+
* Improved static checking.
−
End users asked the Rodin team to provide 32-bit and 64-bit versions of the Rodin platform for Linux and Windows operating systems. Before Rodin 2.4, the only 64-bit version of Rodin was available on Mac platforms as 32-bit Mac (early 2006) platforms are no longer maintained by Apple. The motivation that would push forward 64-bit architectures is the possibility to increase the available java heap size which is, for example, extensively used during the automated proof. After a phase of testing and despite the drawbacks of assembling and maintaining five platforms instead of three, Linux and Windows 64-bit as well as 32-bit platforms are now systematically made available since the Rodin 2.4 release.
 
  
−
'''The Rodin Editor in the Rodin core platform'''<br>
+
We have also provided some details of the [http://wiki.event-b.org/index.php/The_Use_of_Theories_in_Code_Generation use of Theories in code generation], from the previous version.
−
According to its role in the Rodin toolset, and its stabilization, the Rodin Editor,<ref>http://wiki.event-b.org/index.php/Rodin_Editor</ref> has been integrated into the core platform since Rodin release 2.4.
 
  
−
== Available Documentation ==
+
Updated Examples etc. are available:
−
The release notes, that appear and are maintained on the wiki, and that accompany each release, give useful information about the Rodin platforms. Moreover, two web trackers list and detail the known bugs and open feature requests:
+
−
* a sourceforge bug tracker,<ref>http://sourceforge.net/tracker/?group_id=108850&atid=651669</ref>
+
* Tutorial, and example, projects are available from the Examples directory: [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/v0.2.3/ SVN].
−
* a sourceforge feature requests tracker.<ref>http://sourceforge.net/tracker/?group_id=108850&atid=651672</ref>
+
* Test projects are also available from the Examples directory [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/v0.2.3/Tests SVN].
−
The Event-B wiki,<ref name="rodinWiki">http://wiki.event-b.org/</ref> basic source of documentation for the users and developers of the Rodin toolset, was completed by the Rodin handbook, an ultimate source of documentation which reached completion by the end of the DEPLOY project. The handbook aimed to overcome the lack of a centralized source of information providing the necessary assistance to an engineer in the need to be productive using Event-B and minimize the access to an expert user. It is continuously maintained by the various actors involved in the environment of the Rodin toolset and is available as a PDF version, a HTML version, and help contents within Rodin. Both the Rodin handbook and the Event-B wiki represent the main source of documentation about Event-B and the Rodin toolset.
+
* Sources (will be) available at: [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration SVN]
−
Finally, a channel has been created on Youtube, in order to provide video tutorials about the use of the platform.<ref>http://www.youtube.com/user/EventBTv</ref>
+
* Example Theories at: [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/TheoriesForCG SVN]
 +
 
 +
== Code Generation Feature - Version 0.2.2 For Rodin 2.4==
 +
 
 +
We released V0.2.2 on 22-03-2012. The main changes, to the interface, and translation from theories are described below:
 +
 
 +
* Tasking Event-B is now integrated with the Event-B Editors.
 +
* We have the ability to translate to C, Java, etc. in addition to Ada source code.
 +
* We use theories to define translations of the Event-B mathematical language (Theories for Ada, Java and C are supplied).
 +
* We use the theory plug-in as a mechanism for defining new data types , and the translations to target data types.
 +
* The translator is extensible.
 +
* Minimal use is made of the EMF tree editor in Rose.
 +
 
 +
To install v0.2.2:
 +
 
 +
* Access the main Rodin Update Site. In Eclispe click on Help/Install new Software. Find the Rodin update site from the list. In Utilities add Code Generation.
 +
The approach makes use of the following, which should be installed if the features are required by the user for editing:
 +
*Model Decomposition: Download from the main Rodin Update Site, in the Decomposition section.
 +
*Shared Event Composition: Download from the main Rodin Update Site, in the Decomposition section.
 +
*Theory Plug-in: Download from the main Rodin Update Site, in the Modelling Extensions section.
  
−
== Planning ==
+
Examples available at:
−
Two releases of the core platform have been scheduled after Rodin 2.6 has been published: Rodin 2.7 followed by Rodin 3.0. Rodin 2.7 is intended to be released by the end of October 2012, and Rodin 3.0 will be available by the end of January 2013. Rodin 2.7 will be corrective. It has been scheduled to respect the 3 monthly release policy, as the Rodin 3.0 version will require more that 3 months of development. In addition, Rodin 2.7 will integrate the Theory plug-in (which is currently separate).
+
 +
* Tutorial, and example, projects are available from the Examples directory: [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/v0.2.2/ SVN].
 +
* Test projects are also available from the Examples directory [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/v0.2.2/CG_v0.2.2_Tests SVN].
 +
* Sources at: [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration SVN]
 +
* Example Theories at: [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/TheoriesForCG SVN]
  
−
Indeed, version 3.0 of the platform is being prepared since Rodin 2.6, and will include lots of refactoring and evolutions in the published programming interfaces (API). Here is a non exhaustive list of the main improvements and refactorings that will be part of it:
+
== Code Generation Feature - Version 0.2.1 For Rodin 2.3==
−
*Binders will be allowed in extensions.
+
Contains Bug Fixes for previous release. 14-12-2011
−
*The platform will be based on Eclipse 4.
 
−
*The AST will be made stronger.
 
−
*The sequent prover will be enhanced.
 
−
*Parent-child element relationship extension points will be moved from the UI plug-in to the EventB core plug-in.
 
−
*The Event-B keyboard plug-in will be refactored to separate the UI code from the ASCII/Math translation mechanism.
 
−
*The statistics view will be refactored to handle other kinds of component files (currently just Contexts and Machines are supported).
 
  
−
= UML-B Improvements =
+
== Code Generation Feature - Version 0.2.0 For Rodin 2.3==
 +
We released a new version of the code generator on 30-11-2011, and updated documentation.
 +
===== Changes to the Tooling and Approach =====
 +
The main changes are:
 +
* The code generators have been completely re-written. The translators are now implemented in Java, i.e. there is no longer a dependence on the Epsilon tool set. This was undertaken for code maintenance reasons.
 +
* Tasking Event-B is now integrated with the Event-B explorer.
 +
* The Rose Editor is used for editing the Tasking Event-B, and
 +
* a text-based editor is provided, using the Rose extension, for editing the TaskBody. This feature has been added to address some of the usability concerns. It also overcomes the 'problem' experienced with duplicate event names in a development, since the parser-builder that has been implemented automatically selects the correct event.
 +
* The EMF tree editor in Rose is only used minimally; we plan enhancements to further reduce its use.
 +
* Composed machines are used to store event 'synchronizations'; these are generated automatically during the decomposition process. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events.
 +
* The code generation approach is now extensible; new target language constructs can be added using the Eclipse extension mechanism.
 +
* The translation of target's mathematical language is now specified in the theory plug-in. This improves clarity since the the translation from source to target is achieved by specifying pattern matching rules. Extensibility is also improved; the theory plug-in is used to specify new data-types, and how they are implemented.
 +
* Translated code is deposited in a directory in the appropriate files. An Ada project file is generated for use with AdaCore's GPS workbench. Eventually this could be enabled/disabled in a preferences dialog box.
 +
* The Tasking Event-B to Event-B translator is now properly integrated. Control variable updates to the Event-B model are made in a similar way to the equivalent updates in the state-machine plug-in. The additional elements are added to the Event-B model and marked as 'generated'. This prevents users from manually modifying them, and allows them to be removed through a menu choice.
  
−
== Overview ==
+
===== Changes to the Documentation =====
 +
The following Pages have been updated:
 +
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Overview Tasking Event-B Overview]
 +
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Tutorial Tutorial]
  
−
The UML-B plug-in and associated frameworks are developed and maintained by Dr Colin Snook at the University of Southampton. Significant contributions (to the latest version) have been made by Vitaly Savicks (state-machines) and Gintautas Sulskus (Class Diagrams). The UML-B plugin provides UML-like diagrammatic modelling as an extension to Event-B and the Rodin platform. UML-B is an established plug-in which will be developed and improved to support the aims of the ADVANCE project. UML-B was redeveloped during the DEPLOY project to provide closer integration with Event-B. A state-machine diagram editor is already released in this integrated version and a class diagram editor is now being developed as a prototype.
+
TODO
−
[[Image:Umlb_cap2.jpg|center|A UML-B state machine and its Event-B counterpart]]
+
* Add addressed variables (for direct read/write access to memory)
−
Other improvements will include new diagrammatic notations which are directly related to the aims of ADVANCE, such as component diagrams, as well as more general improvements, such as usability, and any features required by the projects industrial partners.
+
* Flattening of composed machines/implementation machines.
 +
* Interrupts
  
−
== Motivations / Decisions ==
+
=== Sensing and Actuating for Tasking Event-B ===
 +
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.
  
−
The implementation of the UML-B tool is structured to provide re-usable features as much as possible. To achieve this, wherever possible, generic frameworks are developed and the implementation of specific diagram tools is minimised by utilising these frameworks. The following frameworks are now in use by UML-B and available as a basis for future diagrammatic modelling notations.
+
* The new v0.1.5 feature is available from the Rodin Update Site, it resides in the Utilities Category.
  
−
* The ''Event-B EMF framework'' provides an EMF basis for Event-B models (developed during the DEPLOY project). Indeed, it provides an EMF representation of Event-B models with persistence into the Rodin database.
+
* 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/
−
* The ''Event-B EMF Support for Modelling Extensions framework'' provides support for extending Event-B with new modelling features (initially developed during the DEPLOY project and now being extended in the ADVANCE project). It provides Navigator support for EMF-only model elements, a persistence mechanism for model extensions that are not needed to be processed by Rodin and a Generic Refiner for modelling extensions (which has recently been added).
+
 
−
* ''The Event-B GMF Diagrams Generic Support framework'' provides support for developing new diagram notations (started in the DEPLOY project but mostly developed during the ADVANCE project). It provides generic support for diagrammatic aspects of modelling extensions, and a generic validation and Event-B generation service (which has recently been added).
+
* Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
−
+
 
−
A new release of the state-machine diagram editor has been made. This release corrected some problems and improved use of the generic framework features.
+
A new [http://wiki.event-b.org/index.php?title=Tasking_Event-B_Tutorial Code Generation Tutorial] has been produced, that makes use of these new features. There is an explanation of the heating controller, upon which it is based, [http://wiki.event-b.org/index.php/Development_of_a_Heating_Controller_System here].
  
−
Work is in progress on a new version of the UML-B Class Diagram editor. This takes the same approach as the state-machines editor in that the models are contained within machines (and, in this case, also contexts) and that diagrammatic model features link to and enhance existing Event-B elements rather than generate everything. The Class diagram editor is currently a prototype and has not been released.
+
The example/tutorial projects, and also and a Bundled Windows 7 version, are available in the [http://deploy-eprints.ecs.soton.ac.uk/304/ Deploy E-Prints archive] or [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/HeatingController_Tutorial_v0.1.4/ Examples SVN site].
  
−
== Available Documentation ==
+
== The Code Generation Demonstrator for Rodin 2.1.x ==
  
−
A paper exists about the framework for diagrammatic modelling extension in Rodin:
+
Released 24 January 2011.
−
Savicks, Vitaly, Snook, Colin (2012) ''A Framework for Diagrammatic Modelling Extensions in Rodin'' in Rodin User & Developer Workshop 2012 Proceedings. Newcastle University. (Unpublished) <ref>http://deploy-eprints.ecs.soton.ac.uk/382/</ref>
 
  
−
Wiki pages are available for developers using the Generic extensions and Diagrams frameworks:<br>
+
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
−
http://wiki.event-b.org/index.php/EMF_framework_for_Event-B<br>
 
−
http://wiki.event-b.org/index.php/Generic_Event-B_EMF_extensions (Under Construction)
 
  
−
A paper exists about the Event-B state-machines:
+
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
−
Savicks, Vitaly, Snook, Colin and Butler, Michael (2009) ''Animation of UML-B State-machines'' in Rodin User & Developer Workshop 2010 Proceedings. Düsseldorf University, 2010.<ref>http://eprints.soton.ac.uk/268261/</ref>
 
  
−
Wiki pages are available for users of UML-B, everything starts from http://wiki.event-b.org/index.php/UML-B<ref>http://wiki.event-b.org/index.php/UML-B</ref>
+
The update-site is available through the Rodin update site in the ''Utilities'' category.
  
−
== Planning ==
+
The code generation tutorial examples are available for download at:
  
−
The following work is planned:
+
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
−
* Re-base the Event-B EMF framework on the EMF model of the Rodin database (which is now available as a result of the development of a new Rodin editor to replace the form based editor).
 
−
* Re-write the Event-B generator of the state-machine diagram editor so that it uses the generic generator from the Event-B GMF Support for Generic Diagrams framework. This will improve performance.
 
−
* Improve the state-machine diagram animation interface so that it supports animation of multiple diagrams.
 
−
* Complete the development of the new version of the UML-B Class Diagram editor.
 
−
* Develop Animation interface for the Class diagram editor.
 
−
* Develop a Component diagram editor and associated simulation tools.
 
  
−
= Code generation =
+
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:
  
−
== Overview ==
+
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
−
The code generation feature provides the support for the generation of code from refined Event-B models. The development of the approach, and the tools to support it, involved a number of team members at Southampton. To this end a multi-tasking approach, which is conceptually similar to that of the Ada tasking model, was designed. Tasks are modelled by an extension to Event-B, called Tasking Machines which are an extension of the existing Event-B Machine component.
 
−
The latest Code Generation feature was released on 30th May 2012. The new features in this release include code generation from state-machine diagrams (see UML-B).
 
  
−
== Motivations / Decisions ==
+
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
−
State-machines are frequently used to describe the behaviour of embedded systems. It is a relatively new feature in Event-B, and we augment the tool with the ability to generate code from state-machine diagrams in version 0.2.3 of the code generation feature plug-in. Implementation code is generated from the diagram itself, and no additional mark-up of the model is required; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-machines are created, using the existing state-machine plug-in, subject to the limitations described after.
 
  
−
The current code generation tool is restricted to generating code for a single Event-B machine, which may contain one or more state-machines. We have yet to explore the decomposition/composition of machines containing state-machines. In principal we should be able to apply decomposition techniques to decompose the single Event-B machine with state-machines into a number of machines, with the state-machines, or the elements of state-machines, distributed between them.
+
=== Latest Developments ===
−
Another limitation is that we do not handle nested state-machines, although this should be feasible.
+
* Demonstrator plug-in feature version 0.1.0
−
Only the state-machines of tasking/environ machines generate code. State-machines of shared machines do not generate code. This should be explored further during research into decomposition.
+
** for Rodin 2.1.x version is available.
  
−
The translation of the diagrammatic elements to code has been hard-coded in the code generation plug-in. We have introduced new types to the translator's common language model (IL1). We add case-statements, and a container for them (analogous to switch) since these are commonly used to implement state-machines. The code generator navigates through each state of a state-machine, generating an internal representation of the state-machine, which is used to create the IL1 model. The IL1 model is then used to generate code for the various target languages that may have been implemented. We have also updated the IL1-to-target code generators, to generate case/switch statements in Ada, C and Java.
+
* The Code Generation feature consists of,
−
Each state-machine has an Enumerated type whose elements take the names of the states. A state variable is created in the target that keeps track of the current state, and has the type of the enumeration.
+
** 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 ==
+
* A tutorial is available [[Code Generation Tutorial]]
−
A specific page on the Event-B wiki<ref>http://wiki.event-b.org/index.php/Code_Generation_Activity</ref> is dedicated to Code Generation Updates.
+
** Step 1 - Create the tasking development.
 +
** Step 2 - Add annotations.
 +
** Step 3 - Invoke translators.
  
−
== Planning ==
+
=== Ongoing Work ===
−
Efforts will focus on extending the existing code generation approach, and developing new techniques, for the simulation of cyber-physical systems.
 
  
−
= ProR =
+
* Full Rodin Integration
 +
* Sensed Variables
 +
* Branching in Shared Machines
  
−
== Overview ==
+
=== Future Work ===
 +
* Support for Interrupts.
 +
* Richer DataTypes.
 +
* Accommodation of duplicate event names in tasking developments.
  
−
The Rodin/ProR integration plugin is developed and maintained by Lukas Ladenberger and Michael Jastram at the University of Duesseldorf. ProR is a tool for working with requirements in natural language. It is part of the Eclipse Requirements Modeling Framework (RMF).<ref>http://www.eclipse.org/rmf/</ref>
+
=== 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.
  
−
The following paragraphs will give an overview of the the work that has been performed concerning maintenance on the Rodin/ProR plugin.
+
=== Translation Rules ===
 +
* Tasking to IL1/Event-B translation rules [[http://wiki.event-b.org/images/Translation.pdf]]
  
−
== Motivations / Decisions ==
+
== The Code Generation Demonstrator for Rodin 1.3.x ==
  
−
The motivation of the Rodin/ProR integration plugin was to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. Especially, the traceability within a system description is a challenging problem of requirements engineering. In particular, formal models of the system are often based on informal requirements, but creating and maintaining the traceability between the two can be challenging. In ''A Method and Tool for Tracing Requirements into Specifications''<ref name="req1ref">http://www.stups.uni-duesseldorf.de/w/Special:Publication/HalJasLad2012</ref>, we presented an incremental approach for producing a system description from an initial set of requirements. The foundation of the approach is a classification of requirements into artefacts W (domain properties), R (requirements) and S (specification). In addition, the approach uses designated phenomena as the vocabulary employed by the artefacts. The central idea is that adequacy of the system description must be justified, meaning that W ∧ S ⇒ R. The approach establishes a traceability, and the resulting system description may consist of formal and informal artefacts. We created tool support for this approach by integrating Rodin and ProR. We designed it with the goal to support the approach described in <ref name="req1ref"/>, and to ease the integration of natural language requirements and Event-B.
 
  
−
== Available Documentation ==
+
First release: 30 November 2010.
  
−
* ''A Method and Tool for Tracing Requirements into Specifications''.<ref name="req1ref"/> The paper has been submitted to Science of Computer Programming.
+
available from:
−
* ''Requirements Traceability between Textual Requirements and Formal Models Using ProR''.<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/LadenbergerJastram_iFMABZ2012</ref> The paper has been accepted for iFM'2012 & ABZ'2012.
 
  
−
* A Tutorial for the Rodin/ProR integration<ref>http://wiki.event-b.org/index.php/ProR</ref> can be found on the Event-B wiki.
+
https://sourceforge.net/projects/codegenerationd/files/
−
* The User Guide<ref>http://wiki.eclipse.org/RMF/User_Guide</ref> is available on the Event-B wiki and contains an additional tutorials for ProR.
 
  
−
== Planning ==
+
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.
  
−
There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, the method mentioned above<ref name="req1ref"/> lists a number of properties of a correct system description. For example, the existance of a trace between an artifact and its used phenomenon, or the fact that domain properties, requirement items and design decisions may only be expressed referring to phenomena that are visible in the environment, whereas design decisions and plaform properties may only be expressed referring to phenomena that are visible to the system. While the presence of such properties does not guarantee correctness, their absence indicates a problem. This is already done, to a degree, through the colour highlighting, but a reporting tool that lists all violations of those properties will be implemented.
+
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.
  
−
Currently, each used artifact is identified as belonging to one of the following class: domain properties, requirement items, specification elements, implementation elements, design decisions or platform properties. This in turn determine the different kinds of phenomena that are allowed to be used by the artefact. For the moment, the plugin does not support such classification by phenomena types. In a next step, we will work on a concept for classifying and maintaining phenomena with ProR.
+
Mac users - no bundled version available at present, but use the update site in the 'advanced' folder.  
  
−
= Camille =
+
'''A step-by-step [[Code Generation Tutorial]] is available'''
  
−
== Overview ==
+
==== About the Initial Release ====
−
The Camille plug-in provides a textual editor for Rodin.
+
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.
−
Though such a text editor is prefered by many users, Camille currently has the drawback of not supporting extensibility.
 
−
It only supports the core Event-B language and plug-in-specific additions are simply ignored. Such extensions can not be edited through Camille.
 
−
Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions.
 
−
This has become a major issue during the last years, since many plug-ins have been developed in the meantime that are widely used by many users.
 
  
−
This issue is currently being adressed by Ingo Weigelt at the University of Duesseldorf.
+
==== Source Code ====
  
−
== Motivations / Decisions ==
+
The sources are available from,
−
A new version of Camille will be implemented during the ADVANCE project to enable users to edit extended Event-B models solely through a text editor.
 
−
To plan the new version, the problem and a number of possible solutions have been analysed and related in a technical report<ref name="Architectures_for_an_Extensible_Text_Editor_for_Rodin">http://www.stups.uni-duesseldorf.de/mediawiki/images/0/0a/Pub-Weigelt2012.pdf</ref> from Ingo Weigelt.
 
−
The results of this work have been dicussed in the Rodin community and one of the proposed solution (a blockparser) has been selected to be implemented during the next months.
 
−
The dedicated solution promises to provide Camille extensibility with minimal extra workload required from plug-in developers while still being very flexible regarding future, yet unknown, requirements.
 
  
−
== Available Documentation ==
+
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
  
−
* ''Architectures for an Extensible Text Editor for Rodin''.<ref name="Architectures_for_an_Extensible_Text_Editor_for_Rodin"/> Bachelor thesis analysing the problem and discussing possible solutions.
+
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
−
* An earlier version of the thesis has been published as a technical report<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/Weigelt2012></ref> that has been discussed on the Roding Developers Mailing List and the ADVANCE Progress Meeting in May 2012 in Paris.
 
  
−
== Planning ==
 
−
The new Camille version will be implemented at the University of Duesseldorf during 2012. The final version is expected in January or February 2013.
 
  
−
= References =
 
−
<references/>
 
  
−
[[Category:ADVANCE D3.2 Deliverable]]
+
[[Category:Work in progress]]

Revision as of 11:43, 17 May 2012

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, or Chris Lovell mailto:cjl3@ecs.soton.ac.uk


Code Generation Feature - Version 0.2.3 For Rodin 2.5

A new release of the tool is imminent.

The main new features are:

  • Code generation from state-machine diagrams.
  • Improved static checking.

We have also provided some details of the use of Theories in code generation, from the previous version.

Updated Examples etc. are available:

  • Tutorial, and example, projects are available from the Examples directory: SVN.
  • Test projects are also available from the Examples directory SVN.
  • Sources (will be) available at: SVN
  • Example Theories at: SVN

Code Generation Feature - Version 0.2.2 For Rodin 2.4

We released V0.2.2 on 22-03-2012. The main changes, to the interface, and translation from theories are described below:

  • Tasking Event-B is now integrated with the Event-B Editors.
  • We have the ability to translate to C, Java, etc. in addition to Ada source code.
  • We use theories to define translations of the Event-B mathematical language (Theories for Ada, Java and C are supplied).
  • We use the theory plug-in as a mechanism for defining new data types , and the translations to target data types.
  • The translator is extensible.
  • Minimal use is made of the EMF tree editor in Rose.

To install v0.2.2:

  • Access the main Rodin Update Site. In Eclispe click on Help/Install new Software. Find the Rodin update site from the list. In Utilities add Code Generation.

The approach makes use of the following, which should be installed if the features are required by the user for editing:

  • Model Decomposition: Download from the main Rodin Update Site, in the Decomposition section.
  • Shared Event Composition: Download from the main Rodin Update Site, in the Decomposition section.
  • Theory Plug-in: Download from the main Rodin Update Site, in the Modelling Extensions section.

Examples available at:

  • Tutorial, and example, projects are available from the Examples directory: SVN.
  • Test projects are also available from the Examples directory SVN.
  • Sources at: SVN
  • Example Theories at: SVN

Code Generation Feature - Version 0.2.1 For Rodin 2.3

Contains Bug Fixes for previous release. 14-12-2011

Code Generation Feature - Version 0.2.0 For Rodin 2.3

We released a new version of the code generator on 30-11-2011, and updated documentation.

Changes to the Tooling and Approach

The main changes are:

  • The code generators have been completely re-written. The translators are now implemented in Java, i.e. there is no longer a dependence on the Epsilon tool set. This was undertaken for code maintenance reasons.
  • Tasking Event-B is now integrated with the Event-B explorer.
  • The Rose Editor is used for editing the Tasking Event-B, and
  • a text-based editor is provided, using the Rose extension, for editing the TaskBody. This feature has been added to address some of the usability concerns. It also overcomes the 'problem' experienced with duplicate event names in a development, since the parser-builder that has been implemented automatically selects the correct event.
  • The EMF tree editor in Rose is only used minimally; we plan enhancements to further reduce its use.
  • Composed machines are used to store event 'synchronizations'; these are generated automatically during the decomposition process. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events.
  • The code generation approach is now extensible; new target language constructs can be added using the Eclipse extension mechanism.
  • The translation of target's mathematical language is now specified in the theory plug-in. This improves clarity since the the translation from source to target is achieved by specifying pattern matching rules. Extensibility is also improved; the theory plug-in is used to specify new data-types, and how they are implemented.
  • Translated code is deposited in a directory in the appropriate files. An Ada project file is generated for use with AdaCore's GPS workbench. Eventually this could be enabled/disabled in a preferences dialog box.
  • The Tasking Event-B to Event-B translator is now properly integrated. Control variable updates to the Event-B model are made in a similar way to the equivalent updates in the state-machine plug-in. The additional elements are added to the Event-B model and marked as 'generated'. This prevents users from manually modifying them, and allows them to be removed through a menu choice.
Changes to the Documentation

The following Pages have been updated:

TODO

  • Add addressed variables (for direct read/write access to memory)
  • Flattening of composed machines/implementation machines.
  • Interrupts

Sensing and Actuating for Tasking Event-B

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.

  • The new v0.1.5 feature is available from the Rodin Update Site, it resides in the Utilities Category.
  • Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.

A new Code Generation Tutorial has been produced, that makes use of these new features. There is an explanation of the heating controller, upon which it is based, here.

The example/tutorial projects, and also and a Bundled Windows 7 version, are available in the Deploy E-Prints archive or Examples SVN site.

The Code Generation Demonstrator for Rodin 2.1.x

Released 24 January 2011.

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.

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.

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 [[1]]

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

Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.2_General_Platform_Maintenance&oldid=1456’