Scenarios for Team-based Development

See also the associated talk page for discussion about this topic.

Objective

Rodin is currently a stand-alone tool. Attempts to use it in a team environment by simply putting a code repository underneath it (e.g. Subversion) failed, as this makes handling of conflicts awkward at best. We decided to take a step back and to first figure out what is needed in the first place, before deciding on how to solve the problem.

Aproach

• Identify scenarios at dusseldorf (through Brainstorming)

• While identifying scenarios, collect requirements that must hold true for all scenarios

• Share the scenarios with the industry partners to validate and improve them (and to find missing scenarios)

• Decide on the scenario(s) that will be implemented for Rodin

• Design a subsystem for Rodin that will realize the selected scenario(s) and implement it

Scenarios

(S-1) Only one person at a time works on an Event-B Project

While it is important not to corrupt data through concurrent edits, in this scenario it is sufficient if access for editing is granted only one user at a time.

(S-2) Multiple users work concurrently on an Event-B Project

In this scenarios it is expected that several users need concurrent write-access to the project. It is acceptable if individual elements of the system must be locked, or if individual elements need to be merged in case of conflict.

(S-3) A History of changes on an Event-B Project is maintained and accessible

In this scenario, the users don't care much about the team aspect, but require access to a change history.

(S-4) A project is exchanged between two sites (e.g. customer and supplier), where each party has a clear responsibility

In this scenario it is expected that each party can modify only a certain part of the model, and it is expected that a merge must be performed on a regular basis.

Requirements for all Scenarios

(R-1) If a change in the machine or context has an impact on proofs, the proofs are either updated or invalidated.

(R-2) The impact of editing on the rest of the system shall be as small as possible.

This could mean, for instance that if we change an invariant, that not the whole prooftree of a proof is invalidated, but only a subtree.

Some general thoughts

• There are two common types of repositories: Those following a lock-edit-unlock cylce (MS SourceSafe, Perforce) and those following an update-edit-merge cycle (Subversion, CVS). These two approaches are not compatible. The question of which approach to use will appear sooner than later.

• The granularity of the Event-B-models for the purpose of team-based development has to be decided at some point. As we noted earlier, the current file structure clearly does not have the right granularity.

• With a text editor, it would be possible to for example store the textual representations of the models in subversion. This would in principle enable concurrent editing: updating the Rodin XML models in case of an svn update would not be much different from when a user locally modifies a text file. This still leaves open the issue of how to enable multiple users to work on proofs a the same time. If every proof is represented by a single file, one could for example put those files as binary files within subversion. (Note: this means that individual proofs cannot be merged; if two users have modified the same proof one would have to chose one of the two versions.) There are, however, still issues with how to manage the individual proof files in case of changes to the model (renaming of some files, deletion of others and additions).

Proposal for a solution

• I have drawn a small picture of a technical solution relying on subversion, a textual representation of models, the two-way translator between Rodin XML files and text files (part of a text editor), and an extension of the Rodin POG where proofs for POs are stored in individual XML files.