Difference between pages "ADVANCE D3.2 General Platform Maintenance" and "FAQ"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Colin
 
imported>Laurent
 
Line 1: Line 1:
−
== Core Rodin platform (Thomas Muller) ==
+
== General ==
 +
=== What is Event-B? ===
 +
'''Event-B''' is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. More details are available in http://www.event-b.org/
  
−
=== Overview ===
+
=== What is Rodin? ===
−
{{TODO|Fill this paragraph.}}
+
The '''Rodin Platform''' is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.
  
−
=== Motivations / Decisions ===
+
=== Where does the ''Rodin'' name come from? ===
−
{{TODO|Fill this paragraph.}}
 
  
−
=== Available Documentation ===
+
== General Tool Usage? ==
−
{{TODO|Fill this paragraph.}}
 
  
−
=== Planning ===
+
=== How do I install external plug-ins without using Eclipse Update Manager? ===
−
{{TODO|Fill this paragraph.}}
+
Although it is preferred to install additional plug-ins into the Rodin platform using the Update Manager of Eclipse, this might not always be practical. In this case, a manner to install these plug-ins is to emulate either manually or using ad-hoc scripts the operations normally performed by the Update Manager.
  
 +
This manual installation of plug-ins is described in ''[[Installing external plug-ins manually]]''.
  
 +
=== The builder takes too long ===
 +
Generally, the builder spends most of its time attempting to prove POs.  There are basically two ways to get it out of the way:
 +
* the first one is to disable the automated prover in the Preferences panel.
 +
* the second one is to mark some PO as reviewed when you don't want the auto-prover to attempt them anymore.
 +
Note that if you disable the automated prover, you always can run it later on some files by using the contextual menu in the event-B Explorer.
  
−
== UML-B Improvements (Colin Snook, Vitaly Savicks) ==
+
To disable the automated prover, open Rodin <tt>Preferences</tt> (menu {{menu|Window > Preferences...}}).  In the tree in the left-hand panel, select {{menu|Event-B > Sequent Prover > Auto-tactic}}. Then, in the right-hand panel ensure that the checkbox labelled <tt>Enable auto-tactic for proving</tt> is disabled.
  
−
=== Overview ===
+
To review a proof obligation, just open it in the interactive prover, then click on the ''review'' button (this is a round blue button with a ''R'' in the proof control toolbar).  The proof obligation should now labelled with the same icon in the event-B explorer.
  
−
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. 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.
+
===What are the ASCII shortcuts for mathematical operators===
  
−
=== Motivations / Decisions ===
+
The ASCII shortcuts that can be used for entering mathematical operators are described in the help of the event-B keyboard plug-in.  In the help system, this page has the following path {{menu|Event-B Keyboard User Guide > Getting Started > Special Combos}}.
  
−
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.
+
This page is also available in the dynamic help system.  The advantage of using dynamic help is that it allows to display the help page side-by-side with the other views and editors. To start the dynamic help, click {{menu|Help > Dynamic Help}}, then click {{menu|All Topics}} and select the page in the tree.
  
−
* The Event-B EMF framework provides an EMF basis for Event-B models (developed during the Deploy project).
+
== Modeling and Proving==
−
** Provides an EMF representation of Event-B models with persistance into the Rodin database.
+
=== Witness for {{Ident|Xyz}} missing. Default witness generated ===
−
* 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).
+
A parameter as disappeared during a refinement. If this is intentional, you have to add a [[Witnesses (Modelling Language)|witness]] telling how the abstract parameter is refined.
−
** Provides Navigator support for EMF-only model elements
 
−
** Provides a persistence mechanism for model extensions that are not needed to be processed by Rodin.
 
−
** A Generic Refiner for modelling extensions has recently been added.
 
−
** More generic support features may be added during Advance as required.
 
−
* 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).
 
−
** Provides Generic support for diagrammatic aspects of modelling extensions
 
−
** A generic Validation and Event-B generation service has recently been added
 
−
 
−
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.
 
  
−
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.
+
=== I've added a witness for {{ident|Xyz}} but it keeps saying ''"Identifier {{ident|Xyz}} has not been defined"'' ===
 +
As specified in the [[Witnesses (Modelling Language)|modelling language manual]], the witness must be labelled by the name {{Ident|Xyz}} of the concrete variable being concerned.
  
