imported>Colin |
imported>Im06r |
| Line 1: |
Line 1: |
| − | == Core Rodin platform (Thomas Muller) == | + | == Overview == |
| | + | Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions). |
| | | | |
| − | === Overview ===
| + | The Theory plugin provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. The theory component is used to hold mathematical extensions (datatypes, operators with direct definitions, operators with recursive definitions and operators with axiomatic definitions), and proof extensions (polymorphic theorems, rewrite and inference rules). Theories are developed in the workspace (akin to models), and are subject to static checking and proof obligation generation. Proof obligations generated from theories ensure any contributed extensions do not compromise the soundness of the existing infrastructure for modelling and proof. In essence, the Theory plugin provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations. |
| − | {{TODO|Fill this paragraph.}}
| |
| − | | |
| − | === Motivations / Decisions ===
| |
| − | {{TODO|Fill this paragraph.}}
| |
| | | | |
| − | === Available Documentation === | + | == Motivations / Decisions == |
| | {{TODO|Fill this paragraph.}} | | {{TODO|Fill this paragraph.}} |
| | | | |
| − | === Planning === | + | == Available Documentation == |
| | {{TODO|Fill this paragraph.}} | | {{TODO|Fill this paragraph.}} |
| | | | |
| − | | + | == Planning == |
| − | | + | Issam Maamria will not be part of Advance after July 31, 2012. |
| − | == UML-B Improvements (Colin Snook, Vitaly Savicks) == | |
| − | | |
| − | === Overview ===
| |
| − | | |
| − | 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.
| |
| − | | |
| − | === Motivations / Decisions ===
| |
| − | | |
| − | The implementation of the UML-B tool is structured to provide re-usable features as much as possible. To achieve this, wherever possible, generic frameworks are developed and the implementation of specific diagram tools is minimised by utilising these frameworks. The following frameworks are now in use by UML-B and available as a basis for future diagrammatic modelling notations.
| |
| − | | |
| − | * The Event-B EMF framework provides an EMF basis for Event-B models (developed during the Deploy project).
| |
| − | ** Provides an EMF representation of Event-B models with persistance into the Rodin database.
| |
| − | * 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).
| |
| − | ** 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.
| |
| − | * 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.
| |
| − | | |
| − | === Available Documentation ===
| |
| − | | |
| − | [reference Fontainebleau Rodin workshop paper on Generic frameworks]
| |
| − | | |
| − | Wiki pages for developers using the Generic extensions and Diagrams frameworks.
| |
| − | http://wiki.event-b.org/index.php/EMF_framework_for_Event-B
| |
| − | http://wiki.event-b.org/index.php/Generic_Event-B_EMF_extensions (Under Construction)
| |
| − | | |
| − | [reference Dusseldorf Rodin workshop paper on Event-B Statemachines]
| |
| − | Wiki pages for users of UML-B
| |
| − | http://wiki.event-b.org/index.php/UML-B
| |
| − | | |
| − | === Planning ===
| |
| − | | |
| − | The following work is planned:
| |
| − | * 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.
| |
| − | * 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.
| |
| − | * 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) ==
| |
| − | | |
| − | === Overview ===
| |
| − | {{TODO|Fill this paragraph.}}
| |
| − | | |
| − | === Motivations / Decisions ===
| |
| − | {{TODO|Fill this paragraph.}}
| |
| − | | |
| − | === Available Documentation ===
| |
| − | {{TODO|Fill this paragraph.}}
| |
| − | | |
| − | === Planning ===
| |
| − | {{TODO|Fill this paragraph.}}
| |
| − | | |
| − | | |
| − | | |
| − | == 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 == |
Overview
Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions).
The Theory plugin provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. The theory component is used to hold mathematical extensions (datatypes, operators with direct definitions, operators with recursive definitions and operators with axiomatic definitions), and proof extensions (polymorphic theorems, rewrite and inference rules). Theories are developed in the workspace (akin to models), and are subject to static checking and proof obligation generation. Proof obligations generated from theories ensure any contributed extensions do not compromise the soundness of the existing infrastructure for modelling and proof. In essence, the Theory plugin provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.
Motivations / Decisions
TODO: Fill this paragraph.
Available Documentation
TODO: Fill this paragraph.
Planning
Issam Maamria will not be part of Advance after July 31, 2012.
References
