D23 Introduction: Difference between revisions
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 | 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. | * 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.