Difference between revisions of "D32 Introduction"
From Event-B
Jump to navigationJump to searchimported>Tommy (Initial commit) |
imported>Tommy m |
||
| Line 4: | Line 4: | ||
The Rodin platform can be downloaded from 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 can be downloaded from 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 | + | This document gives an insight into the work achieved throughout the WP9 ''Tooling research and development'' work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming year. |
| − | + | Among the aims that WP9 partners reached, it might be worth to cite : | |
| + | {{TODO}} Refactor this part. | ||
* 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. | * 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. | * 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. | ||
| Line 13: | Line 14: | ||
* UML integration. UML-B provides a diagrammatic, formal modelling notation based on UML. | * 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. | * 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. | ||
| + | ---- | ||
| − | + | The various parts making up this document are the following: general platform maintenance, mathematical extensions, provers, UML-B improvements, code generation, teamwork, scalability, model animation, and model-based testing. | |
| − | + | Note that each of these parts is describing the improvements made, and 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. | ||
* Choices / decisions. The decisions (e.g. design decisions) are justified. | * Choices / decisions. The decisions (e.g. design decisions) are justified. | ||
* 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 | + | * Planning. A timeline and the current status (as of 28 Jan 2011) is given. |
[[Category:D23 Deliverable]] | [[Category:D23 Deliverable]] | ||
Revision as of 13:04, 19 November 2010
The DEPLOY's D32 deliverable is composed of:
- The Rodin core platform and plug-ins (i.e. the DEPLOY tools).
- This document.
The Rodin platform can be downloaded from SourceForge site ([1]). The tool documentation is provided within the Event-B wiki ([2]).
This document gives an insight into the work achieved throughout the WP9 Tooling research and development work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming year.
Among the aims that WP9 partners reached, it might be worth to cite : TODO Refactor this part.
- 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.
The various parts making up this document are the following: general platform maintenance, mathematical extensions, provers, UML-B improvements, code generation, teamwork, scalability, model animation, and model-based testing.
Note that each of these parts is describing the improvements made, and 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 28 Jan 2011) is given.
