nos newsletters
Abonnez-vous à Micro Hebdo : 4,90 €/mois
Abonnez-vous à l'Ordinateur Individuel : 3 €/mois
Abonnez-vous à la version digitale
Abonnez-vous à 01Business et Technologies : 19 €/mois
Un Français reçoit l'équivalent du prix Nobel d'informatique
Joseph Sifakis, premier Français à recevoir le prix de Turing, nous explique ses travaux de recherche sur le Model Checking.
2007 est décidément une grande année pour la recherche française. Après
l'attribution du prix Nobel de physique 2007, en octobre dernier au français Albert Fert,
ainsi qu'à Peter Grünberg, c'est un autre chercheur français, Joseph Sifakis qui vient de recevoir le prix Turing 2007.
Cette récompense est l'équivalent du prix Nobel d'informatique. Elle a été décernée conjointement à Edmund M. Clarke et E. Allen Emerson des universités américaines de Carnegie Mellon et du Texas.
Joseph Sifakis est aujourd'hui chercheur CNRS au laboratoire Verimag à Grenoble, dont il est le fondateur. Laboratoire qui travaille sur les systèmes embarqués critiques.
<i> 01net. :</i> pour quels travaux de recherche avez-vous reçu cette récompense ?
Joseph Sifakis : Nous avons travaillés tous les trois, d'abord indépendamment, puis ensemble, et ensuite avec l'industrie, sur la théorie et la technologie du ' Model Checking '.
D'habitude, les systèmes [c'est à dire un ensemble de composants, logiques comme physiques, NDLR] sont validés par des tests qui sont réalisés sur des prototypes physiques. Mais, cette méthode suppose qu'on arrive à
réaliser le modèle physique. Et beaucoup de réalisations de systèmes complexes échouent avant que l'on soit parvenu à les réaliser.
D'autre part, on ne peut pas vérifier exhaustivement toutes les situations avec un prototype physique. On ne peut pas non plus observer les réactions de tous les éléments qui composent le système. Certains composants sont inobservables
sans perturber le système.
L'idée du ' Model Checking ' est donc de travailler sur un modèle virtuel plutôt que sur un prototype physique, et de le vérifier ?" on parle donc de vérification et non plus de test ?"
avant de le produire. Mais deux problèmes se posent alors : la construction de ce modèle, et la définition de l'algorithme pour comparer le modèle aux exigences.
Dans les systèmes complexes, on se trouve notamment confrontés à ' l'explosion des états '. Plus le modèle détient de composants plus la manière dont il va réagir ?" son état futur ?" va
être difficile à déterminer. Il y a donc une difficulté inhérente pour analyser ce nombre d'états du système. Mais nous avons réussi à résoudre ces problèmes.
Le ' Model Checking ' est-il utilisé aujourd'hui ?
Oui, l'industrie l'utilise aujourd'hui couramment. IBM et Intel par exemple, s'en servent pour analyser les logiciels critiques ou pour valider les processeurs. Mais le ' Model Checking ' ne peut être employé pour vérifier tous les systèmes. Le système doit être conçu avec certaines précautions pour permettre ensuite d'extraire le modèle.
Oui, l'industrie l'utilise aujourd'hui couramment. IBM et Intel par exemple, s'en servent pour analyser les logiciels critiques ou pour valider les processeurs. Mais le ' Model Checking ' ne peut être employé pour vérifier tous les systèmes. Le système doit être conçu avec certaines précautions pour permettre ensuite d'extraire le modèle.
Le ' Model Checking ' permet alors d'obtenir des systèmes plus fiables qui seront utilisés par exemple dans l'avionique.
Quels sont vos travaux actuels ?
Au sein du laboratoire Verimag, je travaille sur les techniques de construction des systèmes pour simplifier leur vérification. Si j'ai une théorie de constructivité, je peux alors créer des modèles et les vérifier plus simplement. En informatique, cela va permettre de construire des systèmes de plus en plus sûrs à des coûts moindres.
Au sein du laboratoire Verimag, je travaille sur les techniques de construction des systèmes pour simplifier leur vérification. Si j'ai une théorie de constructivité, je peux alors créer des modèles et les vérifier plus simplement. En informatique, cela va permettre de construire des systèmes de plus en plus sûrs à des coûts moindres.
Vous êtes également le coordinateur du réseau d'excellence Artist2, sur quoi travaille-t-il ?
Artist 2 est un réseau d'excellence sur les systèmes embarqués. Nous travaillons sur leur conception. L'embarqué pose les problèmes de l'autonomie et du coût. Tout notre effort porte donc sur le développement de théories qui permettront de construire des systèmes fiables à bas coût.
Artist 2 est un réseau d'excellence sur les systèmes embarqués. Nous travaillons sur leur conception. L'embarqué pose les problèmes de l'autonomie et du coût. Tout notre effort porte donc sur le développement de théories qui permettront de construire des systèmes fiables à bas coût.
Pour cela, il faut tout repenser. Les systèmes d'exploitation en temps réel, par exemple, sont aujourd'hui trop monolithiques et volumineux. Pour les systèmes embarqués, il faut des OS beaucoup plus modulaires.
Pour vous, quelles seront les technologies de demain ?
L'intelligence ambiante ! On va trouver de plus en plus de systèmes embarqués partout, et ils seront de plus en plus invisibles. Ils coopéreront entre eux pour nous fournir des services qui vont de plus en plus faciliter la vie des
gens.
Va alors se poser la question de la gestion des systèmes. Elles seront de plus en plus complexes et leur défaillance pourrait avoir des conséquences catastrophiques. On le voit déjà aujourd'hui avec les accidents dans la manipulation
des appareils de radiologie.
D'où l'importance de plus en plus grande des vérifications... et du ' Model Checking '.
envoyer
par mail
par mail
imprimer
l'article
l'article
Avis sur «Un Français reçoit l'équivalent du prix Nobel d'informatique»
Alan
de
fabounio
, posté le 07 février 2008 à 18h31
qui de vous connait Alan Turing ?
Quand on connait les circonstances de sa disparition, on ne peut s'empecher de faire le rapprochement avec la pomme d'apple....
Quand on connait les circonstances de sa disparition, on ne peut s'empecher de faire le rapprochement avec la pomme d'apple....
alerter le modérateur
Docteur
de
bastit
, posté le 07 février 2008 à 19h34
Outre qu'il a une bonne gueule, ce scientifique est, manifestement un "enseignant" car son exposé me parait lumineux, même s'il reste manifestement dans des généralités.
Bravo!!
Bravo!!
alerter le modérateur
Félicitations
de
Willy.r
, posté le 07 février 2008 à 21h45
Pour avoir suivi un cours à Grenoble portant sur les bases du model checking, je ne peux qu'appuyer l'idée qu'il s'agit là d'un outil d'une très grande puissance.
alerter le modérateur
Bravo
de
samAlex
, posté le 08 février 2008 à 08h58
En tout cas bravo. Etudiany en informatique dans ce cdomaine justement, j'ai assisté à des conference qu'il présentait et il le mérite vraiment. En tout cas le model checking a de l'avenir devant nous.
alerter le modérateur
Mais où est l'avenir ?
de
Galim
, posté le 08 février 2008 à 13h51
de l'avenir "devant nous" ou devant lui ???
alerter le modérateur
à lire aussi
SUR LES MÊMES THÈMES 
Nos partenaires