D45 Introduction: Difference between revisions

From Event-B
Jump to navigationJump to search
Newer edit →
imported>Tommy
m New page: The DEPLOY deliverable D45 is composed of: * the Rodin core platform and plug-ins (i.e. the DEPLOY tools), * this document. The Rodin platform can be downloaded from the SourceForge site (...
 
imported>Tommy
mNo edit summary
Line 1: Line 1:
The DEPLOY deliverable D45 is composed of:
The DEPLOY deliverable D45 is made of the Rodin core platform and plug-ins (i.e. the DEPLOY tools), and this document. The Rodin platform can be retrieved from the Sourceforge site ([https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform]). The documentation of the toolset takes place on two sites:
* the Rodin core platform and plug-ins (i.e. the DEPLOY tools),
* the Event-B wiki ([http://wiki.event-b.org]).
* this document.
* the Event-B Handbook ([http://handbook.event-b.org]).
The Rodin platform can be downloaded from the SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The Event-B wiki ([http://wiki.event-b.org]) hosts the documentation of the tool.


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 the project.
This document will give an overview of the work done within the WP9 ''Tooling research and development'' work package, during the fourth and last year of the DEPLOY project (Feb 2011-Apr 2012). It also gives a status of the toolset by the end of the project.


Among the aims that WP9 partners reached in the past year, it is worth citing :
By the end of the third year of the DEPLOY project, the DEPLOY partners reported some issues they encountered and expressed some specific needs which they considered mandatory to address before the end of DEPLOY. To ensure that all these issues were considered by the end of DEPLOY, the various tasks done by the WP9 partners have been early scheduled and prioritized to both fit with the original description of work(DOW) and give answers to the DEPLOY partner issues.  
* 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.
Here is short list of important tasks that the WP9 partners were committed to achieve and are worth citing:
*
*
*
 
The various parts making up this document are the following: general platform maintenance, scalability, prover enhancement, 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:
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 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, handbook, or related publications are listed.
* Planning. A timeline and the current status (as of 28 Jan 2011) is given.
* Planning. The current status (as of 27 Apr 2012) is given.


[[Category:D45 Deliverable]]
[[Category:D45 Deliverable]]

Revision as of 15:33, 7 November 2011

The DEPLOY deliverable D45 is made of the Rodin core platform and plug-ins (i.e. the DEPLOY tools), and this document. The Rodin platform can be retrieved from the Sourceforge site ([1]). The documentation of the toolset takes place on two sites:

  • the Event-B wiki ([2]).
  • the Event-B Handbook ([3]).

This document will give an overview of the work done within the WP9 Tooling research and development work package, during the fourth and last year of the DEPLOY project (Feb 2011-Apr 2012). It also gives a status of the toolset by the end of the project.

By the end of the third year of the DEPLOY project, the DEPLOY partners reported some issues they encountered and expressed some specific needs which they considered mandatory to address before the end of DEPLOY. To ensure that all these issues were considered by the end of DEPLOY, the various tasks done by the WP9 partners have been early scheduled and prioritized to both fit with the original description of work(DOW) and give answers to the DEPLOY partner issues.

Here is short list of important tasks that the WP9 partners were committed to achieve and are worth citing:

The various parts making up this document are the following: general platform maintenance, scalability, prover enhancement, 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 improvement are expressed.
  • Choices / decisions. The decisions (e.g. design decisions) are justified.
  • Available documentation. Some pointers to the Event-B wiki, handbook, or related publications are listed.
  • Planning. The current status (as of 27 Apr 2012) is given.
Retrieved from ‘https://wiki.event-b.org/index.php?title=D45_Introduction&oldid=3026’