La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Partagez cette publication

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
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin