Main dans la main, des chercheurs de l’Inria et de Microsoft tentent de redéfinir la façon de concevoir les logiciels, afin de s’approcher au plus près du zéro défaut.
Pour concocter un logiciel, la recette est quasiment toujours la même depuis de nombreuses années. Elle commence par une phase d’analyse : d’abord, on décrit dans divers documents ce que le logiciel est censé faire (ses spécifications générales, fonctionnelles et techniques) ; puis on définit comment il se comportera avec les logiciels qui cohabiteront avec lui.Un peu comme s’il s’agissait de construire une maison… On dresse tout d’abord les plans, détaillés, dans des documents dits de conception architecturale. Puis on identifie les différentes briques : des petits bouts de programmes censés remplir une fonction précise qui, mis bout à bout, constitueront le logiciel. Et ce n’est qu’après cette phase d’analyse que les informaticiens peuvent commencer à coder le logiciel, en le traduisant dans un langage informatique (C, C++, Java, etc. ).Au terme de cette phase de développement, il ne reste plus qu’à compiler le programme ?” c’est-à-dire le traduire en langage machine, compréhensible par un ordinateur ?” et, surtout, à le tester… Ce qui revient à partir à la chasse aux bogues !
Des logiciels qui fonctionneront sans même avoir été testés !
Une phase de vérification ultime qui peut durer longtemps… Car il faut imaginer toutes les situations auxquelles le logiciel devra faire face, pour les programmer dans des outils de tests. Des outils de simulation qui éprouveront non seulement le logiciel dans sa globalité, mais aussi les briques qui le composent, une à une. C’est ce que l’on appelle les tests unitaires. Et dès qu’une anomalie de fonctionnement est détectée, il faut en trouver l’origine, apporter les corrections nécessaires, et relancer les tests… encore et encore. Un travail de longue haleine qui diminue considérablement le risque de dysfonctionnement du logiciel, mais sans jamais le réduire à néant !Voilà tout l’objet de l’accord de collaboration passé, en février 2005, entre l’Institut national de recherche en informatique et en automatique (Inria) et la division recherche de Microsoft. L’objectif : en finir une bonne fois pour toutes avec les bogues dans les programmes. Cela, grâce à des techniques qui remettent complètement en cause la façon de développer les logiciels : les méthodes formelles avec preuve, qui s’appuient sur les mathématiques pures.Pour le moment, les méthodes formelles avec preuve ont surtout été utilisées pour développer des logiciels embarqués – c’est-à-dire intégrés à un équipement – comme le système de pilotage automatique de la ligne 14 du métro parisien. Mais demain, grâce en partie aux travaux de l’Inria et de Microsoft Research, elles serviront peut-être à faire tourner les logiciels de nos ordinateurs personnels. Des ordinateurs qui devraient alors s’avérer beaucoup plus stables et beaucoup plus fiables qu’aujourd’hui.
