Connaissez-vous Joseph Sifakis?

J'ai découvert Joseph Sifakis en écoutant Continent Sciences sur France Culture, dans les embouteillages, un après-midi. Premier lauréat français du Prix Turing, en 2007, Joseph Sifakis y faisait part de ses travaux, en matière de vérification de logiciel (model checking): en gros, vérifier si un logiciel ou plus précisément un algorithme remplit les specifications initiales. Un domaine que j'ai rapidement abordé lors d'une mission chez Dassault Aviation en 2005.

Cela peut vous paraître étrange, surtout si vous ne travaillez pas dans le secteur  de l'édition de logiciel, mais ... oui, les logiciels sont bourrés de bug. C'est d'ailleurs ce qui fait vivre certains éditeurs comme Oracle ou Dassault Systèmes: la manne payée annuellement par leurs clients pour bénéficier du support (15% environ du prix d'achat) permet de faire vivre l'éditeur et de financer ses développements ultérieurs. 

Ce qui est encore plus étrange, c'est que les travaux de Joseph Sifakis n'ont que peu d'intérêt pour ces éditeurs. En fait, Sifakis voit le monde du logiciel embarqué comme le véritable bénéficiaire de ses travaux de recherche. Il rappelle que 90% du logiciel écrit sur cette planète est embarqué. Et oui, pour un PC familial, on compte souvent plusieurs téléphones portables, une télé, une voiture, une machine à laver, un micro-onde, un ou plusieurs lecteurs MP3, etc. Et le logiciel embarqué dans ces appareils a intérêt à être plus fiable que celui commercialisé par certains éditeurs. 

C'est surtout dans des domaines comme l'aeronautique ou l'espace que ce type d'approche est indispensable. Lorsque les systèmes critiques de ces engins sont livrés au bon vouloir de quelques centaines de lignes de code, l'erreur n'est plus admissible...