Difference between pages "D45 Prover Enhancement" and "D45 Scalability"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Leuschel
 
imported>Tommy
 
Line 1: Line 1:
 
= Overview =
 
= Overview =
−
* Two tasks concerned the prover performance from the core platform: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. While the addition of rewriting and inference rules has always been a regular task to enhance the Rodin integrated prover during DEPLOY lifetime, a new way to manage tactics has been implemented. In fact, the user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations.
+
Three main domains concerned the scalability task during the last year of the project:<br>
−
* The ProB plug-in allows to find and visualize counter examples to the invariant and deadlock preservation proof obligations. ProB has also been used for finding count examples to proof rules of the industrial partner Siemens.
+
'''Improved Performance'''. According to the refocus mentioned in the General Platform Maintenance chapter, much of the reworking efforts performed on the core platform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed in a separate chapter.<br>
−
* The SMT Solvers plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. {{TODO}} (Laurent Voisin, Yoann Guyot)
+
'''Design pattern management / Generic Instantiation'''. Formal methods are applicable to various domains for constructing models of complex systems. However, often they lack some systematic methodological approaches, in particular in reusing existing models, for helping the development process.  The objective in introducing design patterns within formal methods in general, and in Event-B in particular, is to overcome this limitation.<br>
 +
'''Editors'''. Along DEPLOY, edition became a central concern. Indeed, many usability issues appeard the models involved in pilots became "industrial" sized: 
 +
:*The legacy structured editor based on a form edition specific architecture reached its limits in editing such complex models. Industrial partners found this issue significant regarding the adoption of the Rodin platform in industry and providing a new structured editor correcting this issue became an important task during this last year of the DEPLOY project.
 +
:*Camille textual editor had to tackle challenges related to resources mapping and management for projects of industrial size mentioned above or even the design of extension capabilities. Extension capabilities became a major concern since the grammar could be extended with theories.
  
 
= Motivations =
 
= Motivations =
−
== New rewriting and inference rules ==
 
−
In an Event-B development, more than 60% of the time is spent on proofs. It has been a continuous aim to increase the number of automatically discharged proof obligations (POs) by improving the capabilities of the integrated sequent prover through the addition of rewriting and inference rules. These rules were provided through tactics, or existing or newly created. These tactics were automatic, or manual, or sometimes both. Providing new proving rules, even if it sometimes does not increase directly the number of automatically discharged POs aims to help the user to interactively discharge them and spare his time.
 
  
−
== Advanced Preferences for Auto-tactics ==
+
== Improved Performance ==
 +
Many issues concerning stability and performance were related to the core code of the Rodin platform, causing crashes, loss of data, corruption in models. Other issues were related to the UI causing platform hanging, and sometimes leading to its freezing which required sometimes to kill the Rodin process, thus also leading to potential loss of data and corruption in models. Addressing these issues before the end of DEPLOY was mandatory.
  
−
The proportion of automatically discharged proof obligations heavily depends on Auto-Tactic configuration.
+
== Design Pattern Management / Generic Instantiation  ==
−
Sometimes, the automatic prover fails because the tactics are applied in a 'wrong' order - 'wrong' for a given PO - even though all needed tactics are present.
+
The idea of design patterns in software engineering is to have a general and reusable solution to commonly occurring problems.  In general, a design pattern is not necessarily a finished product, but rather a template on how to solve a problem which can be used in many different situations. The idea is to have some predefined solutions, and incorporate them into the development with some modification and/or instantiation.  With the design pattern tool we provide a semi-automatical way of reusing developed models in Event-B. Moreover, the typical elements that we are able to reuse are not only the models themselves, but also (more importantly) their correctness in terms of proofs associated with the models.
−
Early version of Rodin provided preferences for automatic tactics that enabled to reorder them, but the ordering was lost at each change: one could not record a particular tactic order in order to reuse it later.
 
  
−
Another issue is to have more than one possibility to combine the tactics. Indeed, the only implicit combination of tactics available consisted in trying to apply them in turn for every open node of a proof. In the proving area, there exists a notion of ''tactic combinators'', also called ''tacticals'', that allow to combine tactics in various specific manners, thus providing a sort of tactic arithmetic.
+
== Editors ==
  
