ADVANCE D3.3 General Platform Maintenance

From Event-B
Revision as of 08:45, 23 August 2013 by imported>Ladenberger (→‎ProR)
Jump to navigationJump to search

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:

  • a sourceforge bug tracker,[1]
  • a sourceforge feature requests tracker.[2]

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

TODO

Motivations / Decisions

TODO

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. Other improvements will include more general improvements, such as usability, and any features required by the projects industrial partners.

Motivations / Decisions

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.

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

TODO

Camille

Overview

TODO

Motivations / Decisions

TODO

Available Documentation

TODO

Planning

TODO

References

  1. ↑ http://sourceforge.net/tracker/?group_id=108850&atid=651669
  2. ↑ http://sourceforge.net/tracker/?group_id=108850&atid=651672
  3. ↑ http://wiki.event-b.org/
  4. ↑ http://www.youtube.com/user/EventBTv
  5. ↑ http://www.eclipse.org/rmf/
  6. ↑ Cite error: Invalid <ref> tag; no text was provided for refs named req1ref
  7. ↑ http://www.stups.uni-duesseldorf.de/w/Special:Publication/LadenbergerJastram_iFMABZ2012
  8. ↑ http://wiki.event-b.org/index.php/ProR
  9. ↑ http://wiki.eclipse.org/RMF/User_Guide
Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.3_General_Platform_Maintenance&oldid=353’