−
=== Available Documentation ===
+
=== How can I do a Proof by Induction? ===
−
{{TODO|Fill this paragraph.}}
+
[[Induction proof]] will give you some tips about it.
  
−
=== Planning ===
+
=== Labels  of proof tree nodes explained ===
 +
* {{ident|ah}} means ''add hypothesis'',
 +
* {{ident|eh}} means rewrite with ''equality from hypothesis'' from left to right,
 +
* {{ident|he}} means rewrite with ''equality from hypothesis'' from right to left,
 +
* {{ident|rv}} tell us that this goal as been manually [[The_Proving_Perspective_(Rodin_User_Manual)#The_Proof_Control_Window|reviewed]],
 +
* {{ident|sl/ds}} means ''selection/deselection'',
 +
* {ident|PP}} means ''discharged by the predicate prover''
 +
* {{ident|ML}} means ''discharged by the mono lemma prover''
  
−
The following work is planned:
+
== Developer FAQ ==
−
* Re-base the Event-B EMF framework on the EMF model of the Rodin elements which is now available as a result of the development of a new Rodin editor to replace the form based editor.
+
=== Using Rodin-CVS from eclipse consumes too much memory ===
−
* 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 as the current QVT based implementation is too slow.
+
You can [[#How do I generate a Rodin product from CVS|generate a product]] and use it as if it was a normal release.
−
* 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 (Andy Edmunds) ==
+
=== How do I generate a ''Rodin'' product from CVS? ===
 +
In the project ''org.rodinp.platform'', right-click on ''Rodin.platform'' and select {{menu|export}}. Choose {{menu|Plug-in Development > Eclipse product}} and click on {{button|Next}} type <tt>Rodin</tt> for the ''Root directory'', and choose the ''Destination directory''. Then click on {{button|Finish}}.
  
−
=== Overview ===
+
=== How do I collect debug information from the Rodin platform? ===
−
{{TODO|Fill this paragraph.}}
+
You may see the log in the console by appending <tt>-consoleLog</tt> to the rodin executable: <code>rodin -consoleLog</code>
  
−
=== Motivations / Decisions ===
+
You may add specific debug informations by setting specific options: <code>rodin --debug options.file -consoleLog</code> where {{file|options.file}} contains something like:
−
{{TODO|Fill this paragraph.}}
+
<pre>
 +
org.pluginname/debug = true
 +
org.pluginname/debug/optionaldebug = true
 +
</pre>
 +
where'' optionaldebug'' may be found in the {{file|org.pluginname/.options}} file in the [http://rodin-b-sharp.cvs.sourceforge.net/rodin-b-sharp/ rodin source repository].
  
−
=== Available Documentation ===
+
=== How do I submit a patch? ===
−
{{TODO|Fill this paragraph.}}
+
Good practises for patch submission are described [[How to Submit Patches|here]].
  
−
=== Planning ===
+
=== How do I track memory leaks? ===
−
{{TODO|Fill this paragraph.}}
+
If you suspect that some memory isn't freed, you may find some useful directions on how to track memory leaks [[Tracking Memory Leaks|here]].
  
−
 
+
[[Category:User FAQ]]
−
 
+
[[Category:Developer FAQ]]
−
== ProR (Michael Jastram/Lukas Ladenberger) ==
 
−
 
 
−
=== Overview ===
 
−
 
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
* A Method for Tracing Requirements into Specifications
 
−
* ProR/Rodin Integration plugin to support the method
 
−
 
 
−
=== Motivations / Decisions ===
 
−
 
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
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 <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 ===
 
−
 
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
* A Method and Tool for Tracing Requirements into Specifications: <ref name="req1ref"/> The paper has been submitted to Science of Computer Programming.
 
−
* 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.
 
−
 
 
−
* Tutorial for the Rodin/ProR integration can be found here: <ref>http://wiki.event-b.org/index.php/ProR</ref>.
 
−
* The User Guide containing an additional Tutorial for ProR can be found here: <ref>http://wiki.eclipse.org/RMF/User_Guide</ref>.
 
−
 
 
−
=== Planning ===
 
−
 
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
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, <ref name="req1ref"/> lists a number of properties of a correct system description. While the presence of these properties does not guarantee correctness, their absence indicates a problem. Reporting on the state of these properties would be valuable.
 
−
 
 
−
Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.
 
−
 
 
−
== References ==
 
−
<references/>
 
−
 
 
−
== Camille (Ingo Weigelt) ==
 
−
 
 
−
=== Overview ===
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
=== Motivations / Decisions ===
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
=== Available Documentation ===
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
=== Planning ===
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
== References ==
 
−
<references/>
 
−
 
 
−
[[Category:ADVANCE D3.2 Deliverable]]
 

Revision as of 15:10, 11 February 2009

General

What is Event-B?

Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. More details are available in http://www.event-b.org/

What is Rodin?

The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.

Where does the Rodin name come from?

General Tool Usage?

How do I install external plug-ins without using Eclipse Update Manager?

Although it is preferred to install additional plug-ins into the Rodin platform using the Update Manager of Eclipse, this might not always be practical. In this case, a manner to install these plug-ins is to emulate either manually or using ad-hoc scripts the operations normally performed by the Update Manager.

This manual installation of plug-ins is described in Installing external plug-ins manually.

The builder takes too long

Generally, the builder spends most of its time attempting to prove POs. There are basically two ways to get it out of the way:

  • the first one is to disable the automated prover in the Preferences panel.
  • the second one is to mark some PO as reviewed when you don't want the auto-prover to attempt them anymore.

Note that if you disable the automated prover, you always can run it later on some files by using the contextual menu in the event-B Explorer.

To disable the automated prover, open Rodin Preferences (menu Window > Preferences...). In the tree in the left-hand panel, select Event-B > Sequent Prover > Auto-tactic. Then, in the right-hand panel ensure that the checkbox labelled Enable auto-tactic for proving is disabled.

To review a proof obligation, just open it in the interactive prover, then click on the review button (this is a round blue button with a R in the proof control toolbar). The proof obligation should now labelled with the same icon in the event-B explorer.

What are the ASCII shortcuts for mathematical operators

The ASCII shortcuts that can be used for entering mathematical operators are described in the help of the event-B keyboard plug-in. In the help system, this page has the following path Event-B Keyboard User Guide > Getting Started > Special Combos.

This page is also available in the dynamic help system. The advantage of using dynamic help is that it allows to display the help page side-by-side with the other views and editors. To start the dynamic help, click Help > Dynamic Help, then click All Topics and select the page in the tree.

Modeling and Proving

Witness for
Xyz
missing. Default witness generated

A parameter as disappeared during a refinement. If this is intentional, you have to add a witness telling how the abstract parameter is refined.

I've added a witness for
Xyz
but it keeps saying "Identifier
Xyz
has not been defined"

As specified in the modelling language manual, the witness must be labelled by the name

Xyz

of the concrete variable being concerned.

How can I do a Proof by Induction?

Induction proof will give you some tips about it.

Labels of proof tree nodes explained

  • ah
    means add hypothesis,
  • eh
    means rewrite with equality from hypothesis from left to right,
  • he
    means rewrite with equality from hypothesis from right to left,
  • rv
    tell us that this goal as been manually reviewed,
  • sl/ds
    means selection/deselection,
  • {ident|PP}} means discharged by the predicate prover
  • ML
    means discharged by the mono lemma prover

Developer FAQ

Using Rodin-CVS from eclipse consumes too much memory

You can generate a product and use it as if it was a normal release.

How do I generate a Rodin product from CVS?

In the project org.rodinp.platform, right-click on Rodin.platform and select export. Choose Plug-in Development > Eclipse product and click on Next type Rodin for the Root directory, and choose the Destination directory. Then click on Finish.

How do I collect debug information from the Rodin platform?

You may see the log in the console by appending -consoleLog to the rodin executable: rodin -consoleLog

You may add specific debug informations by setting specific options: rodin --debug options.file -consoleLog where

options.file

contains something like: 

org.pluginname/debug = true
org.pluginname/debug/optionaldebug = true

where optionaldebug may be found in the

org.pluginname/.options

file in the rodin source repository.

How do I submit a patch?

Good practises for patch submission are described here.

How do I track memory leaks?

If you suspect that some memory isn't freed, you may find some useful directions on how to track memory leaks here.

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