Cours de modélisation et de vérification

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 ...