Résumé
L’équipe de Prove&Run a montré l’an dernier la faisabilité de la preuve complète d’un micro-noyau, Minix V3, d’une complexité comparable à celle réalisée par l’équipe du NICTA sur Sel4 – une première mondiale jusqu’à présent inégalée. Nous avons utilisé une approche différente afin de prendre en compte de nouvelles contraintes cruciales pour l’utilisation et surtout la généralisation de ce genre de preuve en environnement industriel. L’objectif à plus long terme de Prove&Run est de démontrer et de permettre l’utilisation à grande échelle des méthodes formelles pour le développement de composants critiques.
Le passage à la grande échelle des méthodes formelles nécessite la prise en compte de contraintes supplémentaires pour les applications critiques. À titre d’exemple, on imagine bien que même s’il est crucial de faire au moins un premier vol habité sur Mars avant d’imaginer la première liaison régulière entre Mars et la Terre, les méthodes acceptables pour la première navette expérimentale ne le seront pas forcément pour la première navette commerciale. De la même manière, nous sommes arrivés à la conclusion qu’il fallait développer un nouveau langage et une nouvelle approche, en s’appuyant pour l’essentiel sur l’état de l’art en méthodes formelles, sur les prodigieuses connaissances accumulées pendant ces dernières décennies dans ce domaine et plus largement en informatique théorique. Mais nous avons aussi conclu qu’il convenait de renoncer à certains traits considérés comme des « must » dans le monde académique, car ils nous ont paru trop coûteux actuellement en fonction des contraintes spécifiques du contexte industriel. Nous avons par exemple renoncé à utiliser l’ordre supérieur, au moins dans un premier temps. Nous avons aussi dérogé à la tendance tendant à éliminer les boucles dans la description des programmes : nos définitions de fonctions ne sont pas forcément récursives et peuvent adopter un style impératif, le langage restant malgré tout fonctionnel.
