Quand le logiciel est comme un théorème à prouver

Par 17 juillet 2008
Mots-clés : Smart city

Passer moins de temps sur les tests de softwares, pour approfondir et optimiser leur programmation en amont : telle est l'approche qui devrait assurer la mise sur le marché de logiciels sans faille.

Les logiciels sont rarement sans faille dès leur première sortie. Un fait accepté par les consommateurs, habitués à tester les softwares et à apporter leurs commentaires aux éditeurs, qui améliorent au fur et à mesure leurs produits. "Sur ce plan, l'industrie du logiciel est encore très immature comparée aux autres branches de l'ingénierie", commente Bengt Nordström, chercheurs au sein de l'Université de Göteborg. Ce dernier travaille au sein du programme européen baptisé Future and Emerging Technologies Programme, qui veut faire évoluer ces méthodes."La programmation n'est pas basée sur des théories vérifiées, et nous n'avons pas de bonnes méthodes de design qui peuvent nous garantir que chaque étape du développement est correcte", explique le chercheur. Un procédé qui doit changer : le temps qui est dépensé à tester des logiciels peu aboutis, devrait être passé à écrire et élaborer ces logiciels. Cette approche est basée sur la "théorie des types".
La logique mathématique résout les failles
Il s'agit d'une branche de la logique mathématique : elle fonde la construction des objets sur la notion de fonction et non pas sur celle d'ensemble. Dans cette approche le programme qui arrive à résoudre un calcul est compris comme l'équivalent de la preuve d'un théorème. En prouvant le théorème, le programme est garanti correct. Une méthode qui veut économiser les efforts qui sont traditionnellement effectués pour tester les logiciels : "ce n'est pas ainsi que l'on construit des routes et des ponts, ils sont évidemment tout de suite opérationnels", ajoute Bengt Nordström. La "théorie des types", jugée prometteuse, est développée par en particulier par le programme TYPES, dans le cadre du projet Future and Emerging Technologies Programme. Types est quant à lui basé sur l'open source.
L'open source fait avancer la recherche
"La recherche européenne dans ce domaine est très en avance", assure Bengt Nordström. "Et l'open source est une manière d'ouvrir la recherche au plus grand nombre, afin d'accélérer un processus qui, il est vrai, prend du temps". Les résultats de ces théories sont déjà appliqués dans des projets comme le programme européen Mobius : dans ce cadre elles permettent d'assurer que les programmes téléchargés ne subissent pas de bug. Si l'application de la "théorie des types" n'est pas nécessaire à tous les logiciels, elle s'avère cependant d'une grande aide pour les programmes critiques, comme ceux utilisés dans le cas du e-banking, ou encore pour les transports, la défense ou la santé.

Mentions légales © L’Atelier BNP Paribas