D23 Introduction: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Pascal |
imported>Laurent mNo edit summary |
||
| (4 intermediate revisions by 2 users not shown) | |||
| Line 2: | Line 2: | ||
* The Rodin core platform and plug-ins (i.e. the DEPLOY tools). | * The Rodin core platform and plug-ins (i.e. the DEPLOY tools). | ||
* This document. | * This document. | ||
The Rodin platform is available from the SourceForge site ([ | 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. | ||
For each newly implemented | In particular, the WP9 partners have strovin to meet the following objectives: | ||
* Improved scalability of the Rodin platform to support industrial deployments, through GUI enhancements (smart completion, renaming, text editing, etc), decomposition support and design-pattern management. | |||
* Prover integrity and performance, to enhance the confidence in provers and to enlarge their proving capabilities. To this aim, the existing provers have been improved and a new rule-based prover plug-in has been implemented. | |||
* Model animation and testing, to validate Event-B models. More precisely, the ProB or AnimB plug-ins allow a domain expert to detect errors in a model and ensure the presence of desired functionalities. Moreover, it is very important for many industrial applications to be able to completely hide the underlying formal specification. | |||
* Model checking (ProB), to enable users to find sequences of events that prevent safety properties or proof obligations to be fulfilled. | |||
* UML integration. UML-B provides a diagrammatic, formal modelling notation based on UML. | |||
* Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An initial definition of language support for code generation has been put forward. | |||
This document covers the following items: 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 features or improvements, 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 22: | ||
* 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]] | ||
Latest revision as of 11:20, 27 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.
In particular, the WP9 partners have strovin to meet the following objectives:
- Improved scalability of the Rodin platform to support industrial deployments, through GUI enhancements (smart completion, renaming, text editing, etc), decomposition support and design-pattern management.
- Prover integrity and performance, to enhance the confidence in provers and to enlarge their proving capabilities. To this aim, the existing provers have been improved and a new rule-based prover plug-in has been implemented.
- Model animation and testing, to validate Event-B models. More precisely, the ProB or AnimB plug-ins allow a domain expert to detect errors in a model and ensure the presence of desired functionalities. Moreover, it is very important for many industrial applications to be able to completely hide the underlying formal specification.
- Model checking (ProB), to enable users to find sequences of events that prevent safety properties or proof obligations to be fulfilled.
- UML integration. UML-B provides a diagrammatic, formal modelling notation based on UML.
- Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An initial definition of language support for code generation has been put forward.
This document covers the following items: 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 features or improvements, 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.
