Nous suivre Industrie Techno

En 1982, il invente le model checking

Mathilde Lagier
...révolution conceptuelle qui rend l'informatique plus fiable.

Vérifier la validité d'un système logiciel ou matériel... avant même sa construction. Impossible ? Beaucoup l'ont pensé. Dans des disciplines fondées sur la physique, la chose est relativement aisée : la construction d'un pont par exemple est basée sur des équations mathématiques. Mais en informatique, une analyse des systèmes avant leur construction ne paraissait pas envisageable du fait de leur complexité, c'est-à-dire d'un trop grand nombre d'états à vérifier. Joseph Sifakis y est pourtant parvenu. En 1982, parallèlement à Edmund Clarke et Allen Emerson qui travaillaient tous deux sur le même sujet aux États-Unis, ce chercheur franco-grec a posé les bases de ce que l'on nomme le model checking. Cette méthode algorithmique permet de s'affranchir des erreurs de conception de matériel ou de logiciel en travaillant sur un modèle virtuel plutôt que physique.

Utilisé essentiellement par de très grands groupes

Joseph Sifakis, est né à Héraklion en Grèce en 1946. Il a d'abord étudié l'ingénierie électrique à l'École polytechnique d'Athènes. En 1970, fuyant la dictature, il quitte la Grèce pour rejoindre la France, et plus précisément l'université de Grenoble. Venu étudier la physique dans cette faculté de prestige, il fait la rencontre de Jean Kuntzmann, le fondateur d'Imag (fédération d'unités de recherche de la région grenobloise). Cet homme, mais aussi son intérêt pour l'informatique, pousseront l'ingénieur dans cette voie.

Sifakis a beaucoup oeuvré pour que les travaux de ses recherches sur le model checking soient transférés vers des partenaires industriels. C'est dans les années 1990 que les premières applications industrielles auront finalement lieu. Le model checking permet aujourd'hui la vérification de puces, protocoles de communication, logiciels pilotes de périphériques, systèmes critiques embarqués et d'algorithmes de sécurité. Beaucoup de moyens étant nécessaires à sa mise en oeuvre, il est utilisé surtout par de très grands groupes.

D'après le CNRS, l'impact industriel du model checking devrait être encore plus significatif dans les années à venir notamment pour la vérification des processeurs et des systèmes critiques embarqués.

LE MODEL CHECKING AUJOURD'HUI

- D'après le laboratoire Verimag, le « model checking», est actuellement la méthode la plus utilisée pour la vérification des applications industrielles. - La méthode a été adoptée par de grands groupes comme Google, Intel ou encore France Telecom.

1979

Joseph Sifakis soutient sa thèse portant sur les méthodes de vérification des systèmes finis.

1982

Avec Edmund Clarke et Allen Emerson il pose les bases théoriques du « model checking »

1998

D'importants groupes comme Intel commencent à utiliser le « model checking ».

2007

Le prestigieux prix Turing est décerné à Sifakis, Clarke et Emerson pour leurs recherches.

vous lisez un article d'Industries & Technologies N°0908

Découvrir les articles de ce numéro Consultez les archives 2009 d'Industries & Technologies

Bienvenue !

Vous êtes désormais inscrits. Vous recevrez prochainement notre newsletter hebdomadaire Industrie & Technologies

Nous vous recommandons

MESURE

MESURE

Contrôler mieuxRéaliser une mesure n'est pas un acte anodin, car elle permet de prendre une décision technique ou économique, voire les deux. Cet[…]

01/04/2009 | HorizonLes livres
GESTION DES ACTIFS

GESTION DES ACTIFS

En 1972, il invente le scanner médical...

En 1972, il invente le scanner médical...

QUAND LES INGENIEURS SE CONFIENT...

QUAND LES INGENIEURS SE CONFIENT...

Plus d'articles