−
The advanced preferences for auto-tactics solved these two issues.
+
This section concerns the actual editors that user work with to view and modify models.
  
−
== Isabelle Plug-in ==
+
''' Editor of the core platform '''<br>
−
{{TODO}} ''To be completed by Matthias Schmaltz''
 
−
== ProB Disprover ==
 
  
−
ProB can be used to find counterexamples to invariant preservation and deadlock preservation proof obligations.
+
Two major kinds of failures were faced when developing industrial sized models:
−
This feature relies on the constraint solving capabilities of the ProB kernel. It is available from the ProB plugin after loading an Event-B model.
+
:* Failures occurring on Windows platforms, the mostly used system, when reaching the operating system limit number of graphical elements in memory allowed to be displayed at once. This situation used to crash the Rodin platform, and it appeared necessary to control the number of graphical elements needed to display the model elements. Architectures sparing these graphical elements were thus favoured.
 +
:* Failures due to the high consumption of memory by the heavy graphical elements used by the forms of legacy editor.
 +
:Moreover, it appeared important to visualize some elements that are not part of the current level of modelling, but are linked to it, for example, the actions in an abstract event, or its guards. Such elements are called the "inherited" elements, or "implicit children". The legacy structured editor being directly interfaced with the underlying Event-B models in database, it was difficult and tricky to modify it in order to display inherited elements. This was one more argument to go for a new editor based on a intermediary representation of the models.
 +
:Another motivation to go for another editor was to get a more modest and ergonomic way to visualize and edit the models. The models being presented through styled text pretty printing and the edition tightly derived from a textual edition.
  
−
WIthin the context of WP2 (Transportation) ProB has also been used to try and find counterexamples to individual proof rules in the Siemens proof rule database.
+
''' Camille '''<br>
−
For this, the ProB command line tool has been extended to load proof rule files (using a Prolog parser to avoid the JVM startup time) and then applies the ProB constraint solver to try and find counter examples to each proof rule.
 
−
This work has already identified several errors in the Siemens rule database and the work is still ongoing.
 
−
A current issue is the addition of explicit well-definedness conditions into the proof rules, as well as the fact that some proof rules use substations inside predicates.
 
  
 +
Camille was developed as an alternative editor in 2009.  In contrast to the existing editor, this was a pure textual editor that supported standard features like copy and paste, auto-completion, color highlighting and many more.  In addition, it performed better than the existing structural editor.
  
 +
While successful, Camille offered only limited support for models with extended elements contributed by plug-ins.  Also, the underlying EMF Compare framework was problematic due to bugs and performance issues.
  
−
Mention work using Kodkod here ?
+
= Choices / Decisions =
 +
== Improved Performance ==
 +
SYSTEREL lead a two phase investigation to have a better idea of the work to be done. Each phase being followed by some refactoring of the code. Out of the early investigation, a cause and effect relationship has been found between performance loss and the various reported bugs, such as "platform hanging" bugs. Indeed, it appeared that solving the performance issues sometimes solved induced bugs as well, making the scalability improvement tasks encompass the maintenance goals.<br>
 +
Later, a deeper investigation was performed where profiling and code review were the two techniques used to tackle the issues left. The profiling strategy allowed to get a better localisation of the performance loss in both UI and core code while the code review helped to understand the intrinsic misuses or drawbacks of particular components and/or architectures. The proving UI was refactored in order to use a light textual representation.
  
−
== SMT Solver Integration ==
+
== Design Pattern Management / Generic Instantiation  ==
−
The integration of SMT solvers into the Rodin platform is motivated by two main reasons. On the one hand, the enhancement of its proving capability, especially in the field of arithmetics. On the other hand, the ability of extracting some useful informations from the proofs produced by these solvers, such as unsatisfiable cores, in order to significantly decrease the time necessary to prove a modified model.
+
In our notion of design patterns, a pattern is just a development in Event-B including an abstract model called specification and a refinement. During development there might be the possibility of applying a pattern that was already developed to the current development.  The steps of using the tool are as follows.<br>
 +
