Les méthodes de développement se sont un peu améliorées, mais en 2009 on développe encore du logiciel comme on le faisait dans les années 70 : on spécifie (plus ou moins), on code et on teste (ce que l'on peut). Suivant le temps, les ressources et la volonté dont on dispose, le résultat est plus ou moins réussi, voire largement utilisable (une distribution Linux fonctionne plutôt bien après tout ;-).
Mais cette approche ne permet pas de s'assurer que dans tous les cas le logiciel fonctionnera comme on l'attend. Et vu la place que prend le logiciel dans notre vie (dans les machines à laver, dans les voitures, dans les téléphones, dans nos ordinateurs de bureau, dans les trains et avions, ...), cette approche n'est pas satisfaisante. On devrait quand même être capable de faire du logiciel qui marche correctement, comme on fait des ponts et des immeubles qui ne s'effondrent pas !
C'est pour cette raison que je m'intéresse depuis pas mal de temps aux méthodes formelles. Elles consistent à utiliser les outils mathématiques pour vérifier un certain nombre de propriétés dans un programme et ainsi garantir, par construction, l'absence d'une certaine classe d'erreurs. Ces méthodes formelles sont plus ou moins compliquées à utiliser. Les plus simples sont peut-être l'utilisation des types dans des programmes en C++ ou OCaml, qui garantissent qu'on ne va pas mélanger les e-torchons et les e-serviettes. Les plus compliquées, comme la méthode B, partent d'une spécification formelle dans un formalisme mathématique précis et arrivent par raffinements successifs à un programme conforme par construction à cette spécification.
Évidemment, les méthodes formelles ne sont pas magiques ! Si vous posez mal votre problème, c.-à.d. si vos spécifications sont incorrectes, vous obtiendrez un programme qui garantit des propriétés bidons, pas très utile dans la vraie vie[1]. Mais l'utilisation de méthodes formelles oblige à réfléchir plus sérieusement à son programme et, en général, les programmes sont de meilleure qualité.
La bonne nouvelle, c'est que ces méthodes formelles deviennent de plus en plus accessibles :
- les outils sont facilement accessibles, et de nombreux outils sont disponibles sous forme de logiciels libres (et même deviennent libres). Ainsi, je maintiens une telle liste d'outils formels ou semi-formes libres ;
- les méthodes elle-mêmes deviennent plus accessibles, avec des approches plus « presse bouton » et des formalismes ne nécessitant pas un gros bagage mathématique.
Dans la suite de ce billet, j'insiste sur deux exemples : Frama-C et l'Atelier B.
Frama-C
Frama-C est un outil libre (sous licence GNU LGPL) développé principalement au CEA (Commissariat à l'Énergie Atomique) en partenariat avec des universités et centres de recherche (INRIA). Frama-C permet :
- l'analyse de code C : propagation de constantes, valeurs des variables, arbre d'appel des fonctions, analyse d'impact, slicing, etc. ;
- la preuve de propriétés sur du code C, en utilisant des programmes libres complémentaires (Why et Alt Ergo notamment).
En fait, Frama-C est un framework qui, grâce a un système d'extensions, permet de faire différentes analyses ou vérifications. Par exemple, l'analyse d'impact permet de savoir quelles variables ou structures de données sont influencés par la modification d'une variable : très utile pour l'analyse de sécurité ! Et comme Frama-C utilise une approche formelle (notamment l'interprétation abstraite), les analyses produites sont valables dans tous les cas (avec éventuellement des sur-approximations).
Avec Frama-C (et un peu d'huile de coude), on peut également prouver des propriétés sur un programme C, par exemple que telle variable entière ne débordera pas ou que telle fonction renvoie bien le résultat escompté. J'ai ainsi utilisé Frama-C pour prouver quelques propriétés sur un programme de vote électronique jouet. Ça peut-être utile d'être sûr que le gagnant calculé par le programme de vote a bien le nombre de voix le plus élevé[2]. ;-)
L'Atelier B
L'Atelier B est un environnement logiciel pour faire des spécifications et des programmes en utilisant la méthode B. Attention, l'Atelier B n'est pas un programme libre (honte à moi !) mais simplement gratuit. Seulement, lorsqu'on sait qu'il y a quelques mois à peine il était vendu 45.000 € et qu'il est utilisé pour développer des systèmes critiques comme le cœur de calcul du métro Météor, sa disponibilité devient intéressante. Enfin et surtout ClearSy, l'entreprise qui développer l'Atelier B, a une réelle ouverture vers le Libre (voir notamment la politique de distribution de l'Atelier B) avec mise à disposition de certains de ses outils en logiciels libres (licence GNU GPLv3) ou de certaines documentations en documentation libre (licence CC-BY).
L'Atelier B 4.0 est disponible en version Linux (mais aussi Windows et MacOS X). Il s'installe relativement facilement même si le script d'installation n'est pas standard. Il est fournit avec toutes les documentations (en anglais et français) nécessaires : Référence du langage B, Manuel de l'utilisateur d'Atelier B, etc.
En guise de conclusion
J'espère que ce petit billet a au moins éveillé une curiosité pour les méthodes formelles. Si vous avez des questions, n'hésitez pas à me les poser.