---

© E. Perrin/CNRS phototèque

Joseph Sifakis est le premier Français à recevoir le prix Turing, l'équivalent du prix Nobel en informatique.

---

L’ACM (Association for Computing Machinery) vient de vous décerner le prix Turing, l’équivalent du prix Nobel en informatique. Que ressentez-vous ?Joseph Sifakis : C’est évidemment un très grand honneur qui vient comme une reconnaissance ou une confirmation de l’intérêt de mes travaux. C’est aussi une grande responsabilité. En effet, même si je suis connu dans mon domaine, je deviens d’un coup un personnage public. Depuis quelques jours, on m’invite à prendre position sur des questions diverses et variées, qui vont au-delà de mes compétences techniques ! Cette notoriété nouvelle m’invite donc aussi à la prudence.

Concrètement, ce prix couronne des travaux développés depuis le début des années 1980 sur une technique appelée model checking. De quoi s’agit-il ?
J.S. : Faisons une comparaison. Lorsqu’un ingénieur construit un pont, il dispose des équations de la mécanique qui lui indiquent comment s’y prendre pour que son ouvrage ne s’effondre pas. Inversement, en informatique, parce que cette science n’a qu’une cinquantaine d’années, aucune théorie générale n’existe actuellement. Lorsqu’un ingénieur élabore un microprocesseur, un logiciel, le pilote automatique d’un avion ou l’électronique d’un appareil photo, il n’a pas d’autre solution que de le tester une fois celui-ci réalisé, afin de garantir son autonomie et/ou sa fiabilité. Or il est impossible d’expérimenter un système réel dans toutes les conditions possibles et imaginables. Ainsi, la problématique du model checking est le développement d’outils permettant de systématiser le test de systèmes informatiques. Concrètement, ce que nous avons proposé avec Edmund Clarke et Allen Emerson, c’est une méthode de test qui ne travaille pas sur le système réel, mais sur un prototype virtuel, un modèle, de celui-ci. La méthode consiste donc d’une part à extraire un modèle mathématique décrivant le système réel, d’autre part à analyser ce modèle afin de déterminer s’il répond ou pas à un certain nombre d’exigences qui caractérisent son comportement correct.

Sur le papier, le model checking est abstrait et très général. Néanmoins, cette méthode est aujourd’hui employée dans de très nombreuses applications.
J.S. : De façon amusante, lorsque nous avons introduit le model checking, en 1982, nous avons eu des difficultés pour publier nos travaux. Théoriquement en effet, cette méthode se proposait de tester des systèmes dont le nombre d’états possibles est potentiellement infini. Or, en pratique, elle ne permettait de tester que 10 000 de ces états. Nous étions alors assez peu crédibles ! C’est à partir de 1989 que tout a changé. J’ai alors initié, ici à Grenoble, une conférence considérée aujourd’hui comme « la » conférence du domaine. Et nous avons réussi dès lors à intéresser une large communauté de chercheurs ainsi que des industriels comme Intel et AT&T (American Telephone & Telegraph) à nos travaux.Après vingt ans d’efforts, nous avons partiellement surmonté les principaux obstacles grâce à des progrès sur deux fronts. Le premier, les techniques d’analyse qui sont devenues de plus en plus performantes. Et le deuxième, le nombre d’états d’un système que l’on peut tester – entre 2100 et 2300 – du fait de l’augmentation de la puissance des ordinateurs. Aujourd’hui, le model checking est utilisé dans toutes les industries où il y a de l’informatique : microélectronique, logiciels, avionique, automobile, etc.

D’ailleurs, toute votre carrière s’est faite à l’interface de la recherche fondamentale et de la recherche appliquée…
J.S. : Très franchement, en ce qui me concerne, je ne fais pas de distinction. Dans les grandes universités américaines par exemple, on trouve les bons résultats théoriques là où l’on fait aussi les meilleures applications ! Ainsi, le débat sur ce qu’il faudrait préférer ou soutenir est à mon avis stérile. L’important est de faire de la bonne recherche, c’est-à-dire une recherche créative. Pour ce faire, le système doit être capable de retenir les meilleurs chercheurs. D’une manière générale, je pense qu’il faut une forte sélectivité couplée à des carrières attrayantes, y compris financièrement. Cette sélectivité doit aussi ouvrir la possibilité aux meilleurs de travailler pour longtemps. C’est parce que j’ai pu travailler sans être ballotté au gré des modes ou des financements que j’ai pu réaliser mes travaux. Et ceci, y compris dans leur dimension la plus concrète.

Sur quoi travaillez-vous actuellement ?
J.S. : Je m’intéresse essentiellement à la question de savoir comment construire au mieux un système informatique afin de pouvoir le vérifier le plus facilement possible. Ceci dans le cadre d’une approche dite de composants : dans toutes les disciplines, on construit un système complexe à partir de composants élémentaires, comme une maison à partir de briques. Ainsi je travaille sur ce que pourraient être ces briques en informatique, et sur les différents types de « colles » permettant d’agencer entre elles ces différentes briques. C’est la question d’une théorie générale en informatique dont je vous parlais au début. Celle qui serait à l’informatique ce que la mécanique est à la construction des ponts.

Propos recueillis par Mathieu Grousson

Parcours d’un informaticien hors pair Directeur de recherche au CNRS, Joseph Sifakis est né en Crête en 1946. Après des études d’ingénieur électricien à l’École polytechnique d’Athènes, il vient en France afin de poursuivre des études de physique théorique. Mais il découvre l’informatique, une discipline alors en plein essor, et rejoint le laboratoire Imag de Grenoble. Il y soutient sa thèse de docteur-ingénieur en 1974, puis, en 1979, sa thèse de doctorat d’État qui porte sur le model checking. En 1993, il crée le Verimag, aujourd’hui rattaché au département des Sciences et Technologies de l’information et de l’ingénierie (ST2I) du CNRS, l’un des premiers laboratoires de recherche dans le domaine des systèmes embarqués critiques 1. Les travaux théoriques et technologiques effectués à Verimag sont notamment à l’origine de l’outil Scade, utilisé par Airbus pour la conception et la validation des systèmes critiques temps réel, et devenu une référence dans l’aéronautique. Soucieux d’allier recherche fondamentale et recherche appliquée, Joseph Sifakis, médaillé d’argent du CNRS en 2001, a établi des liens de longue durée entre Verimag et de nombreuses entreprises, dont ST Microelectronics et France Télécom. M.G. 1. Un système est dit « critique » lorsqu’une panne ou un dysfonctionnement de celui-ci peut avoir des conséquences dramatiques.