Formal Modelling of Version Control Systems

Abstract

<p>Version control systems are widely used to manage collections of files and directories, along with changes made to them over their lifetime. Any previously checked in version of a file is recoverable at any time from the repository. They allow people to work on the same files in a decentralized and concurrent way, while consistently managing and integrating changes.<br /> In this thesis we develop a subset of the SVN and CVS version control systems from specifications using Atelier B 4. Both of these systems are feature rich, widely used in cross-platform environments and representative of their class of file based extensional version control systems. Support for abstract data types like sets and refinement is well suited to the task. The most commonly used features such as Add, Check-in, Update are modeled in increasing detail in multiple refinement steps. Later refinement steps add features such as binary file support and the local cache. Having both models allows us to compare and contrast their feature sets. Documentation for SVN and CVS is extensive but informal. One feature of CVS required experimentation when the written documentation was insufficient. SVN is modelled in approximately 1400 lines in eight refinement steps with 109 proof obligations. CVS is likewise specified in roughly 1150 lines in seven steps with 29 proof obligations. With all proof obligations discharged we are confident the models represent the real systems and are a reasonable first step towards the goal of verifiable implementations of version control systems.</p>