Over the last two decades, free and open source software has grown considerably. Distributions that started out with a few hundred packages now contain tens of thousands of packages, taken from many different sources. This creates problems for quality assurance. The tools and procedures used are no longer suitable for the size and complexity of modem distributions. In this thesis, we start by presenting a mathematical model of the commonalities between the different types of distributions (Debian and RPM) ; notably the concept of packages and the relations between them : dependencies and conflicts. The model is partially formalised using the Coq proof assistant. The model will subsequently be used to propose 'semantic' relations, more appropriate than existing relations for finding and correcting errors in distributions. We will also present algorithms that can be used to efficiently compute these relations, and we will use Coq to formally prove key theorems used by these algorithms Finally, we have validated our algorithms on existing distributions. We will present an analysis that is a result of this validation, as well as a discussion of the 'small world' phenomenon in relation with open source distributions.
A formal study of Free Software distributions