ADVANCE D3.3 General Platform Maintenance: Difference between revisions
imported>Colin |
imported>Nicolas m Fix title levels |
||
| Line 1: | Line 1: | ||
This part concerns the general maintenance performed on the Rodin toolset within the second year of the ADVANCE project. As the maintenance is a task that concerns the whole toolset, and to ease the reading of this part of the deliverable, the maintenance section has been decomposed in a list of subsections corresponding to scopes of the toolset. All these subsections maintain the template previously defined in the introduction. | This part concerns the general maintenance performed on the Rodin toolset within the second year of the ADVANCE project. As the maintenance is a task that concerns the whole toolset, and to ease the reading of this part of the deliverable, the maintenance section has been decomposed in a list of subsections corresponding to scopes of the toolset. All these subsections maintain the template previously defined in the introduction. | ||
= Core Rodin platform = | == Core Rodin platform == | ||
== Overview == | === Overview === | ||
The Rodin platform versions concerned by this deliverable are: | The Rodin platform versions concerned by this deliverable are: | ||
* 2.7 (released on 2012-11-05), | * 2.7 (released on 2012-11-05), | ||
| Line 13: | Line 13: | ||
{{TODO}} | {{TODO}} | ||
== Motivations / Decisions == | === Motivations / Decisions === | ||
'''Major version Rodin 3.0'''<br/> | '''Major version Rodin 3.0'''<br/> | ||
As the platform has grown in complexity, internal architecture needed adjustments in order to remain maintainable. The number of external plug-ins has increased too, raising need for core API improvements. The new major version Rodin 3.0 addresses these expectations. The API of the AST, prover tactics, have thus been reviewed. The platform code is now fully compatible with Eclipse 4. | As the platform has grown in complexity, internal architecture needed adjustments in order to remain maintainable. The number of external plug-ins has increased too, raising need for core API improvements. The new major version Rodin 3.0 addresses these expectations. The API of the AST, prover tactics, have thus been reviewed. The platform code is now fully compatible with Eclipse 4. | ||
| Line 19: | Line 19: | ||
{{TODO}} | {{TODO}} | ||
== Available Documentation == | === Available Documentation === | ||
The release notes, that appear and are maintained on the wiki, and that accompany each release, give useful information about the Rodin platforms. Moreover, two web trackers list and detail the known bugs and open feature requests: | The release notes, that appear and are maintained on the wiki, and that accompany each release, give useful information about the Rodin platforms. Moreover, two web trackers list and detail the known bugs and open feature requests: | ||
* a sourceforge bug tracker,<ref>http://sourceforge.net/tracker/?group_id=108850&atid=651669</ref> | * a sourceforge bug tracker,<ref>http://sourceforge.net/tracker/?group_id=108850&atid=651669</ref> | ||
| Line 26: | Line 26: | ||
Finally, a channel has been created on Youtube, in order to provide video tutorials about the use of the platform.<ref>http://www.youtube.com/user/EventBTv</ref> | Finally, a channel has been created on Youtube, in order to provide video tutorials about the use of the platform.<ref>http://www.youtube.com/user/EventBTv</ref> | ||
{{TODO}} | {{TODO}} | ||
== Planning == | === Planning === | ||
{{TODO}} | {{TODO}} | ||
= UML-B Improvements = | == UML-B Improvements == | ||
== Overview == | === Overview === | ||
UML-B provides a diagrammatic front end to Event-B to assist in constructing models. UML-B is UML-like. It is semantically and syntactically different from UML but should feel familiar to UML users. | UML-B provides a diagrammatic front end to Event-B to assist in constructing models. UML-B is UML-like. It is semantically and syntactically different from UML but should feel familiar to UML users. | ||
| Line 38: | Line 38: | ||
consists of a collection of diagrams which contribute additional modelling aspects to an extant Event-B machine (i.e. some of the modelling is still done in an Event-B machine). iUML-B currently provides a project diagram, and state-machine diagram. iUML-B class diagrams are currently under development and component diagrams are planned for future developemnt. The University of Southampton is responsible for UML-B. | consists of a collection of diagrams which contribute additional modelling aspects to an extant Event-B machine (i.e. some of the modelling is still done in an Event-B machine). iUML-B currently provides a project diagram, and state-machine diagram. iUML-B class diagrams are currently under development and component diagrams are planned for future developemnt. The University of Southampton is responsible for UML-B. | ||
== Motivations / Decisions == | === Motivations / Decisions === | ||
In general, classic UML-B is maintained but not substantially developed. Some improvements have been made in response to user requests. These include improved property fields for text entry and fixing a handles leak that causes problems on the Windows platform. | In general, classic UML-B is maintained but not substantially developed. Some improvements have been made in response to user requests. These include improved property fields for text entry and fixing a handles leak that causes problems on the Windows platform. | ||
| Line 50: | Line 50: | ||
* Classes, attributes and asssociations link to (elaborate) extisting data items (sets, constants or variables) that are in scope of the containing machine or context (via refines, sees or extends) | * Classes, attributes and asssociations link to (elaborate) extisting data items (sets, constants or variables) that are in scope of the containing machine or context (via refines, sees or extends) | ||
== Available Documentation == | === Available Documentation === | ||
{{TODO}} | {{TODO}} | ||
== Planning == | === Planning === | ||
{{TODO}} | {{TODO}} | ||
= Code generation = | == Code generation == | ||
== Overview == | === Overview === | ||
{{TODO}} | {{TODO}} | ||
== Motivations / Decisions == | === Motivations / Decisions === | ||
{{TODO}} | {{TODO}} | ||
== Available Documentation == | === Available Documentation === | ||
{{TODO}} | {{TODO}} | ||
== Planning == | === Planning === | ||
{{TODO}} | {{TODO}} | ||
= ProR = | == ProR == | ||
== Overview == | === Overview === | ||
The ProR/Rodin integration plugin is developed and maintained by Lukas Ladenberger and Michael Jastram at the University of Duesseldorf. ProR is a tool for working with requirements in natural language. It is part of the Eclipse Requirements Modeling Framework (RMF).<ref>http://www.eclipse.org/rmf/</ref> The goal of the ProR/Rodin integration plugin is to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. The ProR/Rodin integration plugin supports the user by maintaining a traceability between natural language requirements and formal models. | The ProR/Rodin integration plugin is developed and maintained by Lukas Ladenberger and Michael Jastram at the University of Duesseldorf. ProR is a tool for working with requirements in natural language. It is part of the Eclipse Requirements Modeling Framework (RMF).<ref>http://www.eclipse.org/rmf/</ref> The goal of the ProR/Rodin integration plugin is to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. The ProR/Rodin integration plugin supports the user by maintaining a traceability between natural language requirements and formal models. | ||
| Line 80: | Line 80: | ||
Other improvements will include more general improvements, such as usability, and any features required by the projects industrial partners. | Other improvements will include more general improvements, such as usability, and any features required by the projects industrial partners. | ||
== Motivations / Decisions == | === Motivations / Decisions === | ||
'''Phenomena Support''' | '''Phenomena Support''' | ||
| Line 90: | Line 90: | ||
While all required data structures exist to support the tracing method, the ProR/Rodin integration plugin would benefit from more sophisticated reporting. In particular, the tracing method lists a number of properties of a correct system description. For example, the existence of a trace between an artifact and its used phenomenon, or the fact that domain properties, requirement items and design decisions may only be expressed referring to phenomena that are visible in the environment, whereas design decisions and plaform properties may only be expressed referring to phenomena that are visible to the system. While the presence of such properties does not guarantee correctness, their absence indicates a problem. A ''requriements analyzer'' that lists all violations of those properties would be valuable to support the user by maintaining a system description of high quality. We developed a first system description for such requriements analyzer by means of the tracing method. We applied Event-B for modelling and validating the different artefacts of the system description and demonstrated how the formal model can be used as a first prototype in the early development phase. | While all required data structures exist to support the tracing method, the ProR/Rodin integration plugin would benefit from more sophisticated reporting. In particular, the tracing method lists a number of properties of a correct system description. For example, the existence of a trace between an artifact and its used phenomenon, or the fact that domain properties, requirement items and design decisions may only be expressed referring to phenomena that are visible in the environment, whereas design decisions and plaform properties may only be expressed referring to phenomena that are visible to the system. While the presence of such properties does not guarantee correctness, their absence indicates a problem. A ''requriements analyzer'' that lists all violations of those properties would be valuable to support the user by maintaining a system description of high quality. We developed a first system description for such requriements analyzer by means of the tracing method. We applied Event-B for modelling and validating the different artefacts of the system description and demonstrated how the formal model can be used as a first prototype in the early development phase. | ||
== Available Documentation == | === Available Documentation === | ||
* ''A Method and Tool for Tracing Requirements into Specifications''.<ref name="req1ref"/> Accepted for Science of Computer Programming. | * ''A Method and Tool for Tracing Requirements into Specifications''.<ref name="req1ref"/> Accepted for Science of Computer Programming. | ||
| Line 98: | Line 98: | ||
* The User Guide<ref>http://wiki.eclipse.org/RMF/User_Guide</ref> contains additional tutorials for ProR. | * The User Guide<ref>http://wiki.eclipse.org/RMF/User_Guide</ref> contains additional tutorials for ProR. | ||
== Planning == | === Planning === | ||
The following work is planned: | The following work is planned: | ||
| Line 105: | Line 105: | ||
*Applying the tracing method on the case studies of the industrial partners | *Applying the tracing method on the case studies of the industrial partners | ||
= Camille = | == Camille == | ||
== Overview == | === Overview === | ||
The Camille plug-in provides a textual editor for Rodin. This editor provides the same look and feel as a typical Eclipse text editor, including features most text editors provide, such as copy, paste, syntax highlighting and code completion. | The Camille plug-in provides a textual editor for Rodin. This editor provides the same look and feel as a typical Eclipse text editor, including features most text editors provide, such as copy, paste, syntax highlighting and code completion. | ||
The latest release finally supports the full core Event-B language as it is supported by the built-in editors too. | The latest release finally supports the full core Event-B language as it is supported by the built-in editors too. | ||
== Motivations / Decisions == | === Motivations / Decisions === | ||
A new version of the editor has been published to support the full feature of the core Event-B language. | A new version of the editor has been published to support the full feature of the core Event-B language. | ||
Event guards can now be defined as theorems as it is possible in the other Rodin editors. | Event guards can now be defined as theorems as it is possible in the other Rodin editors. | ||
| Line 120: | Line 120: | ||
With the new syntax all model elements now occur in the same order in every editor and pretty print. This finally lead to a more consistent modelling experience within the Rodin platform. | With the new syntax all model elements now occur in the same order in every editor and pretty print. This finally lead to a more consistent modelling experience within the Rodin platform. | ||
== Available Documentation == | === Available Documentation === | ||
* ''Architectures for an Extensible Text Editor for Rodin''.<ref name="Architectures_for_an_Extensible_Text_Editor_for_Rodin">http://www.stups.uni-duesseldorf.de/mediawiki/images/0/0a/Pub-Weigelt2012.pdf</ref> Bachelor thesis analysing the problem and discussing possible solutions. | * ''Architectures for an Extensible Text Editor for Rodin''.<ref name="Architectures_for_an_Extensible_Text_Editor_for_Rodin">http://www.stups.uni-duesseldorf.de/mediawiki/images/0/0a/Pub-Weigelt2012.pdf</ref> Bachelor thesis analysing the problem and discussing possible solutions. | ||
* An earlier version of the thesis has been published as a technical report<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/Weigelt2012></ref> that has been discussed on the Roding Developers Mailing List and the ADVANCE Progress Meeting in May 2012 in Paris. | * An earlier version of the thesis has been published as a technical report<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/Weigelt2012></ref> that has been discussed on the Roding Developers Mailing List and the ADVANCE Progress Meeting in May 2012 in Paris. | ||
== Planning == | === Planning === | ||
Camille still has the drawback of not supporting extensibility. It only supports the core Event-B language and plug-in-specific additions are simply ignored. Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions. | Camille still has the drawback of not supporting extensibility. It only supports the core Event-B language and plug-in-specific additions are simply ignored. Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions. | ||
A new version of Camille will be implemented during the ADVANCE project. Plug-in Developers will be able to provide syntax contributions and parsers for their extensions. By this users will be able to edit extended Event-B models solely through a text editor. | A new version of Camille will be implemented during the ADVANCE project. Plug-in Developers will be able to provide syntax contributions and parsers for their extensions. By this users will be able to edit extended Event-B models solely through a text editor. | ||
= References = | == References == | ||
<references/> | <references/> | ||
[[Category:ADVANCE D3.3 Deliverable]] | [[Category:ADVANCE D3.3 Deliverable]] | ||
Revision as of 12:34, 27 August 2013
This part concerns the general maintenance performed on the Rodin toolset within the second year of the ADVANCE project. As the maintenance is a task that concerns the whole toolset, and to ease the reading of this part of the deliverable, the maintenance section has been decomposed in a list of subsections corresponding to scopes of the toolset. All these subsections maintain the template previously defined in the introduction.
Core Rodin platform
Overview
The Rodin platform versions concerned by this deliverable are:
- 2.7 (released on 2012-11-05),
- 2.8 (released on 2013-06-20),
- 3.0 (TODO: ?).
During this second period of the ADVANCE project, the core developments have been focused on stability and design improvement. Thus, releases 2.7 and 2.8 mainly contain bug fixes, while version 3.0 prepares for future evolutions.
TODO
Motivations / Decisions
Major version Rodin 3.0
As the platform has grown in complexity, internal architecture needed adjustments in order to remain maintainable. The number of external plug-ins has increased too, raising need for core API improvements. The new major version Rodin 3.0 addresses these expectations. The API of the AST, prover tactics, have thus been reviewed. The platform code is now fully compatible with Eclipse 4.
TODO
Available Documentation
The release notes, that appear and are maintained on the wiki, and that accompany each release, give useful information about the Rodin platforms. Moreover, two web trackers list and detail the known bugs and open feature requests:
The Event-B wiki,[3] basic source of documentation for the users and developers of the Rodin toolset, was completed by the Rodin handbook, an ultimate source of documentation which reached completion by the end of the DEPLOY project. The handbook aimed to overcome the lack of a centralized source of information providing the necessary assistance to an engineer in the need to be productive using Event-B and minimize the access to an expert user. It is continuously maintained by the various actors involved in the environment of the Rodin toolset and is available as a PDF version, a HTML version, and help contents within Rodin. Both the Rodin handbook and the Event-B wiki represent the main source of documentation about Event-B and the Rodin toolset. Finally, a channel has been created on Youtube, in order to provide video tutorials about the use of the platform.[4] TODO
Planning
TODO
UML-B Improvements
Overview
UML-B provides a diagrammatic front end to Event-B to assist in constructing models. UML-B is UML-like. It is semantically and syntactically different from UML but should feel familiar to UML users. There are two variants of UML-B. Classic UML-B is self contained (i.e. all modelling is done on the diagram) and a read-only Event-B project is automatically generated for verification. Classic UML-B provides project diagrams to show the machine refinement structure, class diagrams to provide object oriented lifting and state-machine diagrams to provide event sequencing. The more recent iUML-B (i for integrated) consists of a collection of diagrams which contribute additional modelling aspects to an extant Event-B machine (i.e. some of the modelling is still done in an Event-B machine). iUML-B currently provides a project diagram, and state-machine diagram. iUML-B class diagrams are currently under development and component diagrams are planned for future developemnt. The University of Southampton is responsible for UML-B.
Motivations / Decisions
In general, classic UML-B is maintained but not substantially developed. Some improvements have been made in response to user requests. These include improved property fields for text entry and fixing a handles leak that causes problems on the Windows platform.
The development of iUML-B comprises improvement of the State-machines plug-in and development of a new class diagram plug-in.
The following improvements have been made to the state-machines plug-in:
The major features of the class-diagram plug-in are:
- Classes, attributes and asssociations link to (elaborate) extisting data items (sets, constants or variables) that are in scope of the containing machine or context (via refines, sees or extends)
Available Documentation
TODO
Planning
TODO
Code generation
Overview
TODO
Motivations / Decisions
TODO
Available Documentation
TODO
Planning
TODO
ProR
Overview
The ProR/Rodin integration plugin is developed and maintained by Lukas Ladenberger and Michael Jastram at the University of Duesseldorf. ProR is a tool for working with requirements in natural language. It is part of the Eclipse Requirements Modeling Framework (RMF).[5] The goal of the ProR/Rodin integration plugin is to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. The ProR/Rodin integration plugin supports the user by maintaining a traceability between natural language requirements and formal models.
Significant contributions to the latest version of the ProR/Rodin integration plugin have been made on phenomena support (maintaining a glossary and tracing phenomena) and the integration of the tracing method for producing a system description of high quality as presented in [6].
Other improvements will include more general improvements, such as usability, and any features required by the projects industrial partners.
Motivations / Decisions
Phenomena Support
System descriptions are composed of phenomena and artefacts: phenomena describe the state space and state transitions of an environment and a system, while artefacts describe constraints on the state space and the state transitions. A (concrete) collection of all phenomena of a system description is called glossary of phenomena. The user is now able to maintain a glossary of phenomena in the ProR/Rodin integration plugin. The phenomena are automatically available in the different artefacts. For instance, an auto complete feature is available to the user while editing an artefact. In addition the user can define synonyms for phenomena as well as custom colours for highlighting the different phenomena in the artefacts.
Tracing Method Integration
While all required data structures exist to support the tracing method, the ProR/Rodin integration plugin would benefit from more sophisticated reporting. In particular, the tracing method lists a number of properties of a correct system description. For example, the existence of a trace between an artifact and its used phenomenon, or the fact that domain properties, requirement items and design decisions may only be expressed referring to phenomena that are visible in the environment, whereas design decisions and plaform properties may only be expressed referring to phenomena that are visible to the system. While the presence of such properties does not guarantee correctness, their absence indicates a problem. A requriements analyzer that lists all violations of those properties would be valuable to support the user by maintaining a system description of high quality. We developed a first system description for such requriements analyzer by means of the tracing method. We applied Event-B for modelling and validating the different artefacts of the system description and demonstrated how the formal model can be used as a first prototype in the early development phase.
Available Documentation
- A Method and Tool for Tracing Requirements into Specifications.[6] Accepted for Science of Computer Programming.
- Requirements Traceability between Textual Requirements and Formal Models Using ProR.[7] The paper has been accepted for iFM'2012 & ABZ'2012.
- A Tutorial for the Rodin/ProR integration[8] can be found on the Event-B wiki.
- The User Guide[9] contains additional tutorials for ProR.
Planning
The following work is planned:
- Further work on the development of the system description for the requriements analyzer tool that supports the user by maintaining a consistent system description
- Applying the tracing method on the case studies of the industrial partners
Camille
Overview
The Camille plug-in provides a textual editor for Rodin. This editor provides the same look and feel as a typical Eclipse text editor, including features most text editors provide, such as copy, paste, syntax highlighting and code completion.
The latest release finally supports the full core Event-B language as it is supported by the built-in editors too.
Motivations / Decisions
A new version of the editor has been published to support the full feature of the core Event-B language. Event guards can now be defined as theorems as it is possible in the other Rodin editors. With this version all core Event-B models can be edited solely with Camille. It is no longer necessary to switch between different Editors.
To further improve the user experience, the syntax was slightly modified. With the new syntax all model elements now occur in the same order in every editor and pretty print. This finally lead to a more consistent modelling experience within the Rodin platform.
Available Documentation
- Architectures for an Extensible Text Editor for Rodin.[10] Bachelor thesis analysing the problem and discussing possible solutions.
- An earlier version of the thesis has been published as a technical report[11] that has been discussed on the Roding Developers Mailing List and the ADVANCE Progress Meeting in May 2012 in Paris.
Planning
Camille still has the drawback of not supporting extensibility. It only supports the core Event-B language and plug-in-specific additions are simply ignored. Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions. A new version of Camille will be implemented during the ADVANCE project. Plug-in Developers will be able to provide syntax contributions and parsers for their extensions. By this users will be able to edit extended Event-B models solely through a text editor.
References
- ↑ http://sourceforge.net/tracker/?group_id=108850&atid=651669
- ↑ http://sourceforge.net/tracker/?group_id=108850&atid=651672
- ↑ http://wiki.event-b.org/
- ↑ http://www.youtube.com/user/EventBTv
- ↑ http://www.eclipse.org/rmf/
- ↑ 6.0 6.1 http://www.stups.uni-duesseldorf.de/w/Special:Publication/HalJasLad2012
- ↑ http://www.stups.uni-duesseldorf.de/w/Special:Publication/LadenbergerJastram_iFMABZ2012
- ↑ http://wiki.event-b.org/index.php/ProR
- ↑ http://wiki.eclipse.org/RMF/User_Guide
- ↑ http://www.stups.uni-duesseldorf.de/mediawiki/images/0/0a/Pub-Weigelt2012.pdf
- ↑ http://www.stups.uni-duesseldorf.de/w/Special:Publication/Weigelt2012>
