D32 Teamwork

Overview

Teamwork consists of

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

• Decomposition

Difficulties in managing complex models (in particular for a large number of proof obligations) fed the idea of decomposing a model in a way that the resulting sub-models could be developed by different individuals. The decomposition process should be seen as a refinement step where the original properties and respective proof obligations should remain valid. With shared event and shared variable decomposition, these requirements are preserved, with the advantage of simplifying the overall development by dealing with sub-parts of the model at once in each sub-model.

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.

• Decomposition

The two styles of decomposition use as criteria of partition two of the most important elements of an Event-B model: variables and events. The plug-in supports the two styles and allows the decomposition through a stepwise wizard or through a decomposition file (with extension .dcp) that can be stored are re-run whenever necessary. For the shared event decomposition, the user needs to selects which variables are allocated to which sub-component. For the share variable decomposition, the user selects which events with be part of which sub-component. The rest of the sub-component (which is no more than an ordinary machine) is built automatically (after some validations).

Available Documentation

• SVN Team-based development documentation
• Decomposition plug-in user guide
• Event Model decomposition for shared variable approach
• Decomposition tool for Event-B

Planning

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

• Decomposition
  • Solve compatibility problems with other plug-ins: Records, Modularisation
  • Introduction of a graphical interface for decomposition, where the user drags and drop the elements to the respective sub-component.