:'''Matching''' The developer the starts the design pattern plug-in and manually matches the specification of the pattern with the current development. In this linking of pattern and problem the developer has to define the which variable in the current development corresponds to each variable in the pattern specification. Furthermore the developer has to ensure the consistency of the variable matching by matching the events of the pattern specification with events in the development.<br>
 +
:'''Renaming''' Once the matching is done, the developer has the possibility to adapt the pattern refinement such as renaming the variables and events or merging events of the pattern refinement with uninvolved events of the development. Renaming can become mandatory there are name clashes, meaning the pattern refinement includes variable or events having the same name as existing elements in the development.<br>
  
−
= Choices / Decisions =
+
After adaptation of the pattern refinement the tool generates automatically a new Event-B machine as a refinement of the machine where the developer started the design pattern tool. The correctness of the generated machine being a refinement is guaranteed by the generation process of the tool.
−
== New rewriting and inference rules ==
 
−
{{TODO}} ''To be completed by Laurent Voisin''
 
−
== Advanced Preferences for Auto-tactics ==
 
  
−
Since Rodin 2.1, one can create his own tactic profiles. A tactic profile allows to set and record a particular order of chosen basic tactics. Furthermore, a profile can be applied either globally (as before), or specifically for a given project.
+
Design Patterns in Event-B are nothing else than ordinary Event-B models and are not restricted with respect to their size. Due to the fact that pattern and development have to be matched manually by the
 +
developer, the size of a pattern effects the usability. Furthermore, if the pattern is too specific either the pattern cannot be used in most situations or the developer is forced to tune its development
 +
such that a further appliance of the pattern is possible. A pattern-driven development could thus lead to models including needless elements that would have been avoided when developing without patterns.
  
−
Since Rodin 2.3, tacticals and parameterization have been added to the profiles, thus increasing the potential of such proving feature.
+
== Editors ==
−
A tactic profile may now be composed of tacticals, that combine any number of basic tactics and other profiles.
+
''' Rodin Editor '''<br>
−
The parameterization allows for example to set a custom timeout on external provers such as AtelierB P1.
 
  
−
== Isabelle Plug-in ==
+
The Rodin Editor has been built on the basis of enhancements brought to the Proving UI. In fact, by using the same kind of textual component, every model element is presented as text, as would a pretty print do. The edition is made possible through the use of a unique additional graphical component that overlays the presentation of the element (to be edited).  It lighten the presentation, but also side steps the use of a significant amount of greedy graphical elements. Only two graphical elements are needed for presentation and edition: the model viewer and its overlay editor!<br>
−
{{TODO}} ''To be completed by Matthias Schmaltz''
+
The first public version (0.5.0) of the Rodin Editor has been released on the 13/07/2011 as a plug-in of the Rodin platform. This decision has been made in order to let the plug-in incubation for the time it is being tested and stated that no regression is introduced. The Rodin Editor since its version 0.6.1 is part of the Rodin core platform.
−
== ProB Disprover ==
 
  
−
Currently the constraint based invariant and deadlock checker is run from within the ProB plug-in and not from the prover interface on individual proof obligations.
+
''' Camille '''<br>
−
Indeed, for invariant preservation the disprover thus checks an event for all invariants, rather than being applied on individual proof obligations related to that event.
 
−
However, ProB does know which invariants have already been proven to be preserved by that particular event.
 
−
The rationale for running the invariant preservation checks in this way is that:
 
−
* the counterexample is a full valuation of the models variables and constants which can be displayed using the ProB interface,
 
−
* the invariants and guards truth values can be inspected in detail using the ProB interface, make the counter-example intelligible to the user,
 
