D32 Teamwork

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.

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

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