Dans l’esprit du système… portrait de Joseph Sifakis

© Photo : DR.

Propos recueillis par Jeanne Morcellet, 16 mars 2012.

Quel a été votre parcours d’étudiant ?

Après avoir obtenu mon diplôme d’ingénieur électricien de l’Université technique d’Athènes, je suis arrivé en France en août 1970 pour y poursuivre mes études. Je devais faire une thèse en physique théorique mais très vite j’ai été intéressé par l’informatique qui n’en était alors qu’à ses débuts. J’ai commencé des études à l’Imag (Informatique et mathématiques appliquées de Grenoble), passé une maîtrise d’informatique suivie d’un DEA et d’une thèse de docteur ingénieur. J’ai obtenu un poste CNRS en 1974 que j’occupe toujours.

Que vous a apporté votre formation en Grèce ?

Un goût pour les applications et une motivation très forte de faire de la théorie qui serve à quelque chose. J’ai toujours trouvé plus intéressant le travail de la formalisation d’un problème pratique que la solution d’un problème bien formulé. Pour moi, les problèmes pratiques ont toujours été une source d’inspiration. L’interaction entre théorie et pratique est un cercle vertueux qui fertilise la pensée et conduit à la découverte de nouvelles directions de recherche fondamentale.

Vous recevez en 2008 le prestigieux prix Turing, avec Ed Clarke et Allen Emerson, qui couronne une technique et une méthode appelées model checking : de quoi s’agit-il exactement ?

Il s’agit d’un cadre théorique et en même temps d’une méthode algorithmique pour la vérification des systèmes informatiques. Son application permet de vérifier (prouver) qu’un système représenté par un modèle formel satisfait des propriétés formulées dans une logique temporelle. Cette dernière est utilisée pour exprimer des propriétés essentielles du comportement du système, telles que des propriétés de sûreté. Contrairement à des méthodes de validation ad hoc fondées sur le test, le model checking fournit la preuve formelle qu’un système est correct. Il faut toutefois souligner que l’application de méthodes de vérification rigoureuses souffre de certaines limitations intrinsèques soulevées par la théorie de la calculabilité dont les fondements ont été posés par Alan Turing.

Quelle est votre définition personnelle d’un système embarqué critique ?

L’aérospatiale est l’un des secteurs où il est crucial de garantir le comportement des systèmes embarqués.
Ici, le centre de contrôle Jupiter 2, en Guyane.
© Photo : CNES/ESA/Arianespace/Optique Vidéo CSG/P. Baudon, 2012.

Un système embarqué est un système informatique enfoui qui interagit d’une manière continue avec son environnement physique comme par exemple le pilote automatique d’un avion, les composants électroniques d’une voiture, d’un appareil électroménager ou le système d’un téléphone portable. Contrairement aux systèmes traditionnels, ordinateurs de bureau ou serveurs, ils doivent répondre à un ensemble d’exigences techniques de réactivité, d’autonomie, de sûreté et de sécurité. Le temps de réponse de votre ordinateur peut être arbitrairement long, ce qui n’est pas permis pour un contrôleur de vol. En cas de problème, vous redémarrez votre ordinateur, ce qui n’est pas facile pour les composants embarqués de votre voiture. D’où le concept de « criticité ». Il faut garantir pour les systèmes embarqués, surtout pour ceux qui assurent des fonctions critiques, leur bon comportement.

Pourquoi avoir créé Verimag ?

Verimag a été créée en janvier 1993, comme une unité mixte industrielle entre l’Imag et la société Verilog, d’où son nom. L’objectif était de transférer des résultats de recherche développés dans notre équipe. L’opération la plus réussie a été le transfert du langage Lustre vers l’environnement de programmation synchrone Scade, utilisé par Airbus depuis plus de quinze ans pour le développement de systèmes critiques. Depuis janvier 1997, Verimag est une unité mixte de recherche associée au CNRS et à l’université de Grenoble.

Quels sont les secteurs pour lesquels vous œuvrez ?

Après avoir travaillé pour les systèmes embarqués critiques (nucléaire, transport), je me suis intéressé aux systèmes « best effort » tels que les systèmes multimédia et les télécommunications. Plus récemment, je me suis impliqué dans des projets de recherche sur des systèmes de « criticalité mixte » et notamment des systèmes résultant de la convergence des technologies de l’embarqué et des services internet.

Les marchés pourraient-ils devenir plus collaboratifs ? Quels seraient les enjeux d’une standardisation ?

L’absence de standardisation permet une fragmentation des marchés et la création de « niches » pour certains acteurs industriels. Par exemple, une unification des standards pour systèmes embarqués critiques aurait permis dans une certaine mesure l’intégration des marchés de l’embarqué pour l’avionique, le spatial, le ferroviaire et l’automobile. Une unification peut mettre en danger des industries ayant des positions fortes dans ces domaines et, en revanche, pourra donner une position dominante à des géants de l’industrie du logiciel.

Quel est pour vous le statut « exact » de l’informatique ? Une science au même titre que la physique ou la chimie, ou plutôt une technologie de pointe ? Sert-elle à décrire le monde ou à comprendre le monde ?

L’informatique est une discipline à part entière avec ses propres concepts et paradigmes. Elle traite des problèmes liés à la représentation, transformation et transmission de l’information. Elle étudie tous les aspects du calcul y compris les modèles de calcul, la programmation et la conception des systèmes. L’information est une entité distincte de la matière et de l’énergie. Elle peut être stockée, transformée et consommée. Elle est immatérielle mais elle a besoin de média pour sa représentation. L’informatique ne se réduit pas à une branche des mathématiques. Comme toute discipline scientifique, elle s’appuie sur les mathématiques mais elle développe un corpus de résultats théoriques pour expliquer et prévoir les propriétés des systèmes informatiques. Bien sûr, ces résultats peuvent être validés expérimentalement. Enfin, je soulignerai une importante différence avec les sciences physiques. Ces dernières ont comme premier objectif de comprendre un monde existant en découvrant des lois qui gouvernent ses phénomènes. L’informatique étudie des mondes artificiels composés de systèmes de calcul. Son premier objectif est le développement de théories permettant la construction de systèmes de qualité et de performance garanties.

Sur quoi travaillez-vous aujourd’hui ?

Je travaille sur une théorie pour la construction des systèmes à partir de composants. Cette théorie fournit les outils théoriques et pratiques pour obtenir des systèmes complexes par composition de composants plus simples tout en garantissant par construction leur bon fonctionnement. Elle doit, en principe, permettre de dépasser les limitations des approches par vérification et ouvrir la voie vers des techniques de conception rigoureuses permettant de garantir la qualité et les performances des systèmes informatiques.

Cet article est paru dans la revue DocSciences n°14 Alan Turing : La pensée informatique, éditée par le CRDP de l’Académie de Versailles en partenariat avec Inria.