| Attributes | Values |
|---|
| type
| |
| Thesis advisor
| |
| Author
| |
| alternative label
| - A formal study of Free Software distributions
|
| dc:subject
| - Thèses et écrits académiques
- Algorithmes
- Modèles mathématiques
- Progiciels
- Logiciels libres
|
| preferred label
| - Etude formelle des distributions de logiciel libre
|
| Language
| |
| Subject
| |
| dc:title
| - Etude formelle des distributions de logiciel libre
|
| Degree granting institution
| |
| note
| - 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.
- Dans les deux dernières décennies, le logiciel libre a pris un essor considérable. Des distributions qui au début comptaient une centaine de paquets, en ont maintenant des dizaines de milliers, tous de provenance très différente. Ceci engendre des problèmes pour la gestion de qualité. Les outils et procédures ne sont plus adaptés à la taille et la complexité des distributions d'aujourd'hui. Dans cette thèse, nous commençons par présenter une modélisation mathématique des points communs entre les différents types de distribution (Debian et RPM); notamment le concept des paquets et des relations qui existent entre eux: les dépendances et les conflits. Cette modélisation est en partie formalisé avec l'assistant de preuves Coq. Cette modélisation sera ensuite utilisée pour proposer des relations 'sémantiques', qui sont plus adaptés que les relations existantes pour repérer et corriger des erreurs dans les distributions. Nous présentons aussi des algorithmes pour calculer ces relations d'une façon efficace, et nous utiliserons Coq pour prouver formellement les théorèmes les plus importantes utilisées par ces algorithmes. Finalement, nous avons validé les algorithmes sur des distributions existantes. Nous présenterons une analyse de la structure des distributions qui est le résultat de cette validation, ainsi qu'une discussion de la phénomène du \"petit monde\" en rapport avec les distributions.
|
| dc:type
| |
| http://iflastandar...bd/elements/P1001
| |
| rdaw:P10219
| |
| has content type
| |
| is primary topic
of | |
| is rdam:P30135
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
