D32 Introduction

From Event-B
Revision as of 14:04, 19 November 2010 by imported>Tommy
Jump to navigationJump to search

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 : 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.