D32 Introduction: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Tommy mNo edit summary |
imported>Tommy mNo edit summary |
||
| Line 7: | Line 7: | ||
Among the aims that WP9 partners reached, it might be worth to cite : | Among the aims that WP9 partners reached, it might be worth to cite : | ||
* Improved scalability and teamwork ability of the Rodin platform to support industrial deployments, through GUI refactorings and new features, SVN model storage, decomposition, modularisation, flows support, as well as qualitative probabilistic reasoning and others, | |||
* Improved scalability of the Rodin platform to support industrial deployments, through GUI | * Mathematical extensions, | ||
* Prover | * Prover performance, to increase the number of automatically discharged proof obligations. A relevance filtering tool has been developed, and work has been done to establish the soundness of provers and improve the well-definition proof obligation generation, | ||
* Model animation and testing, to validate Event-B models. | * Model animation and testing, to validate Event-B models.{{TODO}} Refactor | ||
* | * Records, | ||
* UML | * UML is thighter integrated in Rodin, through new features implementation or even the state-machine animation, | ||
* Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An | * Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An demonstrator tool has been developed. | ||
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. | 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. | ||
Revision as of 14:30, 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 and last year of DEPLOY.
Among the aims that WP9 partners reached, it might be worth to cite :
- Improved scalability and teamwork ability of the Rodin platform to support industrial deployments, through GUI refactorings and new features, SVN model storage, decomposition, modularisation, flows support, as well as qualitative probabilistic reasoning and others,
- Mathematical extensions,
- Prover performance, to increase the number of automatically discharged proof obligations. A relevance filtering tool has been developed, and work has been done to establish the soundness of provers and improve the well-definition proof obligation generation,
- Model animation and testing, to validate Event-B models.TODO Refactor
- Records,
- UML is thighter integrated in Rodin, through new features implementation or even the state-machine animation,
- Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An demonstrator tool has been developed.
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.
