tous les documents
  • tous les documents
  • Images
  • Films
  • Rushes
  • Publications
  • Audio
Recherche avancée
Ensemble de recherche :
tous les documents
  • tous les documents
  • Images
  • Films
  • Rushes
  • Publications
  • Audio
Recherche par couleur
Ensemble de recherche :
tous les documents
  • tous les documents
  • Images
  • Films
  • Rushes
  • Publications
  • Audio
Code HTML Copiez-collez le code ci-dessous pour l'intégrer dans une page Web.
Titre :
Marie Duflot, informatique débranchée : un château pas très fort.
Légende - Résumé :
Comprendre l'informatique en jouant : un château pas très fort. L'informatique débranchée permet de s’initier aux algorithmes, à la vérification, à la détection d’erreurs, etc. sans ordinateur. Public : lycéens.
Avec Marie Duflot-Kremer, maître de conférence à l'Université de Lorraine, membre de l'équipe VERIDIS du centre Inria Nancy - Grand Est et du LORIA.
Nom de fichier :
Inria-1050_MarieDuflot_ChateauFort_VF.mp4
Titre :
Marie Duflot, informatique débranchée : un château pas très fort.
Année :
2017
Durée (min) :
00:19:19
Publications :
https://videotheque.inria.fr/videotheque/doc/1050
Autres versions :
Master VF : 1050
Master VEN :
Autre : Lien externe :
Lien Equipe-projet :
Lien Centre de Recherche :
Mots clés :
N° master :
1050
Durée :
19 min 19 sec
IsyTag :
atteindre - Celui-ci - château - chemin - est-ce - état-là - fenêtre - flèche - formule - j' - l' - modèle - opérateur - pièce - pièce-là - propriété - qu' - regarder - système - torche - trésor - vérifier
Transcription automatiqu :
Dans cette activité on représente un château ici pour lequel il y a différentes pièces qui sont représentées par des ronds En informatique on appelle ça des états Et il y a des passages entre les pièces ici que en informatique on appelle des transitions Donc dans un château-fort en général c'est assez habituel que quand je peux passer d'un état à un autre je peux revenir dans l'autre sens Mais il est zarbi mon château Ici je peux passer de cette pièce-là à cette pièce-là mais il n'y a pas de flèche pour faire le retour Pourquoi Eh ben justement là il faut avoir l'idée pour se dire qu'est ce que je peux mettre comme truc logique sur un truc d'informaticien complètement hein Eh bien c'est parce mon château il est plein de passages secrets et je peux depuis cette pièce activer le passage secret qui va me permettre de passer dans celle-là Mais dans l'autre sens y a pas de bouton de truc pour l'activer dans l'autre sens Alors il y a même un truc encore encore plus tordu C'est un passage secret qui permet d'aller d'une pièce faire un tournicoton et retourner dans la même pièce ça s'appelle une boucle sur un état Alors des fois ça a un sens en informatique En château-fort il faut vraiment être tordu pour avoir fait un passage secret qui fait retourner dans la même pièce Sur ce système sur ce château on va vouloir vérifier des propriétés Et pour vérifier ces propriétés tout comme on avait besoin d'un modèle pour décrire le château d'accord pour dire précisément de quelles pièces on pouvait passer à quelle autre et en combien d'étapes pour vérifier les propriétés on va avoir besoin d'un langage particulier et ce langage s'appelle un langage logique et pour cela on a toute une série d'opérateurs Comme on pourrait appeler le plus de l'addition un opérateur ici c'est des opérateurs spéciaux pour la logique celui qui a plusieurs flèches dit que dans un état pour tout chemin à partir de cet état on a une certaine propriété qu'on va devoir écrire avec les autres opérateurs Une seule flèche veut dire qu'à partir d'ici il existe un chemin qui satisfait une certaine propriété et puis le long d'un chemin on a quatre opérateurs Un qui dit que un jour à un moment le long de ce chemin quelque chose est vrai un autre qui dit que toujours le long de ce chemin quelque chose est vrai Celui-ci qui est un petit peu plus compliqué qui dit qu'une chose est vraie jusqu'à ce qu'une autre devienne vraie le dernier signifie que dans la pièce suivante donc après une étape une flèche dans le château on va arriver dans un état qui satisfait une propriété Pour comprendre il faut bidouiller avec Donc par exemple je vous demande je peux aller voir une fenêtre j'ai besoin de il existe un chemin le long duquel un jour j'ai une fenêtre et donc c'est ici si je lis ça il existe un chemin le long duquel un jour j'ai une fenêtre Pourquoi on utilise ce genre de langage et pas le français parce qu'en français il y a beaucoup de phrases qui sont ambiguës Et donc pour une même phrase on ne sait pas exactement ce que cela veut dire Si on sait pas exactement ce que veut dire la phrase en français ça va être très difficile de le vérifier sur mon château ici Et là ces langages ont été écrits de telle sorte que pour une formule logique une phrase avec mon langage logique je n'ai qu'une seule interprétation possible et ensuite je vais pouvoir aller regarder si dans mon château je satisfais cette formule Donc je pars de mon état départ et je vais regarder s'il existe un chemin qui me mène devant une fenêtre Donc ici je pour faire ce chemin-là ici en deux étapes je suis devant la fenêtre Ou je peux faire des chemins plus longs par exemple je pourrais aller dans cette pièce revenir repartir passer par ici est ensuite arriver devant la fenêtre donc non seulement il existe un chemin mais il en existe plusieurs Donc là ma formule telle qu'elle est écrite ici est vraie dans mon château Et après ce machin-là en fait il faudrait mettre un ET un OU ou je sais pas quoi Enfin là tout seul il ne veut pas dire grand chose Si on voulait dire tous les chemins où y'aurait pas de fenêtre on prendrait pas Ah je le prendrais pas ça je sais pas l'exprimer Alors après avec cette formule si je veux dire des choses légèrement différentes je peux légèrement changer ma formule Par exemple si j'ai envie de dire que je peux atteindre un trésor eh ben je remplace juste la fenêtre par le trésor Ici ça veut dire je peux atteindre le trésor Et puis je peux vouloir exprimer d'autres propriétés par exemple est-ce qu'il est possible de me promener dans le château sans jamais atteindre le trésor donc du coup la possibilité de faire quelque chose ça s'exprime avec cet opérateur-là mais maintenant je veux dire ne jamais croiser le trésor ne jamais croiser le trésor avec mes opérateurs ici c'est d'être toujours dans une pièce où il n'y a pas de trésor donc je rajoute l'opérateur toujours ici Et j'ai envie de dire il n'y a pas de trésor Pour ça l'opérateur non qui me dit il n'est pas vrai que donc il existe un chemin où toujours le long de ce chemin il n'est un vrai qu'il y a trésor donc il n'y a pas de trésor Donc cette formule me dit je peux me promener dans le château à l'infini sans m'arrêter sans jamais rencontrer un trésor Par exemple je peux faire ce chemin-là et puis ensuite m'amuser à tourner en rond ici et là je ne passerai jamais par le trésor Et puis je peux changer de chemin Ah ici je suis obligée de revenir et puis je peux faire tout un tas de choses et faire un chemin qui va peut-être boucler jusqu'à la fin des temps ici et qui ne passera jamais dans un des deux états où il y a un trésor Alors j'utilisé cet opérateur-là mais j'ai l'autre celui-ci Qu'est-ce que je pourrais dire avec celui-là je pourrais dire hum est-ce qu'il est vrai que quoi que je fasse dans la pièce il y aura toujours un tableau une torche ou une fenêtre comment ça s'écrit Ben ça s'écrit avec quel que soit le chemin que je prends toujours le long de ce chemin j'ai j'ai dit une torche une fenêtre ou un tableau donc je vais prendre ces opérateurs et j'ai envie de dire l'un de ces trois-là eh ben l'un de ces trois-là ça va se faire avec l'opérateur OU donc ici une fenêtre ou une torche ou un tableau et pour être même plus précis pour savoir que c'est pas toujours fenêtre ou bien l'un des deux autres je vais mettre ici des parenthèses Donc ça veut dire quel que soit le chemin que je prends à tout instant le long de ce chemin j'ai soit une fenêtre soit une torche soit un tableau Alors la question peut être est-ce que c'est vrai sur ce modèle-là Si on regarde le modèle on voit que tous les états ont l'une de ces trois choses sauf l'état qui est en haut ici Donc on peut dire c'est pas vrai parce que si j'arrive dans cet état-là je ne satisfais pas une fenêtre ou une torche ou un tableau mais si regarde bien le modèle et cet état-là les flèches qui sont connectées à cet état ce sont toutes des flèches qui s'en vont de l'état Y'a aucune flèche qui rentre dans cet état-là ce qui veut dire que si je pars de l'état de départ j'ai aucune chance d'arriver ici un jour Je suis d'accord que pour le concepteur du château c'est quand même totalement idiot parce qu'il y a un trésor Et il y a aucun moyen d'aller jusqu'à ce trésor-là à part peut-être de casser un mur Donc mon système ici où tous les états satisfont fenêtre torche ou tableau sauf celui-ci Mais comme on peut pas accéder à celui-ci mon système ici satisfait la formule J'ai utilisé certains de mes opérateurs mais j'ai pas encore utilisé celui-ci qui dit dans la pièce suivante Et justement je vais l'utiliser parce que là maintenant j'ai envie de dire quoi que je fasse après deux déplacements je suis dans une pièce où il y a une torche Alors déjà quoi que je fasse ça va être cet opérateur-là après deux déplacements eh ben ça ce serait après un déplacement puisque c'est dans la prochaine pièce Si j'ai envie de faire après deux déplacements eh ben je vais juste le mettre deux fois de suite donc ça ce serait quoi que je fasse après un deux déplacements je vois une torche Donc sur mon système ici Après deux déplacements c'est pas très compliqué il suffit juste que je suive deux flèches à partir du départ Donc je peux pour la première flèche je peux aller par ici et du coup la deuxième flèche elle peut m'amener soit là soit là et effectivement cet état a une torche et celui-ci aussi Ou bien à partir du départ je peux partir là Et puis après en une transition je reviens ici j'ai une torche Donc cette propriété ici elle est satisfaite sur mon système je peux aussi demander s'il est possible d'atteindre le trésor en exactement trois transitions donc ici c'est si je peux ça s'exprime avec cet opérateur-là Est-ce qu'il est possible en trois étapes en trois transitions d'atteindre le trésor ce serait cette formule-là Et donc sur mon système je vais essayer d'atteindre le trésor en trois transitions Ici une deux c'est pas possible une deux je vais pas y arriver non plus une deux trois Oui là c'est possible En trois transitions je suis dans une salle où y'a le trésor Je suis d'accord que la troisième étape je l'ai fait en restant sur mes pas mais mon système ici tel qu'il est écrit il satisfait cette propriété-là Est-ce que quelqu'un qui a peur du noir peut atteindre le trésor Pour ça une personne qui a peur du noir il faut se dire qu'elle ne peut aller dans des pièces que s'il y a une torche ou bien une fenêtre ou les deux éventuellement Donc en particulier dans cette pièce-là la personne qui a peur du noir ne va jamais y passer Donc pour exprimer cette propriété je vais prendre l'opérateur il existe un chemin où je vais atteindre un trésor à un moment donc la question c'est est-ce qu'il existe un chemin où à un moment je vais avoir le trésor et tous les moments avant d'atteindre le trésor je dois avoir soit une torche soit une fenêtre donc je prends une torche une fenêtre je veux l'un des deux donc avoir une torche ou une fenêtre Pour faire propre je vais mettre des parenthèses s'il existe un chemin est-ce qu'il existe un chemin où j'ai une torche ou une fenêtre jusqu'à ce que j'arrive dans une pièce où il y a un trésor Parce que en fait il a besoin de deux choses Un truc est vrai jusqu'à ce qu'un autre devienne vrai il est rouge jusqu'à ce qu'il devienne vert Donc là il manque le il est rouges ou quoi que ce soit que tu voulais y mettre Sauf que cette formule elle sous-entend que la personne qui a peur du noir quand elle est devant le trésor elle s'en fiche de voir des torches ou des fenêtres si elle a vraiment très peur noir alors il va falloir rajouter quelque chose il va falloir demander à ce qu'y ait un trésor et et aussi une torche ou une fenêtre ça commence à devenir un tout petit peu compliqué mais ça ce que je construis ici cette formule logique c'est l'équivalent de la phrase quelqu'un qui a peur du noir peut atteindre le trésor Il est possible de passer dans des pièces avec des torches ou des fenêtres jusqu'à ce que on soit dans une pièce qui a un trésor et une torche ou une fenêtre Finally globally until et next je vous les ai appelés avec des trucs en français Mais vous avez toute la logique CTL Quand vous sortez de cette pièce vous pouvez dire que vous connaissez la logique CTL C'est comme tout à l'heure c'était le vrai modèle de Huffman là c'est le vrai modèle CTL La question qu'on peut se poser après c'est comment un ordinateur parce que quand même c'est pas un humain qui va vérifier ça comment un ordinateur pourrait vérifier si une formule telle que je l'ai écrite avec mes opérateurs est vraie sur ce système sur ce château parce que pour l'instant on n'a fait que regarder si à la main on pouvait savoir si la propriété était vraie dans le château l'ordinateur lui va faire ça de manière automatique donc je vais partir sur une formule qui dit qu'il existe un chemin le long duquel un jour j'atteins le trésor Alors comment fait l'ordinateur pour ça Déjà il y a des états à partir desquels c'est très facile de savoir que la propriété est vraie ces états c'est ceux pour lesquels on est déjà dans le trésor Ces deux états-là l'ordinateur se dit c'est facile Il va juste regarder dans les états si jamais il y un petit trésor dessiné à côté de la pièce et puis ensuite j'ai envie de savoir quels sont les autres états qui satisfont ma formule Pour ça je peux me dire de cet état c'est facile puisque en une transition je vais dans un état qui a un trésor eh ben je vais faire cette méthode de manière systématique Je vais prendre un état où j'ai déjà un point dedans donc je sais qu'à partir de cet état je peux atteindre le trésor et puis ensuite je vais regarder toutes les transitions qui arrivent dans cet état Ici j'en ai quatre une deux trois et quatre Et je vais dire que l'état de départ de cette transition donc ici la pièce qui ici satisfait ma formule puisque en une étape je peux atteindre un état qui peut atteindre le trésor Donc ici je mets un point dans cette pièce cette pièce cette pièce Et puis pour la transition ici ce serait cette pièce-là qui a déjà un point et puis maintenant comme j'ai regardé toutes les tous les passages secrets toutes les transitions qui arrivaient dans cette pièce je vais mettre une croix pour dire cette pièce-là j'ai fini j'ai regardé tous les chemins qui y arrivaient Et puis je vais reprendre un autre état qui a un point par exemple celui-ci Je vais regarder toutes les transitions qui arrivent dans cet état-là c'est bien simple il n'y en a aucune Donc j'ai fini pour cet état-là et je continue Je prends par exemple celui-ci je regarde toutes les flèches qui arrivent dans cet état donc une deux trois et donc maintenant je sais que tous les états qui ont une croix satisfont la formule qui est ici et les états qui sont vides ne satisfont pas la formule et ça c'est pour moi un algorithme que je vais pouvoir traduire dans un langage pour l'ordinateur Et cet algorithme s'appelle un algorithme de point fixe parce que au départ on avait aucun état avec des points ou des croix Et petit à petit on a appliqué une méthode qui nous permettait d'augmenter l'ensemble des états qui avaient un point ou une croix dedans Quand ça rajoute plus rien j'ai un point fixe c'est-à-dire si je réessaye encore une fois ça va rien rajouté et j'ai gagné et donc je viens devant vos yeux ébahis de vous parler de mon cours de Master première année L'activité du château permet d'illustrer une technique qui existe en informatique ça s'appelle le model checking Et le model checking consiste à vérifier tous les comportements d'un système mais avant de pouvoir faire ça il faut faire une étape indispensable il faut prendre notre système par exemple un distributeur de boissons ou le train d'atterrissage d'un avion ou une centrale nucléaire et en réaliser un modèle C'est le dessin qu'on avait du château L'avantage c'est que quand on a une distribution d'un système qui est juste écrite à la main on pourrait l'interpréter de différentes façons Quand c'est représenté sous forme d'un automate comme c'était le cas pour le château eh bien du coup on sait exactement quels sont les comportements dans ce système donc c'est un modèle formel du système Pareil pour la propriété est-ce que je peux atteindre le trésor si j'ai peur du noir on va l'écrire dans un langage formel un langage logique Et ensuite il existe des programmes qui permettent de vérifier automatiquement si un système satisfait ou pas une propriété ou bien j'ai une torche dans l'état de départ communes et ça sera une formule acceptable Cette activité a été présentée sur un château avec des petits dessins sympas et puis des opérateurs qui ont des formes rigolotes C'est exactement les modèles qu'on réalise sur des systèmes et c'est exactement eux toutes les formules qu'on peut faire dans une véritable logique qui sert à faire de la vérification formelle Et cette méthode de vérification formelle ça s'appelle du model checking comment je vais vérifier cette formule je vais faire ça en regardant d'abord les formules simples qui sont à l'intérieur Donc je vais regarder quels sont les états qui satisfont y'a pas de trésor puis les états qui satisfont pour tous chemins toujours pas de trésor et enfin les états qui satisfont ma formule en entier Et du coup j'ai des étapes qui seront assez faciles et qui me permettront d'être assez simple pour que l'ordinateur puisse le faire de manière systématique Le model checking doit permettre de vérifier que tous les comportements du système satisfont une certaine propriété le problème c'est que on n'a pas moyen de les vérifier tous ce nombre de chemins au mieux il est en très grand nombre et au pire il est en nombre infini Donc on a besoin d'une méthode exacte qui va nous garantir qu'une propriété est satisfaite mais qui fonctionne en un temps fini Alors si on veut avoir une idée de combien de temps ça prend de faire de la vérification il faut savoir que le temps que ça prend c'est de l'ordre de grandeur de la taille de notre système donc les états et les transitions multiplié par la taille de la formule On peut se dire une multiplication c'est pas énorme Sauf que notre système en général il est très grand Cette activité est plutôt adaptée pour les élèves de toute fin collège voire de lycée et ça permet d'aborder différentes de choses qui vont assez loin dans le domaine de l'informatique
Inria-1050_MarieDuflot_ChateauFort_VF.mp4

Format : .mp4
761,7 Mo
1280 x 720 pixels
Inria-1050_MarieDuflot_C_HD.MP4

Format : .mp4
709,1 Mo
1024 x 576 pixels
Moyenne définition - équivalent DVD
Encodage PAL .MP4 H264
5 Mbits/s
Sélection
Voir Selection
Déposer ici pour retirer de la sélection