Cours de modélisation et de vérification

Sujets

• informatique
• ordinateur

Informations

• Publié par: Anjyo
• Nombre de lectures: 48
• Langue: Français

Extrait

Introduction à la modØlisation et à la vØri cation Application aux systŁmes temporisØs Patricia Bouyer LSV – CNRS & ENS de Cachan Cachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 1/85ModØlisation & VØri cation Introduction Cachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 2/85Ü Ü SystŁmes informatiques ordinateurs personnels,serveurs systŁmesembarquØs tØlØphonesmobiles avions fusØes Lego Mindstorms automobiles(X-by-wire) ... Cachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 3/85Ü Ü Ü SystŁmes informatiques ordinateurs personnels,serveurs systŁmesembarquØs tØlØphonesmobiles avions fusØes Lego Mindstorms automobiles(X-by-wire) ... Deux tendances: de plus en plus performants,de plus en plus miniaturisØs de plus en plus complexes Cachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 3/85Ü Ü Ü Ü SystŁmes informatiques ordinateurs personnels,serveurs systŁmesembarquØs tØlØphonesmobiles avions fusØes Lego Mindstorms automobiles(X-by-wire) ... Deux tendances: de plus en plus performants,de plus en plus miniaturisØs de plus en plus complexes Une caractØristique « nouvelle » : systŁmescritiques abilitØ indispensable ! Cachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 3/85þ Ü Quelques bogues cØlŁbres Therac 25, traitement aux rayons X des tumeurs cancØreuses «x Up Edit e Enter » en moins de 8s radiation 125 x la dose normale 6 dØcŁs aux tats-Unis en 1986 erreur logicielle ! Cachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 4/85þ Ü Ü Quelques bogues cØlŁbres Therac 25, traitement aux rayons X des tumeurs cancØreuses «x Up Edit e Enter » en moins de 8s radiation 125 x la dose normale 6 dØcŁs aux tats-Unis en 1986 erreur logicielle ! AT&T un patch non vØri Ø dans le systŁme d’exploitation une erreur dans unswitch (en C) le rØseau tØlØphonique de la c te est des tats-Unis a ØtØ bloquØ pendant 9h ! Cachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 4/85þ Ü Ü Ü Quelques bogues cØlŁbres Therac 25, traitement aux rayons X des tumeurs cancØreuses «x Up Edit e Enter » en moins de 8s radiation 125 x la dose normale 6 dØcŁs aux tats-Unis en 1986 erreur logicielle ! AT&T un patch non vØri Ø dans le systŁme d’exploitation une erreur dans unswitch (en C) le rØseau tØlØphonique de la c te est des tats-Unis a ØtØ bloquØ pendant 9h ! Le bogue pentium une erreur dans la division ottante du processeur heureusement, un chercheur en thØorie des nombres veillait... 470 millions de $ Cachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 4/85Une solution parmi d’autres Le systŁme vØri e-t-il la propriØtØ? ModØlisation Cachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 5/85Une solution parmi d’autres Le systŁme vØri e-t-il la propriØtØ? ModØlisation j= Algorithmede model-checking Cachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 5/85