Difference between pages "D32 Mathematical Extensions" and "D32 Teamwork"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Im06r
 
imported>Vitaly
 
Line 1: Line 1:
 
=== Overview ===
 
=== Overview ===
 +
Teamwork consists of
 +
* SVN enabling teamwork plug-in
 +
* Decomposition methods
  
−
Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (prover extensions).
 
  
−
A theory is a file that can be used to define new algebraic types, new operators/predicates and new proof rules. Theories are developed in the Rodin workspace, and proof obligations are generated to validate prover and mathematical extensions. When a theory is completed and (optionally) validated, the user can make it available for use in models (this action is called the deployment of a theory). Theories are deployed to the current workspace (i.e., Workspace Scope), and the user can use any defined extensions in any project within the workspace.
+
* Team-working Plug-in is a new feature developed by University of Southampton in request to industrial partners who required support of Rodin project management and team development using Subversion system. Having this support would bring the benefit of centralised model storage and versioning, as well as parallel development. Despite a few functional limitations, derived by specific nature of the Rodin projects, the implemented plug-in gives support for Subversion-based project sharing and collaborative development.
  
−
Records Plug-in has been developed by University of Southampton before the mathematical extensions as a new feature to provide structured types in Event-B. The plug-in extends Rodin standard context editor with a new modelling construct to provide support for structured types, which can be defined in terms of two new clauses: record declarations and record extensions. Both enable users to define their custom reusable types, that are treated underline by Rodin as Event-B constant sets and relations, supported by additional axioms, which the plug-in generates to simplify the proofs.
+
* Decomposition plug-in was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: ''shared event'' (studied initially by Michael Butler) and ''shared variable'' (studied initially by Jean-Raymond Abrial). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.
  
 
=== Motivations ===
 
=== Motivations ===
−
 
+
Main reasons for implementing teamwork are:
−
Main reasons for implementing mathematical extensions are:
+
* SVN Teamwork
−
* increased readability (<math>a \; \operatorname{OR} \; b</math> rather than <math>\operatorname{bool}(a=TRUE \or b=TRUE)</math>)
+
: The reason to support compatibility of Rodin projects with Subversion was to allow Rodin users to share their projects and work on them together, as well as have the benefits of versioning and revision control, provided by the SVN system. It was difficult to work on models in parallel and manage changes made by different parties, especially for big and complex models. Other users expressed a concern on safety aspect of collaborative development, thus pointing out the benefits of centralised repository storage of the models under development on SVN.
−
* polymorphism (<math>l \in List(S \cprod T)</math>)
 
−
* decreased proving effort, thanks to extension specific proof rules instead of general purpose ones
 
−
 
 
−
The Theory plug-in superseded the Rule-based Prover v0.3 plug-in, and is the placeholder for mathematical and prover extensions. It provides a high-level interface to the Rodin Core capabilities with regards to mathematical extensions. The Rule-based Prover was originally devised to provide an usable mechanism for user-defined rewrite rules through theories. Theories were, then, deemed a natural choice for defining mathematical extensions as well as proof rules to reason about such extensions. In essence, the Theory plug-in provides a systematic platform for defining and validating extensions through a familiar technique: proof obligations.
 
−
 
 
−
The motivation for development of Records plug-in was to fill the gap in Event-B language - a missing support of a syntax for the direct definition of structured types. Some of the industrial partners expressed a desire to have this missing feature in Event-B, that would allow them to define their own structured types such as records or classes. Theoretically these structures could be modelled with existing Event-B capabilities via projection functions. Backed up by a refined theoretical proposal Records plug-in was developed to extend the standard Event-B notation with requested capability.
 
  
 
=== Choices / Decisions ===
 
=== Choices / Decisions ===
−
 
+
* SVN Teamwork
−
On the Core Rodin Platform side, implementing mathematical extensions required to make some parts of the code extensible, that were not designed to be so, namely the lexer and the parser. We were using tools that automatically generated them from a fixed grammar description, so we had to change to other technologies. A [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser study] has been made on available technologies. The Pratt algorithm was selected for its adequation with the purpose and it did not have the drawbacks of other technologies:
+
: The desired objective of a plug-in that would bring support for Subversion in Rodin was to make a Rodin project compatible with standard SVN interface. Due to nature of the Rodin resource management, in particular the use of Rodin database and non-XMI serialisation, it turned out a hard task. A solution to this difficulty was to provide an alternative serialisation method, that would be compatible with Subversion interface. XMI serialisation has been chosen in the final plug-in, which together with Event-B EMF framework provides a shareable copy of the resources of a Rodin project and takes care of synchronisation between two.
−
* foreign language integration
 
−
* overhead due to over generality
 
−
 
 
−
After a mocking up phase to verify feasibility, the Pratt algorithm has been confirmed as the chosen option and implemented in the Rodin Platform.
 
