Nom de fichier :
|
Inria-1153-CONVECS-180sec-FR.mp4
|
Titre :
|
Mon équipe en 180 secondes : CONVECS
|
Année :
|
2018
|
Durée (min) :
|
00:02:50
|
Publications :
|
http://videotheque.inria.fr/videotheque/doc/1153
|
Autres versions :
|
Master VF : 1153 Master VEN : Autre : Lien externe :
|
Lien Equipe-projet :
|
|
Lien Centre de Recherche :
|
|
Mots clés :
|
|
N° master :
|
1153
|
Durée :
|
02 min 50 sec
|
IsyTag :
|
botte
- bugs
- chercher
- CONVECS
- évènements
- foin
- Mateescu
- modèle
- modéliser
- s’agit
- système
- Vérification et preuve de programme
|
Transcription automatiqu :
|
Bonjour Je m'appelle Radu Mateescu et récemment j'étais en voyage à l'étranger pour aller à une conférence quand brusquement le train s'est arrêté en pleine voie et tous les systèmes qui fonctionnaient dedans se sont arrêtés les uns après les autres Après avoir passé une demi heure dans le silence et l'immobilité la seule solution trouvée a été de remorquer le train jusqu'à la dernière gare où le logiciel embarqué a été entièrement redémarré ce qui a tout remis en ordre Et pendant tout ce temps comme l'arrivage de l'air avait été coupé aussi les voyageurs ont respirer parcimonieusement La solution du redémarrage complet ne peut pas bien s'appliquer à un avion qui est en plein vol ni à une voiture intelligente qui roule sur autoroute ni même à une puce électronique Et en fait comme l'informatique est devenu maintenant omniprésent des objets connectés jusqu'au niveau des processus métier dans les organisations les bugs peuvent s'infiltrer un peu partout et peuvent avoir parfois des conséquences catastrophiques Donc le job de l'équipe CONVECS de traquer impitoyablement les bugs bien en proposant des langages avec sémantique mathématique propre et syntaxe facile à apprendre pour modéliser formellement le comportement et les propriétés attendues du système à vérifier ensuite il s’agit de chercher les bugs dans l'espace d'état du système qui contient tous les entrelacements d'évènements possibles produits par les différentes choses qui s'exécutent en parallèle et qui communiquent entre-eux dans le système C'est ce qu'on appelle la vérification de modèle ou le modèle checking Chercher un séquence d'évènements qui mène un état fautif par exemple un blocage c'est comme chercher une aiguille dans une botte de foin et quand la botte de foin fait un milliard d'états il y a besoin d'avoir des algorithmes et des outils de vérification efficaces comme ceux que l'équipe CONVECS s'efforce de développer et de diffuser dans le monde Et en plus de cela nous travaillons directement avec des partenaires industriels comme Nokia Orange Labs ou Tiempo Secure pour les aider à modéliser et à valider leurs applications critiques Et nous apportons ainsi notre modeste contribution à éradiquer les bugs et à rendre le monde numérique plus propre et plus sûr Je vous remercie
|