INE20 : Tests, preuves et validation des logiciels
English version
Ainsi la plupart des fonctions vitales de systèmes comme les avions, les trains, les métros mais aussi les centrales nucléaires, les réacteurs chimiques, les centres de logistiques sont contrôlés par des circuits programmables ou des ordinateurs. Si un dysfonctionnement d'un programme informatique peut-être tolérée dans le cadre d'un ordinateur personnel, ce n'est plus le cas dans des systèmes relativement complexe, soit pour des raisons économiques : un dysfonctionnement dans un système d'encaissement conduit à des pertes d'exploitation de plusieurs millions d'euros par heure de dysfonctionnement, soit pour des raisons de mise en danger de la vie des personnes : un dysfonctionnement dans les commandes d'un avion, d'un train ou d'un réacteur chimique peuvent immédiatement se solder par la mort d'un très grand nombre de personne.
Les systèmes programmables se doivent donc d'être certifiés comme les autres systèmes mécaniques, électriques. Cependant la certification des systèmes programmables pose deux problèmes majeurs :
-. d'une part les modèles mathématiques sous-jacent sont des modèles mathématiques discrets
-. d'autre part le nombre de configurations possibles est exponentiel par rapport à la complexité du programme,
ce qui a pour conséquence de rendre les méthodes classiques de modélisation et simulation inapplicables.
Dans le cadre de ce module, nous vous proposons d'étudier les techniques qui sont en cours d'adoption par l'industrie afin de pouvoir s'assurer du bon fonctionnement d'un programme,
-. le cours "Test et validation formelle des logiciels" s'attache plus à la présentation des techniques d'analyse et de vérification intelligente d'un logiciel par rapport aux spécifications.
-. le cours "Preuve de programme" s'attache plus à la présentation d'un outil de preuve permettant de s'assurer de la "correction logique" du processus implanté.
Cependant, les acquis de ce module seront utiles pour tous les élèves qui auront un projet de prototypage informatique adossé à leur activité principale, notamment dans le cas de simulation.