imported>Fabian |
imported>Colin |
| Line 1: |
Line 1: |
| − | {{TOCright}}
| + | === Overview === |
| − | This page sum up the known developments that are being done around or for the [[Rodin Platform]]. ''Please contributes informations about your own development to keep the community informed'' | + | This part of the deliverable describes improvements to the UML-B plug-in feature, which is the responsibility of University of Southampton. |
| | | | |
| − | == Deploy Tasks ==
| + | A new plug-in feature has been developed to provide Animation of UML-B State-machine diagrams. This feature was developed by University of Southampton. |
| − | The following tasks were planned at some stage of the [[Deploy]] project.
| |
| − | === Core Platform ===
| |
| − | ==== New Mathematical Language ====
| |
| − | ==== Rodin Index Manager ====
| |
| − | [[Systerel]] is in charge of this task.
| |
| − | {{details|Rodin Index Design|Rodin index design}}
| |
| | | | |
| − | The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them. | + | The longer term development of UML-B relies on an EMF representation of Event-B. The development of a new EMF Event-B plugin-in feature is also described in this section. This feature was initially developed by University of Southampton, Heinrich-Heine University, Duesseldorf and University of Newcastle. It is now mostly maintained and developed by University of Southampton. |
| | | | |
| − | ==== Text Editor ==== | + | === Motivations === |
| − | The efforts in [[Düsseldorf]] ([[User:Fabian|Fabian]]) and [[Newcastle]] ([[User:Alexei|Alexei]]) have been joined to create a single text editor which will be part of the [[#EMF framework for Rodin|EMF framework for Rodin]] (see that [[#EMF framework for Rodin|section]] for details).
| + | This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits. |
| | | | |
| − | ==== EMF framework for Rodin ==== | + | ====UML-B improvements==== |
| − | Newcastle, Southampton and Düsseldorf have begun to develop an EMF framework to support Rodin modelling tools based on EMF. The framework includes an EMF representation of Event-B, a synchronising persistence interface for loading and saving models via the Rodin API and facilities to support text editing and parsing. Examples of tools that will be based on the EMF framework for Rodin are, a Text editor, a compare/merge editor (which can be used for team based development), pattern/composition tools, Diagram Editors.
| + | The current version of the UML-B tool has been improved to support the refinement of State-machines. At the last deliverable, refinement of Classes was supported and State-machine refinement was beginning to be investigated. The investigation experimented with several notation and methodological alternatives. The design has now been finalised and an implementation has now been achieved. State-machines can be refined by adding nested state-machines inside states. Some of the transitions in the nested state-machine do not represent new events but contribute to the refinements of existing transitions in the parent state-machine. A concept of ''transition elaboration'' has been invented to represent this relationship. |
| | | | |
| − | More details can be found here: [[EMF framework for Rodin]]
| + | Many other minor improvements have been made to the UML-B tool including: |
| | + | collapsing empty compartments on diagrams, |
| | + | improved navigation between diagrams, |
| | + | improved properties views |
| | + | ability to order classes and class-types in the translation |
| | + | support for theorems everywhere (i.e. invariants and axioms can now be designated as theorems) |
| | | | |
| − | === Plug-ins === | + | ====UML-B State-machine Animation==== |
| − | ==== Requirement Management Plug-in ====
| + | This feature was developed in response to a requirement from Seimens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state. |
| − | [[User:Jastram|Michael]] at [[Düsseldorf]] is in charge of the [[:Category:Requirement Plugin|Requirements Management Plug-in]].
| |
| | | | |
| − | {{See also|ReqsManagement|Requirements Tutorial|l1=Requirements Management Plug-in}}
| + | ====EMF Framework for Event-B==== |
| | | | |
| − | This plug-in allows: | + | === Choices / Decisions === |
| − | * Requirements to be edited in a set of documents (independently from Rodin)
| + | This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices. |
| − | * Requirements to be viewed within Rodin
| |
| − | * Individual Requirements to be linked to individual Event-B-Entities
| |
| − | * A basic completion test to be performed
| |
| | | | |
| − | ==== UML-B Plug-in ==== | + | === Available Documentation === |
| − | [[Southampton]] is in charge of [[UML-B]] plug-in.
| |
| | | | |
| − | * Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.
| + | UML-B Refinement is described in a paper which was presented at the FM2009 conference in Eindhoven. It is available here:- http://eprints.ecs.soton.ac.uk/18268/ |
| | | | |
| − | *Allow user to allocate the name of the 'implicit contextual instance' used in a class. Events and Transitions owned by a class are implicitly acting upon an instance of the class which has formerly been denoted by the reserved word 'self'. This modification allows the modeller to override 'self' (which is now the default name) with any other identifier. This feature is needed to avoid name clashes when synchronising transitions into a single event. It also allows events to be moved between different classes (or outside of all classes) during refinement without creating name clashes.
| + | A tutorial on how to refine state-machines is available on the wiki: [[Refinement_of_Statemachines]] |
| | | | |
| − | * Better support for state machine refinement in UML-B. This revision to UML-B allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines.
| |
| | | | |
| − | ==== ProB Plug-in ====
| + | State-machine animation is described on the wiki here:- [[UML-B_-_Statemachine_Animation]] |
| − | [[Düsseldorf]] is in charge of [[ProB]].
| |
| − | <!-- {{details|ProB current developments|ProB current developments}} -->
| |
| | | | |
| − | ===== Work already performed =====
| + | It is also available as a short paper here:- http://eprints.ecs.soton.ac.uk/18261/ |
| | | | |
| − | We have now ported ProB to work directly on the Rodin AST. Animation is working and the user can now set a limited number of preferences.
| |
| − | The model checking feature is now also accessible.
| |
| − | It is also possible to create CSP and classical B specification files. These files can be edited with BE4 and animated/model checked with ProB.
| |
| − | On the classical B side we have moved to a new, more robust parser (which is now capable of parsing some of the more complicated AtelierB
| |
| − | specifications from Siemens).
| |
| | | | |
| − | On the developer side, we have moved to a continuous integration infrastructure using CruiseControl. Rodin is also building from CVS in that infrastructure.
| + | The EMF Framework for Event-B is described on the wiki here:- [[EMF_framework_for_Event-B]] |
| | | | |
| − | ===== Ongoing and future developments=====
| + | It is also available as a short paper here:- http://eprints.ecs.soton.ac.uk/18262/ |
| | | | |
| − | We are currently developing a new, better user interface.
| + | === Planning === |
| − | We also plan to support multi-level animation with checking of the gluing invariant.
| + | This paragraph shall give a timeline and current status (as of 29 Jan 2010). |
| − | | |
| − | We have prototypes for several extensions working, but they need to be fully tested and integrated into the plugin:
| |
| − | * an inspector that allows the user to inspect complex predicates (such as invariants or guards) as well as expressions in a tree-like manner
| |
| − | * a graphical animator based on SWT that allows the user to design his/her own animations easily within the tool
| |
| − | * a 2D viewer to inspect the state space of the specification
| |
| − | | |
| − | ==== B2Latex Plug-in ====
| |
| − | [[Southampton]] is in charge of [[B2Latex]].
| |
| − | | |
| − | Kriangsak Damchoom will update the plug-in to add [[Event Extension|extensions of events]].
| |
| − | | |
| − | ==== Parallel Composition Plug-in ====
| |
| − | [[Southampton]] is in charge of the [[Parallel Composition using Event-B]] .
| |
| − | | |
| − | The intention of the plug-in is to allow the parallel composition of events using Event-B syntax. The composition uses a value-passing style (shared event composition), where parameters can be shared/merged.
| |
| − | | |
| − | This plug-in allows:
| |
| − | * Selection of machines that will be part of the composition (''Includes'' Section)
| |
| − | * Possible selection of an abstract machine (''Refines'' Section)
| |
| − | * Possible inclusion of invariants that relate the included machines (''Invariant'' Section and use of the monotonicity )
| |
| − | * Invariants of included machines are conjoined.
| |
| − | * Selection of events that will be merged. The event(s) must come from different machines. At the moment, events with parameters with same name are merged. If it is a refinement composition, it is possible to choose the abstract event that is being refined.
| |
| − | * Initialisation event is the parallel composition of all the included machines' initialisations.
| |
| − | * For a composed event, the guards are conjoined and the all the actions are composed in parallel.
| |
| − | | |
| − | Currently, after the conclusion of the composition machine, a new machine can be generated, resulting from the properties defined on the composition file. This allows proofs to be generated as well as a visualisation of the composition machine file. In the future, the intention is to make the validation directly on the composition machine file directly where proofs would be generated ( and discharged) - the new machine generation would be optional. An event-b model for the validation/generation of proofs in currently being developed. Another functionality which should be quite useful for the composition (but not restricted to that) is '''renaming''':
| |
| − | | |
| − | * while composing, two machines may have variables with the same name for instance (which is not allowed for this type of composition). In order to solve this problem, one would have to rename one of the variables in order to avoid the clash, which would mean change the original machine. A possible solution for that would be to rename the variable but just on composition machine file, keeping the original machine intact. A renaming framework designed and developed by Stefan Hallerstede and Sonja Holl exists currently although still on a testing phase. The framework was developed to be used in a general fashion (not constrained to event-b syntax). The idea is to extend the development of this framework and apply to Event-B syntax (current development).
| |
| − | | |
| − | There is a prototype for the composition plug-in available that works for Rodin 0.8.2. A release for the Rodin 0.9 is concluded and will be available from the Rodin Main Update Site soon, under 'Shared Event Composition' update.
| |
| − | | |
| − | ==== Refactoring Framework Plug-in ====
| |
| − | [[Southampton]] is in charge of the [[Refactoring Framework]].
| |
| − | | |
| − | The intention of the plug-in is to allow the renaming/refactoring of elements on a file (and possible related files). Although created to be used in a general way, the idea is to embed this framework on the Rodin platform, using Event-B syntax. This plug-in was initially designed and developed by Stefan Hallerstede and Sonja Holl.
| |
| − | | |
| − | This plug-in allows:
| |
| − | * Defining extensions that can be used to select related files.
| |
| − | * Defining extensions that can be used to rename elements based on the type of file.
| |
| − | * Renaming of elements on a file and possible occurrences on related files.
| |
| − | * Generating of a report of possible problems (clashes) that can occur while renaming.
| |
| − | | |
| − | == Exploratory Tasks ==
| |
| − | === One Single View ===
| |
| − | [[Maria]] is in charge of this exploratory work during is internship.
| |
| − | {{details|Single View Design|Single View Design}}
| |
| − | The goal of this project is to present everything in a single view in Rodin. So the user won't have to switch perspectives.
| |
| − | | |
| − | | |
| − | | |
| − | == Others ==
| |
| − | | |
| − | === AnimB ===
| |
| − | [[Christophe]] devotes some of its spare time for this plug-in.
| |
| − | {{details|AnimB Current Developments|AnimB Current Developments}}
| |
| − | The current developments around the [[AnimB]] plug-in encompass the following topics:
| |
| − | ;Live animation update
| |
| − | :where the modification of the animated event-B model is instantaneously taken into account by the animator, without the need to restart the animation.
| |
| − | ;Collecting history
| |
| − | :The history of the animation will be collected.
| |
| − | | |
| − | === Team-Based Development ===
| |
| − | | |
| − | ; Usage Scenarios
| |
| − | : In order to understand the problem properly, [http://www.stups.uni-duesseldorf.de/ Düsseldorf] created a number of usage [[Scenarios for Team-based Development]].
| |
| − | : A page as also been opened for [[Scenarios for Merging Proofs|merging proofs scenarios]].
| |
| − | [[Category:Work in progress]]
| |
| − | | |
| − | === B2C ===
| |
| − | This plug-in translates Event-B models to C source code, which may then be compiled using external C development tools. [[Steve]] wrote B2C with the specific purpose of translating the [http://dx.doi.org/10.1007/978-3-540-87603-8_21 MIDAS] model, an Event-B implementation of a Virtual Machine instruction set.
| |
| − | | |
| − | B2C supports a sub-set of Event-B that can be easily translated to C form. The user provides a final refinement step that does nothing except restate the model in this translatable form: symbolic constants must be replaced by their literal values, range membership guards are replaced by greater-than and less-than guards, and actions are restated not to use global statments on their left-sides (this because the variable may have been modified by an earlier action, and may not be valid). The manipulations are done within EventB where they can be checked by the Proof Obligation system, and B2C made as simple as possible to maximise reliability. This re-write process is currently a manual step, but could in principle be done by another plug-in
| |
| − | | |
| − | B2C source code is not currently available for download: contact [[Steve]] directly if it is required.
| |
Overview
This part of the deliverable describes improvements to the UML-B plug-in feature, which is the responsibility of University of Southampton.
A new plug-in feature has been developed to provide Animation of UML-B State-machine diagrams. This feature was developed by University of Southampton.
The longer term development of UML-B relies on an EMF representation of Event-B. The development of a new EMF Event-B plugin-in feature is also described in this section. This feature was initially developed by University of Southampton, Heinrich-Heine University, Duesseldorf and University of Newcastle. It is now mostly maintained and developed by University of Southampton.
Motivations
This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.
UML-B improvements
The current version of the UML-B tool has been improved to support the refinement of State-machines. At the last deliverable, refinement of Classes was supported and State-machine refinement was beginning to be investigated. The investigation experimented with several notation and methodological alternatives. The design has now been finalised and an implementation has now been achieved. State-machines can be refined by adding nested state-machines inside states. Some of the transitions in the nested state-machine do not represent new events but contribute to the refinements of existing transitions in the parent state-machine. A concept of transition elaboration has been invented to represent this relationship.
Many other minor improvements have been made to the UML-B tool including:
collapsing empty compartments on diagrams,
improved navigation between diagrams,
improved properties views
ability to order classes and class-types in the translation
support for theorems everywhere (i.e. invariants and axioms can now be designated as theorems)
UML-B State-machine Animation
This feature was developed in response to a requirement from Seimens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.
EMF Framework for Event-B
Choices / Decisions
This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.
Available Documentation
UML-B Refinement is described in a paper which was presented at the FM2009 conference in Eindhoven. It is available here:- http://eprints.ecs.soton.ac.uk/18268/
A tutorial on how to refine state-machines is available on the wiki: Refinement_of_Statemachines
State-machine animation is described on the wiki here:- UML-B_-_Statemachine_Animation
It is also available as a short paper here:- http://eprints.ecs.soton.ac.uk/18261/
The EMF Framework for Event-B is described on the wiki here:- EMF_framework_for_Event-B
It is also available as a short paper here:- http://eprints.ecs.soton.ac.uk/18262/
Planning
This paragraph shall give a timeline and current status (as of 29 Jan 2010).
