Validation de specifications de systemes d'information avec ALLOY

Le present memoire propose une investigation approfondie de l'analyseur ALLOY afin de juger son adaptabilite en tant que verificateur de modeles. Dans un premier temps, l'etude dresse un tableau comparatif de six verificateurs de modeles, incluant A LLOY, afin de determiner lequel d'entre eux est le plus apte a resoudre les problematiques de securite fonctionnelle posees par les systemes d'information. En conclusion de cette premiere phase, ALLOY emerge comme l'un des analyseurs les plus performants pour verifier les modeles sur lesquels se fondent les systemes d'information. Dans un second temps, et sur la base des problematiques rencontrees au cours de cette premiere phase, l'etude rapporte une serie d'idiomes pour, d'une part, presenter une maniere optimisee de specifier des traces et, d'autre part, trouver des recours afin de contourner les limitations imposees par ALLOY. A ces fins, le memoire propose deux nouveaux cas d'espece, ceux d'une cuisiniere intelligente et d'une boite noire, afin de determiner si oui ou non l'analyseur est capable de gerer les systemes dynamiques possedant de nombreuses entites avec autant d'efficacite que les systemes qui en possedent moins. En conclusion, le memoire rapporte que ALLOY est un bon outil pour verifier des systemes dynamiques mais que sa version recente, DYN ALLOY, peut etre encore mieux adapte pour le faire puisque precisement concu pour faire face aux specificites de ce type de systeme. Le memoire s'acheve sur une presentation sommaire de ce dernier outil.;Mots-cles: ALLOY; boite noire; idiome de specification; logique dynamique; logique du premier ordre; securite; solutionneurs de satisfiabilite; specification formelle; sftrete; verification de modeles.