Proposé par l'association
ASSOC EPITA, ECOLE POUR L'INFORMATIQUE ET LES TECHNIQUES AVANCEES
Le 24/03/2014
Le Kremlin-Bicêtre (94270)
Le Kremlin-Bicêtre (94270)
Après avoir rejoint l'EDITE, le Laboratoire de recherche et développement de l'EPITA (LRDE) officialise désormais un partenariat avec la Faculté d'Informatique de la Masaryk University à Brno (République tchèque) dans le cadre de Spot, un des projets phares du LRDE traitant de model checking.
Spot : la solution du LRDE pour le model checking
« Le model checking, c'est vérifier qu'un modèle réponde aux contraintes qu'on lui a fixé », détaille Olivier Ricou, le responsable du LRDE, avant de poursuivre son explication avec un exemple simple. « Prenez un carrefour avec des feux de circulation : on n'a pas envie que tous les feux soient rouges ou verts en même temps. À cette première contrainte s'ajoute une seconde comme celle française qui consiste à dire que le feu fonctionne toujours dans le sens rouge, orange, vert et qu'il ne va jamais s'amuser à faire quelque chose comme rouge, orange, rouge, orange, vert, vert, rouge, vert. » Derrière cela, il y a donc « un petit programme » qui va être chargé d'allumer les couleurs qu'il faut les unes après les autres mais va également être chargé d'allumer les couleurs de chaque feu du carrefour. « S'il s'occupe d'un seul feu, on imagine bien qu'il risque d'y avoir doucement un décalage dans le temps et donc un risque de se retrouver avec tous les feux rougesou verts en même temps », précise-t-il. Le « petit programme » en question, même s'il n'a rien de compliqué, doit donc être propre et ne comporter aucune erreur. C'est là que le model checking entre en jeu : grâce à lui et à toute une algorithmie, la vérification devient possible.
« Des calculs qui mettent à genoux les ordinateurs les plus puissants »
La bibliothèque Spot du LRDE est une des bibliothèques de model checking largement reconnue dans le monde académique. Son but ne réside pour autant pas que dans les carrefours avec des feux tricolores. Il est encore plus ambitieux. « C'est d'être capable de vérifier qu'aucun train ne circule à contre-sens sur une voie ou que toute l'électronique embarquée dans un avion ne fera jamais aucune faute - ce qu'aujourd'hui, personne n'est encore capable de mettre en œuvre, poursuit Olivier Ricou. On en est encore aux balbutiements de la vérification. L'un des utilisateurs de la bibliothèque Spot, c'est la NASA qui utilise les algorithmes de traduction de propriétés de Spot dans un de leurs outils. C'est encore un domaine de recherche ou les applications sont difficiles à mettre en œuvre car dès que les systèmes deviennent un peu réels, ils deviennent plus complexes. Cela génère alors des calculs trop lourds même pour les ordinateurs les plus puissants. »
Dans la recherche, l'union fait la force
Retenu pour le programme de recherche bilatéral franco-tchèque PHC Barrande 2014, qui a pour objectif defavoriser les échanges scientifiques et technologiques entre des laboratoires de recherche des deux pays, le LRDE va renforcer l'expérience de ses équipes travaillant sur le model checking. Olivier Ricou en a bien conscience. « Le fonctionnement de la recherche, c'est simple : les chercheurs travaillent avec d'autres chercheurs selon les affinités, explique-t-il. On écrit des articles, on va à des conférences, on y rencontre des gens, on pose des questions, on discute et, au bout d'un moment, on se dit que ça serait bien de travailler ensemble. Voilà comment a commencé l'histoire avec la Masaryk University : comme le courant passait bien et les travaux étaient complémentaires, on a fait une demande de subvention pour nos doctorants afin qu'ils puissent profiter de la synergie entre les deux équipes. » Un financement, accordé grâce au programme Barrande, va permettre de réaliser des actions de mobilité de jeunes chercheurs, de doctorants et post-doctorants. Tout ça pour développer encore davantage la bibliothèque Spot. Autant dire qu'avec ce partenariat franco-tchèque, Spot n'a pas fini de briller.
Spot : la solution du LRDE pour le model checking
« Le model checking, c'est vérifier qu'un modèle réponde aux contraintes qu'on lui a fixé », détaille Olivier Ricou, le responsable du LRDE, avant de poursuivre son explication avec un exemple simple. « Prenez un carrefour avec des feux de circulation : on n'a pas envie que tous les feux soient rouges ou verts en même temps. À cette première contrainte s'ajoute une seconde comme celle française qui consiste à dire que le feu fonctionne toujours dans le sens rouge, orange, vert et qu'il ne va jamais s'amuser à faire quelque chose comme rouge, orange, rouge, orange, vert, vert, rouge, vert. » Derrière cela, il y a donc « un petit programme » qui va être chargé d'allumer les couleurs qu'il faut les unes après les autres mais va également être chargé d'allumer les couleurs de chaque feu du carrefour. « S'il s'occupe d'un seul feu, on imagine bien qu'il risque d'y avoir doucement un décalage dans le temps et donc un risque de se retrouver avec tous les feux rougesou verts en même temps », précise-t-il. Le « petit programme » en question, même s'il n'a rien de compliqué, doit donc être propre et ne comporter aucune erreur. C'est là que le model checking entre en jeu : grâce à lui et à toute une algorithmie, la vérification devient possible.
« Des calculs qui mettent à genoux les ordinateurs les plus puissants »
La bibliothèque Spot du LRDE est une des bibliothèques de model checking largement reconnue dans le monde académique. Son but ne réside pour autant pas que dans les carrefours avec des feux tricolores. Il est encore plus ambitieux. « C'est d'être capable de vérifier qu'aucun train ne circule à contre-sens sur une voie ou que toute l'électronique embarquée dans un avion ne fera jamais aucune faute - ce qu'aujourd'hui, personne n'est encore capable de mettre en œuvre, poursuit Olivier Ricou. On en est encore aux balbutiements de la vérification. L'un des utilisateurs de la bibliothèque Spot, c'est la NASA qui utilise les algorithmes de traduction de propriétés de Spot dans un de leurs outils. C'est encore un domaine de recherche ou les applications sont difficiles à mettre en œuvre car dès que les systèmes deviennent un peu réels, ils deviennent plus complexes. Cela génère alors des calculs trop lourds même pour les ordinateurs les plus puissants. »
Dans la recherche, l'union fait la force
Retenu pour le programme de recherche bilatéral franco-tchèque PHC Barrande 2014, qui a pour objectif defavoriser les échanges scientifiques et technologiques entre des laboratoires de recherche des deux pays, le LRDE va renforcer l'expérience de ses équipes travaillant sur le model checking. Olivier Ricou en a bien conscience. « Le fonctionnement de la recherche, c'est simple : les chercheurs travaillent avec d'autres chercheurs selon les affinités, explique-t-il. On écrit des articles, on va à des conférences, on y rencontre des gens, on pose des questions, on discute et, au bout d'un moment, on se dit que ça serait bien de travailler ensemble. Voilà comment a commencé l'histoire avec la Masaryk University : comme le courant passait bien et les travaux étaient complémentaires, on a fait une demande de subvention pour nos doctorants afin qu'ils puissent profiter de la synergie entre les deux équipes. » Un financement, accordé grâce au programme Barrande, va permettre de réaliser des actions de mobilité de jeunes chercheurs, de doctorants et post-doctorants. Tout ça pour développer encore davantage la bibliothèque Spot. Autant dire qu'avec ce partenariat franco-tchèque, Spot n'a pas fini de briller.
Proposé par l'association :
ASSOC EPITA, ECOLE POUR …
Auteur : T. (Ancien élève de l'IPSA)
Date de rédaction : 24/03/2014
Coordonnées
de l'association
ASSOC EPITA, ECOLE POUR …
Auteur : T. (Ancien élève de l'IPSA)
Date de rédaction : 24/03/2014
Coordonnées
de l'association
ASSOC EPITA, ECOLE POUR L'INFORMATIQUE ET LE…
Adresse
:
14-16, rue Voltaire
94270 Le Kremlin-Bicêtre
Web : http://www.epita.fr
Tel : 01 44 08 01 01
Fax : 01 44 08 01 99
14-16, rue Voltaire
94270 Le Kremlin-Bicêtre
Web : http://www.epita.fr
Tel : 01 44 08 01 01
Fax : 01 44 08 01 99
Ce bouton vous permet d'envoyer un message via un formulaire à l'adresse email de l'association.
Nous ne dévoilons jamais les emails que nous avons dans notre base et l'association décidera seule si elle souhaite vous répondre.
Si vous êtes responsable de cette association, nous vous conseillons de tester cette fonctionnalité et de vérifier que vous recevez bien l'email.
Si ça n'est pas le cas, vérifiez que celui-ci n'a pas été classé par erreur dans votre dossier de "spam". Dans ce cas, déclarez-le comme "non-spam" pour recevoir les futurs messages.
Si vous souhaitez changer l'email de contact ou ayez un doute sur celui-ci, vous pouvez nous envoyer un message via ce formulaire.
Nous ne dévoilons jamais les emails que nous avons dans notre base et l'association décidera seule si elle souhaite vous répondre.
Si vous êtes responsable de cette association, nous vous conseillons de tester cette fonctionnalité et de vérifier que vous recevez bien l'email.
Si ça n'est pas le cas, vérifiez que celui-ci n'a pas été classé par erreur dans votre dossier de "spam". Dans ce cas, déclarez-le comme "non-spam" pour recevoir les futurs messages.
Si vous souhaitez changer l'email de contact ou ayez un doute sur celui-ci, vous pouvez nous envoyer un message via ce formulaire.
Coordonnées
14-16, rue Voltaire,
94270 Le Kremlin-Bicêtre
94270 Le Kremlin-Bicêtre
Toutes les actualités de l'association
-> voir toutes les actualités de cette association
Première promo de l’Executive MBA ISG+EPITA
18/11/2016 : Le Kremlin-BicêtreQuand les étudiants de Polytechnique et d’HEC s’immergent dans la Piscine de l’EPITA
05/11/2016 : Le Kremlin-BicêtreTrophée Excellencia 2016
21/10/2016 : Le Kremlin-Bicêtre« Être une femme qui entreprend, c’est un combat »
15/10/2016 : Le Kremlin-BicêtreLe CESIN, nouveau partenaire de l’EPITA et SecureSphere
10/10/2016 : Le Kremlin-BicêtreL’European Association for International Education 2016
01/10/2016 : Le Kremlin-BicêtreRetour sur la Semaine de la Recherche et de l’Innovation 2016
19/09/2016 : Le Kremlin-BicêtreGirls Can Code! 2016
04/09/2016 : Le Kremlin-BicêtreGirls Can Code! 2016
04/09/2016 : Le Kremlin-BicêtreLes IOI 2016
25/08/2016 : Le Kremlin-BicêtreL’EPITA lance son tout nouveau programme : le MSc « Computer Science »
09/07/2016 : Le Kremlin-BicêtreConcours National d’Informatique 2016
05/06/2016 : Le Kremlin-BicêtreConcours National d’Informatique 2016
05/06/2016 : Le Kremlin-BicêtreLa (cyber)défense, c’est l’affaire de tous
09/05/2016 : Le Kremlin-BicêtreIls ont passé le concours EPITA - IPSA
29/04/2016 : Le Kremlin-BicêtreLes oraux du concours EPITA - IPSA
17/04/2016 : Le Kremlin-BicêtreUne vidéo pour tout savoir sur les écrits du concours commun EPITA / IPSA
11/04/2016 : Le Kremlin-Bicêtre#CodeAvecLaPoste
21/03/2016 : Le Kremlin-BicêtreChat Online Concours Advance
16/03/2016 : ParisDungeon Monsters de Mana Cube
12/03/2016 : Le Kremlin-BicêtreLa Menace Fantôme : l'Entertainment face au numérique
01/03/2016 : ParisTrois étudiants s’illustrent lors du Google Hash Code 2016
24/02/2016 : Le Kremlin-BicêtreLa Colombie, nouveau partenaire de l’EPITA
16/02/2016 : Le Kremlin-BicêtreLe numérique cherche ses talents féminins
16/02/2016 : Le Kremlin-BicêtreStartUp42 by EPITA présente le Demo Day de sa 6e édition
11/02/2016 : Paris