Conceptuellement, un système de stockage de base de données est une simple mappe entre clés et valeurs. Cependant, afin d’offrir performances élevées et fiabilité, une base de donnée moderne est un système complexe et concurrent, ce qui rend ouvre la porte aux erreurs.
Cette thèse relate notre parcours, allant de la spécification formelle d’une base de données à sa mise en œuvre. La spécification est courte et non ambigüe, et aide à raisonner sur la justesse. La lecture de la spécification permet de dégager les problèmes importants et tient lieu de pseudocode rigoureux pour la mise en œuvre.
La spécification décrit la couche de stockage comme une mémoire partagée transactionnelle simple, avec deux variantes (au comportement équivalent), basées respectivement sur une mappe et un journal. Nous mettons en œuvre ces deux variantes, en suivant fidèlement notre spécification. Les mécanismes complexes d’une base de données moderne, comme un système de journalisation, tronqué à volonté grâce à des points de reprise, comme une composition des deux variants. Finalement, nous présentons une évaluation expérimentale, avec des performances qui sont acceptables pour une mise en œuvre rigoureuse.