D23 Introduction: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Pascal
Line 4: Line 4:
The Rodin platform is available from the SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]).
The Rodin platform is available from the SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]).


This document gives a description of the work that was carried on during the second year of the DEPLOY project (Feb 2009-Jan 2010) in the course of the WP9 ''Tooling research and development'' work package. Moreover, it summarizes the planned activities for the coming year.
This document gives a description of the work that was carried on during the second year of the DEPLOY project (Feb 2009-Jan 2010) in the course of the WP9 ''Tooling research and development'' work package and brings new perspectives for the coming year.


More precisely, for each newly implemented feature or improvement, it is structured as follows:
The following items are covered: general platform maintenance, UML-B improvements, ProB improvements, text editor plug-in, decomposition plug-in, initial definition of language support for code generation, improvements to existing provers, rule-based prover, pattern plug-in, flow plug-in and modularisation plug-in.
 
For each of these newly implemented feature or improvement, the document is structured as follows:
* Overview. The involved partners are identified and an overview of the contribution is given.
* Overview. The involved partners are identified and an overview of the contribution is given.
* Motivations. The motivations for each tool extension and improvement are expressed.
* Motivations. The motivations for each tool extension and improvement are expressed.
Line 12: Line 14:
* Available documentation. Some pointers to the Event-B wiki or related publications are listed.
* Available documentation. Some pointers to the Event-B wiki or related publications are listed.
* Planning. A timeline and the current status (as of 29 Jan 2010) is given.
* Planning. A timeline and the current status (as of 29 Jan 2010) is given.
[[Category:D23 Deliverable]]
[[Category:D23 Deliverable]]

Revision as of 16:48, 26 January 2010

The deliverable D23 of the DEPLOY project is split into two parts:

  • The Rodin core platform and plug-ins (i.e. the DEPLOY tools).
  • This document.

The Rodin platform is available from the SourceForge site ([1]). The tool documentation is provided within the Event-B wiki ([2]).

This document gives a description of the work that was carried on during the second year of the DEPLOY project (Feb 2009-Jan 2010) in the course of the WP9 Tooling research and development work package and brings new perspectives for the coming year.

The following items are covered: general platform maintenance, UML-B improvements, ProB improvements, text editor plug-in, decomposition plug-in, initial definition of language support for code generation, improvements to existing provers, rule-based prover, pattern plug-in, flow plug-in and modularisation plug-in.

For each of these newly implemented feature or improvement, the document is structured as follows:

  • Overview. The involved partners are identified and an overview of the contribution is given.
  • Motivations. The motivations for each tool extension and improvement are expressed.
  • Choices / decisions. The decisions (e.g. design decisions) are justified.
  • Available documentation. Some pointers to the Event-B wiki or related publications are listed.
  • Planning. A timeline and the current status (as of 29 Jan 2010) is given.