| Ce memoire par article decrit la comparaison de deux verificateurs de modeles pour EB3. L'integration d'un verificateur de modeles a la plateforme APIS permet de verifier que les specifications des systemes d'information ecrites en EB3 verifient certaines proprietes. Ainsi, nous pourrons affirmer que les systemes d'information generes avec la methode Apis sont valides, c'est-a-dire conformes au cahier des charges formule par le client. Cette etape de validation est importante dans tout projet car elle indique si le concepteur a atteint ses objectifs.;Ce memoire compare deux verificateurs de modeles, SPIN et CADP, dans le cadre de la verification de specifications EB3. Pour illustrer ce travail, nous avons modelise un systeme d'information de bibliotheque dans leurs langages respectifs, PROMELA et LOTOS-NT. Les processus de verification ont ete appliques a ces specifications afin de comparer les deux verificateurs de modeles. Notre objectif ultime est de convertir automatiquement les specifications EB3 en langage du verificateur de modeles choisi pour reduire au minimum l'intervention humaine durant le processus de verification.;Une analyse du probleme conduit a traduire les specifications EB3 dans un langage accepte par un verificateur de modeles. Il convient donc de faire le choix d'un verificateur de modeles adapte aux specifications de systemes d'information ecrites en EB3. |
