Difference between pages "D45 Code Generation" and "D45 Scalability"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Tommy
 
Line 1: Line 1:
 
= Overview =
 
= Overview =
−
The code generation plug-in allows the generation of code for typical real-time embedded control software from refined Event-B models. Such feature would be an important factor in ensuring eventual deployment of the DEPLOY approach within industrial organisations.
+
'''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>
 +
'''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 =
−
DEPLOY industrial partners are interested in the formal development of multi-tasking, embedded control systems. During the project, work has been undertaken to investigate automatic generation, from Event-B models, for these type of systems. Initially, we chose to translate to the Ada programming language, and use it as a basis for the abstractions used in our approach. The first version of the code generator supported translation to Ada, and the current version also has limited support for C.
+
 
 +
== 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 '''<br>
 +
 
 +
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 '''<br>
 +
 
 +
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 =
 
= Choices / Decisions =
−
We described our previous code generation feature as a demonstrator tool; chiefly a tool designed as a proof of concept, used by us to validate the approach. In this sense, the tool as it stands now, is the first prototype intended to be used by developers. However, we can use the demonstrator as a baseline, and describe the new features as follows:
+
== 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 which made 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.
  
−
* Tasking Event-B is now integrated with the Event-B explorer. It uses the extensibility mechanism of Event-B EMF (In the previous version it was a separate model).
+
== Design Pattern Management / Generic Instantiation  ==
−
* Tasking Event-B is now integrated with the Event-B model editors. Tasking Event-B features can now be edited in the same place as the other Event-B features.
+
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>
−
* We have the ability to translate to Java and C, in addition to Ada source code; and the source code is placed in appropriate files within the project.
+
:'''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>
−
* We use theories to define translations of the Event-B mathematical language (Theories for Ada and C are supplied).
+
:'''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>
−
* We use the theory plug-in as a mechanism for defining new data types , and the translations to target data types.
 
−
* The Tasking Event-B to Event-B translator is fully integrated. The previous tool generated a copy of the project, but this is no longer the case.
 
−
* The translator is extensible.
 
−
* The composed machine component is used to store event 'synchronizations'.
 
−
* Minimal use is made of the EMF tree editor in Rose.
 
  
−
== Tasking Event-B and Editing ==
+
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.
−
A text-based task body editor was added, to minimize the amount of editing required with the EMF tree editor. The task body editor is associated with a parser-builder; after the text is entered in the editor the EMF representation is generated (by clicking a button) that is, assuming parsing is successful. If the parser detects an error, information about the parse error is displayed in an adjoining text box. When specifying events in the task body, there is no longer a need to specify two events involved in a synchronization. The code generator automatically finds the corresponding event of a synchronization, based on the event name, and using the composed machine component. Composed machines are used to store event 'synchronizations', and 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 new feature also overcomes the 'problem' that we previously experienced, with duplicate event names in a development, and event selection, when specifying the task body. The EMF tree editor in Rose is now only used minimally; to add annotations for Tasking, Shared and Environ Machines; typing annotations, and parameter direction information; and sensing/actuating annotations, where necessary. Further work is under way to integrate the code generation feature with the new Rodin editor.
 
  
−
== Allowing Extensibility ==
+
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
−
The code generation approach is now extensible; in that, 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. 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.
+
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.
  
−
== Targeting new Languages ==
+
== Editors ==
−
Making the step from Event-B to code is a process that can be aided through automatic code generation.
+
''' Rodin Editor '''<br>
−
The code generation plug-in for Rodin is a new tool for translating Event-B models to concurrent programmes.
 
−
However users of such a tool will likely require a diverse range of target languages and target platforms, for which we do not currently provide translations.Some of these languages may be subtly different to existing languages and only have modest differences between the translation rules, for example C and C++, whilst others may have more fundamental differences. As the translation from Event-B to executable code is non-trivial and to reduce the likelihood of error, we want to generalize as much of the translation as possible so that existing translation rules are re-used.
 
−
Therefore significant effort is needed to ensure that such a translation tool is extensible to allow additional languages to be included with relative ease. Here we concentrate on translation from a previously defined Common Language Meta-model, the intermediary language IL1, which Event-B translates to directly. IL1 is an EMF metamodel representation of generic properties and functionality found in many programming languages. It has representations for key structural concepts such as variables, subroutines, function calls and parameters. The translation of predicates and expressions contained within the code are handled by a new extension to the theory plug-in, which allows translation rules to be developed for specific target languages within the Rodin environment. The generic nature of the intermediary language is designed to allow for a wide range of different target languages. Developers of new target languages are required to write translators in Java for the conversion from the EMF representation to the code of their target language. To do this we provide a central translation manager, that takes an IL1 model and automatically calls the appropriate translators for each element of the model, whilst also providing the link to the predicate and expression translators provided by the new theory plug-in. The developer registers their translators for the target language through an extension point, where currently there are 15 light-weight translators required for a new target language.
 
−
To aid the developer, we provide abstract translators for each required element in the IL1 model that has to be translated. These translators perform the majority of the translation automatically, meaning that in most cases all the developer is required to do is format strings into the appropriate structure for their target language.
 
−
For example in an branch statement, the developer would be required to write a method stating how a branch is defined and structured in their language, using a set of previously translated guard conditions and actions.
 