−
* ProB can find out which of the axioms are theorems and ignore them. Indeed in the old ProB disprover approach all of the assumptions were fed, and ProB did not know which ones are relevant to find correct values for the constants and variables. In fact, some of the theorems turned out to be very complicated to check, and prevented ProB from finding counterexamples.
 
  
−
Similarly, the constraint-based deadlock checker is run from the ProB plug-in on a loaded model. As Rodin does not currently generate the deadlock freedom proof obligations, this was an obvious choice. Also, it enables the user to type in additional predicates to find "particularly interesting" counter examples (see ICLP'2011 article below).
+
Camille was quite successful, but due to the limited suitability for editing models using plug-ins, an architectural overhaul has been planned. The course of action was not obvious, however, as there are a number of possible architectures with varying advantages and disadvantages. Therefore, Ingo Weigelt at the University of Düsseldorf created a technical report<ref name="camille-arch-tech-report">http://cobra.cs.uni-duesseldorf.de/w/Special:Publication/Weigelt2012</ref> that analyzes the needs of the users and suggests a number of possible solutions.  In the FP7 project ADVANCE, a solution will be decided upon and implemented.
−
Also, another advantage is that, again, the counter example can be inspected using the ProB interface.
 
  
−
== SMT Solver Integration ==
+
= Available Documentation =
−
The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory.
+
Links for Improved Performance
−
Technically, the plug-in classes extend the existing XProverCall, XProverInput, XProverReasoner, AbstractLazilyConstrTactic and ITacticParametizer classes which make it easy to integrate new tactics, reasoners and external prover calls.
+
:* There is a wiki page concerning the Rodin Performance<ref>http://wiki.event-b.org/index.php/Rodin_Performances</ref>.
 +
Links for Design Pattern Management / Generic Instantiation
 +
:* A paper concerning the generic instantiation is available<ref name="genInst1">Silva, Renato and Butler, Michael (2009) "Supporting reuse of Event-B developments through generic instantiation". In, International Conference on Formal Engineering Methods (ICFEM 09), Rio de Janeiro, Brazil, 09 - 12 Dec 2009. 19pp. (Submitted) http://eprints.soton.ac.uk/68737/</ref>
 +
:*An article about Pattern Management is published on the wiki<ref>http://wiki.event-b.org/index.php/Pattern</ref>.
 +
:*The article about Generic Instantiation on the wiki<ref>http://wiki.event-b.org/index.php/Generic_Instantiation</ref>
 +
Links for Edition
 +
:Two documentation pages have been created for the Rodin Editor:
 +
:* A general page describing the editor and how it works <ref name="RodinEditorPage">http://wiki.event-b.org/index.php/Rodin_Editor</ref>.
 +
:* A user guide page <ref name="RodinEditorUserManual">http://wiki.event-b.org/index.php/Rodin_Editor_User_Guide</ref>.
 +
: Moreover, a special category has been created on both SourceForge feature request<ref name="featTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651672</ref> and bug<ref name="bugTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651669</ref> trackers.
  
−
= Available Documentation =
+
Camille Documentation
−
* {{TODO}} Links for New rewriting and inference rules
+
* As the Camille text editor is based on the standard Eclipse editor, that documentation applies fully as well: <br>
−
* {{TODO}} Links for Advanced Preferences for Auto-tactics
+
help on Editors<ref>http://help.eclipse.org/indigo/topic/org.eclipse.platform.doc.user/concepts/concepts-6.htm Eclipse</ref>
−
* {{TODO}} Links for Isabelle Plug-in
+
* Additional information is available in the Text Editor<ref>http://wiki.event-b.org/index.php/Text_Editor</ref> section on the wiki.
−
* {{TODO}} Links for ProB Disprover
+
* The Rodin Handbook<ref>http://handbook.event-b.org/</ref> provides some basic usage information in a few places.
−
** [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HaLe2011 Constraint-Based Deadlock Checking of High-Level Specifications. In Proceedings ICLP'2011, Cambridge University Press, 2011.]
+
* The technical report<ref name="camille-arch-tech-report">http://cobra.cs.uni-duesseldorf.de/w/Special:Publication/Weigelt2012</ref> describes analysis of user's needs and possible solutions.
−
* {{TODO}} Links for SMT Solver Integration
 
  
 
= Status =
 
= Status =
−
== New rewriting and inference rules ==
+
== Improved Performance ==
−
{{TODO}} ''To be completed by Laurent Voisin''
+
The refactoring made on both core code and UI code allowed to gain up to 25 times speed-up on the UI (as described below),<br>
−
== Advanced Preferences for Auto-tactics ==
+
[[Image:800px-Rodin_Performances_Core_perf_simple3_nos.png|700px|link=Rodin Performances|General Platform Performances]]<br>
 +
and almost a 2 times speed-up in the core code, making the platform usable in an industrial sized context.<br>
 +
[[Image:Rodin_Performances_Editor_perf_simplev2_nos.png|850px|Rodin Proof Editor Performances]]
 +
 
 +
== Design Pattern Management / Generic Instantiation  ==
 +
The Generic Instantiation plug-in is available in version 0.2.1 for Rodin 2.4 and above from the main Rodin Update Site in the ''Composition and Decomposition'' category.
  
−
Advanced Preferences for Auto-tactics are functional in Rodin 2.3. This release provides a first set of tacticals and parameterization options.
+
== Editors ==
  
−
Further releases may offer additional tacticals and options, according to user feedback.
+
''' Rodin Editor '''
  
−
== Isabelle Plug-in ==
+
The Rodin Editor is part of the Rodin platform since Rodin 2.4 released by end of January 2012.
−
{{TODO}} ''To be completed by Matthias Schmaltz''
 
−
== ProB Disprover ==
 
  
−
The ProB constraint-based invariant and deadlock checkers are available in the current release of ProB for Rodin. The deadlock checker has been applied successfully on a very large industrial model within WP1 (automotive).
+
''' Camille '''
−
There is of course always the scope to improve the capabilities of the tool by improving the constraint solving capabilities.
 
−
In particular, further simplification of existential quantifiers will be important for the deadlock checker to be applied effectively on certain models.
 
  
−
The Siemens proof rule database validation work is still ongoing.
+
Camille has been quite successful, and besides a number of bug fixes and some performance profiling and tuning, the code base has not changed much.
−
This work has already identified several errors in the Siemens rule database.
 
−
However, a current issue is the addition of explicit well-definedness conditions into the proof rules, as well as the fact that some proof rules use substations inside predicates.
 
  
−
== SMT Solver Integration ==
+
= References =
−
{{TODO}} ''Laurent Voisin & Yoann Guyot''
+
<references/>
  
 
[[Category:D45 Deliverable]]
 
[[Category:D45 Deliverable]]

Revision as of 20:57, 20 April 2012

Overview

Three main domains concerned the scalability task during the last year of the project:
Improved Performance. According to the refocus mentioned in the General Platform Maintenance chapter, much of the reworking efforts performed on the core platform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed in a separate chapter.
Design pattern management / Generic Instantiation. Formal methods are applicable to various domains for constructing models of complex systems. However, often they lack some systematic methodological approaches, in particular in reusing existing models, for helping the development process. The objective in introducing design patterns within formal methods in general, and in Event-B in particular, is to overcome this limitation.
Editors. Along DEPLOY, edition became a central concern. Indeed, many usability issues appeard the models involved in pilots became "industrial" sized:

  • The legacy structured editor based on a form edition specific architecture reached its limits in editing such complex models. Industrial partners found this issue significant regarding the adoption of the Rodin platform in industry and providing a new structured editor correcting this issue became an important task during this last year of the DEPLOY project.
  • Camille textual editor had to tackle challenges related to resources mapping and management for projects of industrial size mentioned above or even the design of extension capabilities. Extension capabilities became a major concern since the grammar could be extended with theories.

Motivations

Improved Performance

Many issues concerning stability and performance were related to the core code of the Rodin platform, causing crashes, loss of data, corruption in models. Other issues were related to the UI causing platform hanging, and sometimes leading to its freezing which required sometimes to kill the Rodin process, thus also leading to potential loss of data and corruption in models. Addressing these issues before the end of DEPLOY was mandatory.

Design Pattern Management / Generic Instantiation

The idea of design patterns in software engineering is to have a general and reusable solution to commonly occurring problems. In general, a design pattern is not necessarily a finished product, but rather a template on how to solve a problem which can be used in many different situations. The idea is to have some predefined solutions, and incorporate them into the development with some modification and/or instantiation. With the design pattern tool we provide a semi-automatical way of reusing developed models in Event-B. Moreover, the typical elements that we are able to reuse are not only the models themselves, but also (more importantly) their correctness in terms of proofs associated with the models.

Editors

This section concerns the actual editors that user work with to view and modify models.

Editor of the core platform

Two major kinds of failures were faced when developing industrial sized models:

  • Failures occurring on Windows platforms, the mostly used system, when reaching the operating system limit number of graphical elements in memory allowed to be displayed at once. This situation used to crash the Rodin platform, and it appeared necessary to control the number of graphical elements needed to display the model elements. Architectures sparing these graphical elements were thus favoured.
  • Failures due to the high consumption of memory by the heavy graphical elements used by the forms of legacy editor.
Moreover, it appeared important to visualize some elements that are not part of the current level of modelling, but are linked to it, for example, the actions in an abstract event, or its guards. Such elements are called the "inherited" elements, or "implicit children". The legacy structured editor being directly interfaced with the underlying Event-B models in database, it was difficult and tricky to modify it in order to display inherited elements. This was one more argument to go for a new editor based on a intermediary representation of the models.
Another motivation to go for another editor was to get a more modest and ergonomic way to visualize and edit the models. The models being presented through styled text pretty printing and the edition tightly derived from a textual edition.

Camille

Camille was developed as an alternative editor in 2009. In contrast to the existing editor, this was a pure textual editor that supported standard features like copy and paste, auto-completion, color highlighting and many more. In addition, it performed better than the existing structural editor.

While successful, Camille offered only limited support for models with extended elements contributed by plug-ins. Also, the underlying EMF Compare framework was problematic due to bugs and performance issues.

Choices / Decisions

Improved Performance

SYSTEREL lead a two phase investigation to have a better idea of the work to be done. Each phase being followed by some refactoring of the code. Out of the early investigation, a cause and effect relationship has been found between performance loss and the various reported bugs, such as "platform hanging" bugs. Indeed, it appeared that solving the performance issues sometimes solved induced bugs as well, making the scalability improvement tasks encompass the maintenance goals.
Later, a deeper investigation was performed where profiling and code review were the two techniques used to tackle the issues left. The profiling strategy allowed to get a better localisation of the performance loss in both UI and core code while the code review helped to understand the intrinsic misuses or drawbacks of particular components and/or architectures. The proving UI was refactored in order to use a light textual representation.

Design Pattern Management / Generic Instantiation

In our notion of design patterns, a pattern is just a development in Event-B including an abstract model called specification and a refinement. During development there might be the possibility of applying a pattern that was already developed to the current development. The steps of using the tool are as follows.

Matching The developer the starts the design pattern plug-in and manually matches the specification of the pattern with the current development. In this linking of pattern and problem the developer has to define the which variable in the current development corresponds to each variable in the pattern specification. Furthermore the developer has to ensure the consistency of the variable matching by matching the events of the pattern specification with events in the development.
Renaming Once the matching is done, the developer has the possibility to adapt the pattern refinement such as renaming the variables and events or merging events of the pattern refinement with uninvolved events of the development. Renaming can become mandatory there are name clashes, meaning the pattern refinement includes variable or events having the same name as existing elements in the development.

After adaptation of the pattern refinement the tool generates automatically a new Event-B machine as a refinement of the machine where the developer started the design pattern tool. The correctness of the generated machine being a refinement is guaranteed by the generation process of the tool.

Design Patterns in Event-B are nothing else than ordinary Event-B models and are not restricted with respect to their size. Due to the fact that pattern and development have to be matched manually by the developer, the size of a pattern effects the usability. Furthermore, if the pattern is too specific either the pattern cannot be used in most situations or the developer is forced to tune its development such that a further appliance of the pattern is possible. A pattern-driven development could thus lead to models including needless elements that would have been avoided when developing without patterns.

Editors

Rodin Editor

The Rodin Editor has been built on the basis of enhancements brought to the Proving UI. In fact, by using the same kind of textual component, every model element is presented as text, as would a pretty print do. The edition is made possible through the use of a unique additional graphical component that overlays the presentation of the element (to be edited). It lighten the presentation, but also side steps the use of a significant amount of greedy graphical elements. Only two graphical elements are needed for presentation and edition: the model viewer and its overlay editor!
The first public version (0.5.0) of the Rodin Editor has been released on the 13/07/2011 as a plug-in of the Rodin platform. This decision has been made in order to let the plug-in incubation for the time it is being tested and stated that no regression is introduced. The Rodin Editor since its version 0.6.1 is part of the Rodin core platform.

Camille

Camille was quite successful, but due to the limited suitability for editing models using plug-ins, an architectural overhaul has been planned. The course of action was not obvious, however, as there are a number of possible architectures with varying advantages and disadvantages. Therefore, Ingo Weigelt at the University of Düsseldorf created a technical report[1] that analyzes the needs of the users and suggests a number of possible solutions. In the FP7 project ADVANCE, a solution will be decided upon and implemented.

Available Documentation

Links for Improved Performance

  • There is a wiki page concerning the Rodin Performance[2].

Links for Design Pattern Management / Generic Instantiation

  • A paper concerning the generic instantiation is available[3]
  • An article about Pattern Management is published on the wiki[4].
  • The article about Generic Instantiation on the wiki[5]

Links for Edition

Two documentation pages have been created for the Rodin Editor:
  • A general page describing the editor and how it works [6].
  • A user guide page [7].
Moreover, a special category has been created on both SourceForge feature request[8] and bug[9] trackers.

Camille Documentation

  • As the Camille text editor is based on the standard Eclipse editor, that documentation applies fully as well:

help on Editors[10]

  • Additional information is available in the Text Editor[11] section on the wiki.
  • The Rodin Handbook[12] provides some basic usage information in a few places.
  • The technical report[1] describes analysis of user's needs and possible solutions.

Status

Improved Performance

The refactoring made on both core code and UI code allowed to gain up to 25 times speed-up on the UI (as described below),
General Platform Performances
and almost a 2 times speed-up in the core code, making the platform usable in an industrial sized context.
Rodin Proof Editor Performances

Design Pattern Management / Generic Instantiation

The Generic Instantiation plug-in is available in version 0.2.1 for Rodin 2.4 and above from the main Rodin Update Site in the Composition and Decomposition category.

Editors

Rodin Editor

The Rodin Editor is part of the Rodin platform since Rodin 2.4 released by end of January 2012.

Camille

Camille has been quite successful, and besides a number of bug fixes and some performance profiling and tuning, the code base has not changed much.

References

  1. ↑ 1.0 1.1 http://cobra.cs.uni-duesseldorf.de/w/Special:Publication/Weigelt2012
  2. ↑ http://wiki.event-b.org/index.php/Rodin_Performances
  3. ↑ Silva, Renato and Butler, Michael (2009) "Supporting reuse of Event-B developments through generic instantiation". In, International Conference on Formal Engineering Methods (ICFEM 09), Rio de Janeiro, Brazil, 09 - 12 Dec 2009. 19pp. (Submitted) http://eprints.soton.ac.uk/68737/
  4. ↑ http://wiki.event-b.org/index.php/Pattern
  5. ↑ http://wiki.event-b.org/index.php/Generic_Instantiation
  6. ↑ http://wiki.event-b.org/index.php/Rodin_Editor
  7. ↑ http://wiki.event-b.org/index.php/Rodin_Editor_User_Guide
  8. ↑ https://sourceforge.net/tracker/?group_id=108850&atid=651672
  9. ↑ https://sourceforge.net/tracker/?group_id=108850&atid=651669
  10. ↑ http://help.eclipse.org/indigo/topic/org.eclipse.platform.doc.user/concepts/concepts-6.htm Eclipse
  11. ↑ http://wiki.event-b.org/index.php/Text_Editor
  12. ↑ http://handbook.event-b.org/
Retrieved from ‘https://wiki.event-b.org/index.php?title=D45_Prover_Enhancement&oldid=3352’