Scenarios for Team-based Development - Revision history

imported>Laurent at 14:38, 29 January 2009

2009-01-29T14:38:50Z

← Older revision		Revision as of 14:38, 29 January 2009
Line 3:		Line 3:
	== Objective ==		== 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.		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. It was 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~~ ==		== Approach ==

	* Identify scenarios ~~at dusseldorf~~ (through ~~Brainstorming~~)		* Identify scenarios (users and tool developers through brainstorming)

	* While identifying scenarios, collect requirements that must hold true for all scenarios		* While identifying scenarios, collect requirements that must hold true for all scenarios
Line 21:		Line 21:
	; (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-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-2) Multiple users work concurrently on an Event-B Project: In this scenario, 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-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.
Line 35:		Line 35:
	== Some general thoughts ==		== 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.		* There are two common types of repositories: Those following a lock-edit-unlock cycle (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.		* 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).		* 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 choose 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 ==		== 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.		Here is the 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.
	[[Image:SubversionProposal.svg]]		[[Image:SubversionProposal.svg]]

	[[Category:Design proposal]]		[[Category:Design proposal]]

imported>Mathieu at 20:05, 2 October 2008

2008-10-02T20:05:23Z

← Older revision		Revision as of 20:05, 2 October 2008
Line 47:		Line 47:
	[[Image:SubversionProposal.svg]]		[[Image:SubversionProposal.svg]]

	[[Category:Design]]		[[Category:Design proposal]]

imported>Mathieu at 20:01, 2 October 2008

2008-10-02T20:01:34Z

← Older revision		Revision as of 20:01, 2 October 2008
Line 1:		Line 1:
			''See also the [[Talk:Scenarios for Team-based Development\|associated talk page]] for discussion about this topic.''

	== Objective ==		== Objective ==

imported>Mathieu: Category:Design

2008-09-29T12:09:04Z

Category:Design

← Older revision		Revision as of 12:09, 29 September 2008
Line 44:		Line 44:
	* 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.		* 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.
	[[Image:SubversionProposal.svg]]		[[Image:SubversionProposal.svg]]

			[[Category:Design]]

imported>Jastram: jpg is currently not allowed! Changed to svg

2008-09-28T18:43:18Z

jpg is currently not allowed! Changed to svg

← Older revision		Revision as of 18:43, 28 September 2008
Line 43:		Line 43:

	* 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.		* 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.
	[[Image:SubversionProposal.~~jpg~~]]		[[Image:SubversionProposal.svg]]

imported>Jastram: Scenarios for Team-based Development

2008-09-28T18:36:36Z

Scenarios for Team-based Development

New page

== 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.
[[Image:SubversionProposal.jpg]]