−
Importantly, the flexibility remains for the developer to re-write any of the translations if the ones provided are not suitable.
 
  
−
== Using Abstract Translators ==
+
The Rodin Editor, has been built on the basis of the improvements made to the Proving UI. In fact, the textual component used, the SWT StyledText, allowed to describe every model element 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 edit. It lightened the presentation, but also side stepped the use of a significant amount of greedy graphical because at most two of them are needed: the model viewer and its overlay editor!<br>
−
To test our approach, we have built translators for C, Ada and Java using the same underlying abstract translators.  
+
The first public version (0.5.0) of the Rodin Editor as 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.
−
Additionally we consider the case where a new language may be required that has only modest differences to an existing language. A good example of this is to consider the case where a different library may want to be used from one used in an existing translation. For instance in C, concurrency can be achieved through different mechanisms such as OpenMP or Pthreads. In this case it may be that all but the mechanism for handling a subroutine call are the same, meaning that the majority of the translation can occur using common translators, with separate translators for the different methods of handling a subroutine call. To allow for this we allow the developer to assign a core and specialisation language to each translator they build. In cases where a translator for the specialisation language does not exist, the translator will automatically defer to the default core language translator, if one exists. This means that default translators for a particular core language can be written for the majority of the translation, with specialisations being provided where differences occur. The core and specialisation of the language is also reflected in the theory translator, meaning that language theories are only required for the core languages, rather than for each individual specialization.
+
 
 +
''' Camille '''<br>
 +
 
 +
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 architecture 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.
  
 
= Available Documentation =
 
= Available Documentation =
−
[[TODO]] ''By Andy''
+
* Links for Improved Performance
 +
:*[http://wiki.event-b.org/index.php/Rodin_Performances Rodin Performance]
 +
* Links for Design Pattern Management / Generic Instantiation
 +
:* Silva, Renato and Butler, Michael (2009) "Supporting reuse of Event-B developments through generic instantiation"<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>
 +
:*The article about Pattern Management on the wiki[http://wiki.event-b.org/index.php/Pattern]
 +
:*The article about Generic Instantiation on the wiki[http://wiki.event-b.org/index.php/Generic_Instantiation]
 +
* 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
 +
 
 +
* Camille Documentation
 +
** As the Camille text editor is based on the standard Eclipse editor, that documentation applies fully as well: [http://help.eclipse.org/indigo/topic/org.eclipse.platform.doc.user/concepts/concepts-6.htm Eclipse Help on Editors]
 +
** Additional information is available in the [http://wiki.event-b.org/index.php/Text_Editor Text Editor] Section on the wiki
 +
** The [http://handbook.event-b.org/ Rodin Handbook] provides some basic usage information in a few places
 +
** The technical report<ref name="camille-arch-tech-report">http://cobra.cs.uni-duesseldorf.de/w/Special:Publication/Weigelt2012</ref> describing analysis of user's needs and possible solutions
  
 
= Status =
 
= 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),<br>
 +
[[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.
 +
 +
== Editors ==
 +
 +
=== Rodin Editor ===
 +
 +
The Rodin Editor is part of the Rodin platform since Rodin 2.4 released by end of January 2012.
 +
 +
=== Camille ===
  
−
We released a new version of the code generator on 22-03-2012. We have made changes to the methodology, user interface, and tooling. The code generators have been completely re-written. The translators are now implemented using Java only. In our previous work we attempted to make use of the latest model-to-model transformation technology, available in the Epsilon tool set, but we decided to revert to Java since Epsilon lacked the debugging and productivity features of the Eclipse Java editor. We have also updated the documentation, including the Tasking Event-B Overview, and Tutorial materials.
+
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 =
 
= References =

Revision as of 13:44, 19 April 2012

Overview

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 which made 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 the improvements made to the Proving UI. In fact, the textual component used, the SWT StyledText, allowed to describe every model element 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 edit. It lightened the presentation, but also side stepped the use of a significant amount of greedy graphical because at most two of them are needed: the model viewer and its overlay editor!
The first public version (0.5.0) of the Rodin Editor as 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 architecture 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
  • Links for Design Pattern Management / Generic Instantiation
  • Silva, Renato and Butler, Michael (2009) "Supporting reuse of Event-B developments through generic instantiation"[2]
  • The article about Pattern Management on the wiki[1]
  • The article about Generic Instantiation on the wiki[2]
  • Links for Edition
Two documentation pages have been created for the Rodin Editor:
  • A general page describing the editor and how it works [3]
  • A user guide page [4]
Moreover, a special category has been created on both SourceForge feature request[5] and bug[6] trackers
  • Camille Documentation
    • As the Camille text editor is based on the standard Eclipse editor, that documentation applies fully as well: Eclipse Help on Editors
    • Additional information is available in the Text Editor Section on the wiki
    • The Rodin Handbook provides some basic usage information in a few places
    • The technical report[1] describing 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. ↑ 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/
  3. ↑ http://wiki.event-b.org/index.php/Rodin_Editor
  4. ↑ http://wiki.event-b.org/index.php/Rodin_Editor_User_Guide
  5. ↑ https://sourceforge.net/tracker/?group_id=108850&atid=651672
  6. ↑ https://sourceforge.net/tracker/?group_id=108850&atid=651669
Retrieved from ‘https://wiki.event-b.org/index.php?title=D45_Code_Generation&oldid=3343’