Introduction à la modØlisation et à lavØri cationApplication aux systŁmes temporisØsPatricia BouyerLSV – CNRS & ENS de CachanCachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 1/85ModØlisation & VØri cationIntroductionCachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 2/85ÜÜSystŁmes informatiquesordinateurs personnels,serveurssystŁmesembarquØstØlØphonesmobilesavionsfusØesLego Mindstormsautomobiles(X-by-wire)...Cachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 3/85ÜÜÜSystŁmes informatiquesordinateurs personnels,serveurssystŁmesembarquØstØlØphonesmobilesavionsfusØesLego Mindstormsautomobiles(X-by-wire)...Deux tendances: de plus en plus performants,de plus en plus miniaturisØsde plus en plus complexesCachan, le 17 septembre 2003 Introduction à la modØlisation et à la vØri cation – p. 3/85ÜÜÜÜSystŁmes informatiquesordinateurs personnels,serveurssystŁmesembarquØstØlØphonesmobilesavionsfusØesLego Mindstormsautomobiles(X-by-wire)...Deux tendances: de plus en plus performants,de plus en plus miniaturisØsde plus en plus complexesUne 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ŁbresTherac 25, traitement aux rayons X des tumeurs cancØreuses«x Up Edit e Enter » en moins de 8s radiation 125 ...
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/85ModØ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/85Une 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/85Une 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