Difference between pages "Current Developments" and "Rodin Developer Support"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Colin
 
imported>Laurent
(→‎Debugging: add pointers to Eclipse resources.)
 
Line 1: Line 1:
{{TOCright}}
+
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
This page sum up the known developments that are being done around or for the [[Rodin Platform]]. ''Please contributes informations about your own development to keep the community informed''
 
  
== Deploy Tasks ==
 
The following tasks were planned at some stage of the [[Deploy]] project.
 
=== Core Platform ===
 
==== New Mathematical Language ====
 
==== Rodin Index Manager ====
 
[[Systerel]] is in charge of this task.
 
{{details|Rodin Index Design|Rodin index design}}
 
  
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.
+
== Rodin Developer FAQ ==
  
==== Text Editor ====
+
see [[Developer FAQ]].
The efforts in [[Düsseldorf]] ([[User:Fabian|Fabian]]) and [[Newcastle]] ([[User:Alexei|Alexei]]) have been joined to create a single text editor which will be part of the [[#EMF framework for Rodin|EMF framework for Rodin]] (see that [[#EMF framework for Rodin|section]] for details).
 
  
==== EMF framework for Event-B ====
+
== Architecture of the Rodin Platform ==
Newcastle, Southampton and Düsseldorf have begun to develop an EMF framework to support Rodin modelling tools based on EMF. The framework includes an EMF representation of Event-B, a synchronising persistence interface for loading and saving models via the Rodin API and facilities to support text editing and parsing. Examples of tools that will be based on the EMF framework for Rodin are, a Text editor, a compare/merge editor (which can be used for team based development), pattern/composition tools, Diagram Editors. 
 
  
More details can be found here: [[EMF framework for Event-B]]
+
=== Rodin Platform Core ===
  
=== Plug-ins ===
+
* [[Database]]
==== Requirement Management Plug-in ====
 
[[User:Jastram|Michael]] at [[Düsseldorf]] is in charge of the [[:Category:Requirement Plugin|Requirements Management Plug-in]].
 
  
{{See also|ReqsManagement|Requirements Tutorial|l1=Requirements Management Plug-in}}
+
* [[Builder]]
  
This plug-in allows:
+
* [[Rodin Index Design]]
* Requirements to be edited in a set of documents (independently from Rodin)
 
* Requirements to be viewed within Rodin
 
* Individual Requirements to be linked to individual Event-B-Entities
 
* A basic completion test to be performed
 
  
==== UML-B Improvements ====
+
* [[Indexing System]]
[[Southampton]] is in charge of [[UML-B]] plug-in.
 
  
A new version of UML-B is being developed that will have improved integration with Event-B. The new version will be built as an extension to the EMF framework for Event-B. While this new version is being developed improvements are also being made to the existing version of UML-B. Both topics are covered in more detail on the following page:
+
* [[Undo Redo]]
[[UML-B Integration and Improvements]]
 
  
==== ProB Plug-in ====
+
* [[File Root Separation]]
[[Düsseldorf]] is in charge of [[ProB]].
 
<!-- {{details|ProB current developments|ProB current developments}} -->
 
  
===== Work already performed =====
+
=== Event-B User Interface ===
  
We have now ported ProB to work directly on the Rodin AST. Animation is working and the user can now set a limited number of preferences.
+
The Event-B User Interface of the Roding Platform has two major components that are concerned with either [http://handbook.event-b.org/current/html/event_b_perspective.html modelling] in Event-B or [http://handbook.event-b.org/current/html/proving_perspective.html proving] properties of models.
The model checking feature is now also accessible.
 
It is also possible to create CSP and classical B specification files. These files can be edited with BE4 and animated/model checked with ProB.
 
On the classical B side we have moved to a new, more robust parser (which is now capable of parsing some of the more complicated AtelierB
 
specifications from Siemens).
 
  
On the developer side, we have moved to a continuous integration infrastructure using CruiseControl. Rodin is also building from CVS in that infrastructure.
+
* [http://handbook.event-b.org/current/html/event_b_perspective.html Modelling User Interface]
  
===== Ongoing and future developments=====
+
* [http://handbook.event-b.org/current/html/proving_perspective.html Proving User Interface]
  
We are currently developing a new, better user interface.
+
Apart from these are more minor components.
We also plan to support multi-level animation with checking of the gluing invariant.
 
  
We have prototypes for several extensions working, but they need to be fully tested and integrated into the plugin:
+
* [[Proof Purger Design|Proof Purger]] allows to delete unused proofs.
* an inspector that allows the user to inspect complex predicates (such as invariants or guards) as well as expressions in a tree-like manner
 
* a graphical animator based on SWT that allows the user to design his/her own animations easily within the tool
 
* a 2D viewer to inspect the state space of the specification
 
  
==== B2Latex Plug-in ====
+
* [[Proof Skeleton Design]] is a view that displays skeletons of existing proofs
[[Southampton]] is in charge of [[B2Latex]].
 
  
Kriangsak Damchoom will update the plug-in to add [[Event Extension|extensions of events]].
+
* [[Auto-Completion Design]] proposes a list of names to the user editing a model
  
==== Parallel Composition Plug-in ====
+
=== Event-B Component Library ===
[[Southampton]] is in charge of the [[Parallel Composition using Event-B]] .
 
  
The intention of the plug-in is to allow the parallel composition of events using Event-B syntax. The composition uses a value-passing style (shared event composition), where parameters can be shared/merged.
+
Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a [[Static Checker|static checker]]. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The [[Proof Obligation Generator|proof obligation generator]] uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the [[Proof Manager|proof manager]] attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the [http://handbook.event-b.org/current/html/proving_perspective.html proving user interface]).
  
This plug-in allows:
+
* [[Abstract Syntax Tree]]
* Selection of machines that will be part of the composition (''Includes'' Section)
 
* Possible selection of an abstract machine (''Refines'' Section)
 
* Possible inclusion of invariants that relate the included machines (''Invariant'' Section and use of the monotonicity )
 
* Invariants of included machines are conjoined.
 
* Selection of events that will be merged. The event(s) must come from different machines. At the moment, events with parameters with same name are merged. If it is a refinement composition, it is possible to choose the abstract event that is being refined.
 
* Initialisation event is the parallel composition of all the included machines' initialisations.
 
* For a composed event, the guards are conjoined and the all the actions are composed in parallel.
 
  
Currently, after the conclusion of the composition machine, a new machine can be generated, resulting from the properties defined on the composition file. This allows proofs to be generated as well as a visualisation of the composition machine file. In the future, the intention is to make the validation directly on the composition machine file directly where proofs would be generated ( and discharged) - the new machine generation would be optional. An event-b model for the validation/generation of proofs in currently being developed. Another functionality which should be quite useful for the composition (but not restricted to that) is '''renaming''':
+
* [[Static Checker]]
  
* while composing, two machines may have variables with the same name for instance (which is not allowed for this type of composition). In order to solve this problem, one would have to rename one of the variables in order to avoid the clash, which would mean change the original machine. A possible solution for that would be to rename the variable but just on composition machine file, keeping the original machine intact. A renaming framework designed and developed by Stefan Hallerstede and Sonja Holl exists currently although still on a testing phase. The framework was developed to be used in a general fashion (not constrained to event-b syntax). The idea is to extend the development of this framework and apply to Event-B syntax (current development).
+
* [[Proof Obligation Generator]]
  
There is a prototype for the composition plug-in available that works for Rodin 0.8.2. A release for the Rodin 0.9 is concluded and will be available from the Rodin Main Update Site soon, under 'Shared Event Composition' update.
+
* [[Proof Manager]]
  
==== Measurement Plug-In ====
+
* [[Proof Simplification]]
  
The [[Measurement Plug-In]] to the RODIN platform will provide information both about the model itself and about the process of building the model.
+
== Extending Rodin ==
It has a double purpose:
 
  
* provide feedback to the user about the quality of the Event-B model he is building and about potential problems in it or in the way he is building it.
+
* [[Developer Documentation]]
* automate the data collection process for the measurement and assessment WP. This data collected will be analyzed to identify global transfer (increase in model quality, size, complexity,...), tool shortcomings (usability, prover), modelling issues (to be addressed by training, language, tool evolution,...), etc.
 
  
== Exploratory Tasks ==
+
* [[Plug-in Tutorial]]
=== One Single View ===
 
[[Maria]] is in charge of this exploratory work during is internship.
 
{{details|Single View Design|Single View Design}}
 
The goal of this project is to present everything in a single view in Rodin. So the user won't have to switch perspectives.
 
  
 +
* [[Extending the Rodin Database]]
  
 +
* [[Extending the project explorer]]
  
== Others ==
+
* [[Extending the Structure Editor]]
  
=== AnimB ===
+
* [[Extending the Pretty Print Page]]
[[Christophe]] devotes some of its spare time for this plug-in.
 
{{details|AnimB Current Developments|AnimB Current Developments}}
 
The current developments around the [[AnimB]] plug-in encompass the following topics:
 
;Live animation update
 
:where the modification of the animated event-B model is instantaneously taken into account by the animator, without the need to restart the animation.
 
;Collecting history
 
:The history of the animation will be collected.
 
  
=== Team-Based Development ===
+
* [[Extending the Proof Manager]]
  
; Usage Scenarios
+
* [[Extending the Index Manager]]
: In order to understand the problem properly, [http://www.stups.uni-duesseldorf.de/ Düsseldorf] created a number of usage [[Scenarios for Team-based Development]].
 
: A page as also been opened for [[Scenarios for Merging Proofs|merging proofs scenarios]].
 
[[Category:Work in progress]]
 
  
=== B2C ===
+
* [[Extending the Static Checker]]
This plug-in translates Event-B models to C source code, which may then be compiled using external C development tools. [[Steve]] wrote B2C with the specific purpose of translating the  [http://dx.doi.org/10.1007/978-3-540-87603-8_21 MIDAS] model, an Event-B implementation of a Virtual Machine instruction set.
 
  
B2C supports a sub-set of Event-B that can be easily translated to C form. The user provides a final refinement step that does nothing except restate the model in this translatable form: symbolic constants must be replaced by their literal values, range membership guards are replaced by greater-than and less-than guards, and actions are restated not to use global statments on their left-sides (this because the variable may have been modified by an earlier action, and may not be valid). The manipulations are done within EventB where they can be checked by the Proof Obligation system, and B2C made as simple as possible to maximise reliability. This re-write process is currently a manual step, but could in principle be done by another plug-in
+
* [[Index Query]]
  
B2C source code is not currently available for download: contact [[Steve]] directly if it is required.
+
== Useful Hints ==
  
 +
=== Version Control ===
  
 +
All sources of the core Rodin platform (and of some plug-ins) are managed under version control in SourceForge.  The repository currently used is Subversion and can be accessed using URL [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp].
  
=== New Proof Rules ===
+
=== Building against a version of Rodin ===
  
[[New Proof Rules|This document]] describes the set of newly added reasoners for improving the usability of the prover within Rodin Platform.
+
To develop extensions to the Rodin platform your code build needs access to a consistent (version-wise) set of Rodin platform plug-ins. (Don't just check out the latest versions from 'Head' because it may be under development and in an inconsistent state). An easy way to set up your workspace is to import the Rodin platform source code from SVN into your workspace using the 'Releng' plug-in.
 +
See [http://wiki.event-b.org/index.php/Developer_FAQ#Installing_the_sources_from_Subversion_in_Eclipse Installing the sources from Subversion in Eclipse] for further instructions.
 +
 
 +
Alternatively, you can set your plugin development target platform to any Rodin installation you have installed (Eclipse-Preferences-Plug-in Development-Target Platform). This is useful as a final test that everything will work once installed into Rodin but because it uses a 'built' platform, you don't get access to the Rodin source code (e.g. for de-bugging).
 +
 
 +
=== Testing ===
 +
 
 +
=== Debugging ===
 +
 
 +
There is nothing special to the Rodin platform as concerns debugging. This is just like debugging any Eclipse plug-in. See for instance [http://eclipse.org/resources/?sort=date&category=Debugging Eclipse Debugging Resources].
 +
 
 +
=== Publishing ===
 +
 
 +
A Plug-in developed for the Rodin Platform will normally consist of a collection of eclipse 'plugin' projects and a single eclipse 'feature' project. The feature project contains branding information such as logo's icons and licensing details. It is also used to identify your Plug-in so that users can install it. To build your Plug-in use an eclipse 'site' project. This will build the jar files for your plugin projects and a jar for your feature. See eclipse documentation for more details.
 +
 
 +
Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform).
 +
 
 +
Create a new release folder in the FRS (On Sourceforge Rodin project website - Admin-file releases) noting the naming conventions (e.g. Plugin_<mypluginName>). Now you can upload your jar files using the controls on the releases webpage). Note that you should include a zip of the complete source projects to comply with Sourceforge rules.
 +
You should not repeat files that have not changed. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release.
 +
See here for details:- http://alexandria.wiki.sourceforge.net/File+Release+System+-+Offering+Files+for+Download
 +
 
 +
Finally, the update site must be updated to redirect the update requests to the files on the FRS.
 +
# From the sourceforge SVN repository, check out the project org.rodinp.updateSite.
 +
# Edit the  file site.xml to add your feature and plug-in archive paths ([[Details for Maintaining Main Rodin Update Site]])
 +
# Test the changes by performing the install into a Rodin installation, via the local update site in your workspace.
 +
# Commit the changes back into SVN
 +
# Upload the new version of the update site onto the Rodin webspace ([[Details for Uploading Main Rodin Update Site]]).
 +
 
 +
 
 +
=== Upgrading and maintain ===
 +
 
 +
Please note that you should always keep an existing version of your plug-in for the antepenultimate version of Rodin when you want to perform some clean-up of your update site.
 +
Indeed, not all the users switch to the latest version of Rodin by the time of its release, and certainly would like to use your plug-ins anyway.
 +
 
 +
[[Category:Developer documentation]]
 +
[[Category:Rodin Platform]]

Revision as of 11:28, 28 October 2011

The Developer Support provides resources for developing plug-ins for the Rodin Platform.


Rodin Developer FAQ

see Developer FAQ.

Architecture of the Rodin Platform

Rodin Platform Core

Event-B User Interface

The Event-B User Interface of the Roding Platform has two major components that are concerned with either modelling in Event-B or proving properties of models.

Apart from these are more minor components.

Event-B Component Library

Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an abstract syntax tree. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a static checker. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The proof obligation generator uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the proof manager attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the proving user interface).

Extending Rodin

Useful Hints

Version Control

All sources of the core Rodin platform (and of some plug-ins) are managed under version control in SourceForge. The repository currently used is Subversion and can be accessed using URL https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp.

Building against a version of Rodin

To develop extensions to the Rodin platform your code build needs access to a consistent (version-wise) set of Rodin platform plug-ins. (Don't just check out the latest versions from 'Head' because it may be under development and in an inconsistent state). An easy way to set up your workspace is to import the Rodin platform source code from SVN into your workspace using the 'Releng' plug-in. See Installing the sources from Subversion in Eclipse for further instructions.

Alternatively, you can set your plugin development target platform to any Rodin installation you have installed (Eclipse-Preferences-Plug-in Development-Target Platform). This is useful as a final test that everything will work once installed into Rodin but because it uses a 'built' platform, you don't get access to the Rodin source code (e.g. for de-bugging).

Testing

Debugging

There is nothing special to the Rodin platform as concerns debugging. This is just like debugging any Eclipse plug-in. See for instance Eclipse Debugging Resources.

Publishing

A Plug-in developed for the Rodin Platform will normally consist of a collection of eclipse 'plugin' projects and a single eclipse 'feature' project. The feature project contains branding information such as logo's icons and licensing details. It is also used to identify your Plug-in so that users can install it. To build your Plug-in use an eclipse 'site' project. This will build the jar files for your plugin projects and a jar for your feature. See eclipse documentation for more details.

Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform).

Create a new release folder in the FRS (On Sourceforge Rodin project website - Admin-file releases) noting the naming conventions (e.g. Plugin_<mypluginName>). Now you can upload your jar files using the controls on the releases webpage). Note that you should include a zip of the complete source projects to comply with Sourceforge rules. You should not repeat files that have not changed. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release. See here for details:- http://alexandria.wiki.sourceforge.net/File+Release+System+-+Offering+Files+for+Download

Finally, the update site must be updated to redirect the update requests to the files on the FRS.

  1. From the sourceforge SVN repository, check out the project org.rodinp.updateSite.
  2. Edit the file site.xml to add your feature and plug-in archive paths (Details for Maintaining Main Rodin Update Site)
  3. Test the changes by performing the install into a Rodin installation, via the local update site in your workspace.
  4. Commit the changes back into SVN
  5. Upload the new version of the update site onto the Rodin webspace (Details for Uploading Main Rodin Update Site).


Upgrading and maintain

Please note that you should always keep an existing version of your plug-in for the antepenultimate version of Rodin when you want to perform some clean-up of your update site. Indeed, not all the users switch to the latest version of Rodin by the time of its release, and certainly would like to use your plug-ins anyway.