ADVANCE D3.2 General Platform Maintenance: Difference between revisions
imported>Colin |
imported>Colin |
||
| Line 19: | Line 19: | ||
=== Overview === | === Overview === | ||
The UML-B plug-in is developed and maintained by the University of Southampton. 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 is already released in this version and a class diagram is now being developed as a prototype. | The UML-B plug-in is developed and maintained by the University of Southampton. 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 === | === Motivations / Decisions === | ||
Revision as of 13:48, 19 June 2012
Core Rodin platform (Thomas Muller)
Overview
TODO: Fill this paragraph.
Motivations / Decisions
TODO: Fill this paragraph.
Available Documentation
TODO: Fill this paragraph.
Planning
TODO: Fill this paragraph.
UML-B Improvements (Colin Snook, Vitaly Savicks)
Overview
The UML-B plug-in is developed and maintained by the University of Southampton. 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
TODO: Fill this paragraph.
Available Documentation
TODO: Fill this paragraph.
Planning
TODO: Fill this paragraph.
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 [1], 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 [1], 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: [1] The paper has been submitted to Science of Computer Programming.
- Requirements Traceability between Textual Requirements and Formal Models Using ProR: [2] The paper has been accepted for iFM'2012.
- Tutorial for the Rodin/ProR integration can be found here: [3].
- The User Guide containing an additional Tutorial for ProR can be found here: [4].
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, [1] 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
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.
