En 1982, il invente le model checking

...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.

NEWSLETTER La Quotidienne

Nos journalistes sélectionnent pour vous les articles essentiels de votre secteur.

Votre demande d’inscription a bien été prise en compte.

Votre email est traité par notre titre de presse qui selon le titre appartient, à une des sociétés suivantes...

Votre email est traité par notre titre de presse qui selon le titre appartient, à une des sociétés suivantes du : Groupe Moniteur Nanterre B 403 080 823, IPD Nanterre 490 727 633, Groupe Industrie Service Info (GISI) Nanterre 442 233 417. Cette société ou toutes sociétés du Groupe Infopro Digital pourront l'utiliser afin de vous proposer pour leur compte ou celui de leurs clients, des produits et/ou services utiles à vos activités professionnelles. Pour exercer vos droits, vous y opposer ou pour en savoir plus : Charte des données personnelles.

LES ÉVÉNEMENTS L'USINE NOUVELLE

LES PODCASTS

Le rôle des jeux vidéo dans nos sociétés

Le rôle des jeux vidéo dans nos sociétés

Martin Buthaud est docteur en philosophie à l'Université de Rouen. Il fait partie des rares chercheurs français à se questionner sur le rôle du jeu vidéo dans nos...

Écouter cet épisode

Les coulisses d'un abattoir qui se robotise

Les coulisses d'un abattoir qui se robotise

Dans ce nouvel épisode de La Fabrique, Nathan Mann nous dévoile les coulisses de son reportage dans l'abattoir Labeyrie de Came, dans les Pyrénées-Atlantiques, qui robotise peu à peu...

Écouter cet épisode

La renaissance des montres Kelton

La renaissance des montres Kelton

Le designer Vincent Bergerat donne une nouvelle vie aux montres Kelton. Dans ce nouvel épisode du podcast Inspiration, il explique au micro de Christophe Bys comment il innove et recrée l'identité...

Écouter cet épisode

Connecter start-up et grands groupes

Connecter start-up et grands groupes

Dans ce nouveau numéro du podcast Inspiration, Thomas Ollivier, fondateur du Maif Start-up Club, répond aux questions de Christophe Bys. 

Écouter cet épisode

Tous les podcasts

LES SERVICES DE L'USINE NOUVELLE

Trouvez les entreprises industrielles qui recrutent des talents

BUREAU VERITAS

Expert(e) naval - Jauge (F/H)

BUREAU VERITAS - 11/06/2022 - CDI - Saint Herblain

+ 550 offres d’emploi

Tout voir
Proposé par

ARTICLES LES PLUS LUS