−
 
 
−
Besides, we wanted to set up a way to publish and share theories for Rodin users, in order to constitute a database of pre-built theories for everyone to use and contribute. This has been realised by adding a new tracker on SourceForge site ([http://sourceforge.net/tracker/?group_id=108850&atid=1558661]).
 
−
 
 
−
The Theory plug-in contributes a theory construct to the Rodin database. Theories were used in the Rule-based Prover (before it was discontinued) as a placeholder for rewrite rules. Given the usability advantages of the theory component, it was decided to use it to define mathematical extensions (new operators and new datatypes). Another advantage of using the theory construct is the possibility of using proof obligations to ensure that the soundness of the formalism is not compromised. Proof obligations are generated to validate any properties of new operators (e.g., associativity). With regards to prover extensions, it was decided that the Theory plug-in inherits the capabilities to define and validate rewrite rules from the Rule-based Prover. Furthermore, support for a simple yet powerful subset of inference rules is added, and polymorphic theorems can be defined within the same setting. Proof obligations are, again, used as a filter against potentially unsound proof rules.
 
−
 
 
−
Records plug-in required the extension of the Rodin database with the new constructs to support structured types. On the other hand the Event-B language itself did not support extension at that time. For that reason the decision was made to address extensibility problem at the lowest level possible, which was Rodin database, but to model structured types using standard Event-B notation at the level below. The translation from extended to standard syntax has been entrusted to the static checker, that was also extended for this purpose. Thus the plug-in provides the users with notation for record declarations and extensions in unchecked models, but the checked versions operate with standard Event-B constructs.
 
  
 
=== Available Documentation ===
 
=== Available Documentation ===
−
+
* SVN Team-based development documentation<ref>http://wiki.event-b.org/index.php/Team-based_development</ref>
−
* Pre-studies (states of the art, proposals, discussions).
 
−
** [http://deploy-eprints.ecs.soton.ac.uk/216/ ''Proposals for Mathematical Extensions for Event-B'']
 
−
** [http://deploy-eprints.ecs.soton.ac.uk/251/ ''Mathematical Extension in Event-B through the Rodin Theory Component'']
 
−
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser#Design_Alternatives]
 
−
** [http://wiki.event-b.org/index.php/Structured_Types ''Theoretical Description of Structured Types'']
 
−
* Technical details (specifications).
 
−
** [http://wiki.event-b.org/index.php/Mathematical_Extensions]
 
−
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Lexer]
 
−
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser]
 
−
** [http://wiki.event-b.org/index.php/Theory_Plug-in]
 
−
** [http://wiki.event-b.org/index.php/Records_Extension ''Records Extension Documentation'']
 
−
* Teaching materials (tutorials).
 
−
* User's guides.
 
−
** [http://wiki.event-b.org/images/Theory_UM.pdf]
 
  
 
=== Planning ===
 
=== Planning ===
 
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
 
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
  
−
{{TODO|What will remain to do after Rodin 2.1 ?}}
+
=References=
 +
<references/>
  
 
[[Category:D32 Deliverable]]
 
[[Category:D32 Deliverable]]

Revision as of 10:24, 26 November 2010

Overview

Teamwork consists of

  • SVN enabling teamwork plug-in
  • Decomposition methods


  • Team-working Plug-in is a new feature developed by University of Southampton in request to industrial partners who required support of Rodin project management and team development using Subversion system. Having this support would bring the benefit of centralised model storage and versioning, as well as parallel development. Despite a few functional limitations, derived by specific nature of the Rodin projects, the implemented plug-in gives support for Subversion-based project sharing and collaborative development.
  • Decomposition plug-in was developed by Renato Silva (University of Southampton), Carine Pascal (Systerel) based on the initial prototype developed by T.S. Hoang (ETH Zurich). This plug-in was developed as an answer to models that became to big to be handled with a large number of events, a large number of variables and consequently a large number of proof obligations over several levels of refinements. There are two kinds of decomposition available: shared event (studied initially by Michael Butler) and shared variable (studied initially by Jean-Raymond Abrial). Both decomposition styles allow the partition of the original model into (smaller) sub-models. The sub-models are expected to be easier to handle, with less variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independent of each other and therefore can be refined individually. As a consequence, each sub-model can be further developed by different people allowing teamwork development.

Motivations

Main reasons for implementing teamwork are:

  • SVN Teamwork
The reason to support compatibility of Rodin projects with Subversion was to allow Rodin users to share their projects and work on them together, as well as have the benefits of versioning and revision control, provided by the SVN system. It was difficult to work on models in parallel and manage changes made by different parties, especially for big and complex models. Other users expressed a concern on safety aspect of collaborative development, thus pointing out the benefits of centralised repository storage of the models under development on SVN.

Choices / Decisions

  • SVN Teamwork
The desired objective of a plug-in that would bring support for Subversion in Rodin was to make a Rodin project compatible with standard SVN interface. Due to nature of the Rodin resource management, in particular the use of Rodin database and non-XMI serialisation, it turned out a hard task. A solution to this difficulty was to provide an alternative serialisation method, that would be compatible with Subversion interface. XMI serialisation has been chosen in the final plug-in, which together with Event-B EMF framework provides a shareable copy of the resources of a Rodin project and takes care of synchronisation between two.

Available Documentation

  • SVN Team-based development documentation[1]

Planning

This paragraph shall give a timeline and current status (as of 28 Jan 2011).

References

  1. ↑ http://wiki.event-b.org/index.php/Team-based_development
Retrieved from ‘https://wiki.event-b.org/index.php?title=D32_Mathematical_Extensions&oldid=2642’