ADVANCE D3.2 Introduction

The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The Rodin toolset considered is built of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins that are available for the Rodin core platform which are not maintained in the frame of the ADVANCE project, therefore should not be considered within this deliverable.

The Rodin platform can be downloaded from the SourceForge site ([1]). The platform includes a collaborative documentation that is collected from two maintained locations :

• the Event-B wiki ,
• the Rodin Handbook .

The present document intends to gives a significant overview the work achieved within the WP3 Tooling research and development work package, during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives.

It is worth to remind that the ADVANCE project time frame overlaped with... blablabla Template:TODO: Continue after lunch

Among the aims that WP9 partners reached in the past year, it is worth citing :

• Improved scalability and teamwork ability of the Rodin platform to support industrial deployments, through GUI refactoring and new features, Subversion model storage, decomposition, modularisation, flow support, as well as qualitative probabilistic reasoning and others,
• Mathematical extensions are now supported in Rodin. The core of the Rodin platform has been modified and the Theory plug-in has been developed to allow the definition of new basic predicates, new operators and new algebraic types,
• Prover performance has increased through the addition of a relevance filtering plug-in which raises the number of automatically discharged proof obligations. Moreover, work has been done to establish the soundness of provers and improve the generation of well-definedness proof obligations,
• Model animation has been improved: it now supports multi-level animation and has been applied in WP1-4 deployment workpackages,
• Model testing was guided by the needs of WP1-4 partners and several approaches have been investigated,
• Structured types can now be directly defined and used in Rodin through the Records plug-in,
• UML is more tightly integrated in Rodin, through new features implementation or state-machine animation,
• Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. A 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.