imported>Tommy |
|
Line 1: |
Line 1: |
− | The DEPLOY's D32 deliverable is composed of:
| + | General diagram for the sluice controller example |
− | * The Rodin core platform and plug-ins (i.e. the DEPLOY tools).
| |
− | * This document.
| |
− | 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 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.
| |
− | | |
− | [[Category:D23 Deliverable]]
| |