Évaluation d'outils de vérification pour les spécifications de systèmes d'information

Abstract

Ce mémoire par article décrit la comparaison de deux vérificateurs de modèles pour EB3 . L'intégration d'un vérificateur de modèles à la plateforme APIS permet de vérifier que les spécifications des systèmes d'information écrites en EB3 vérifient certaines propriétés. Ainsi, nous pourrons affirmer que les systèmes d'information générés avec la méthode Apis sont valides, c'est-à-dire conformes au cahier des charges formulé par le client. Cette étape de validation est importante dans tout projet car elle indique si le concepteur a atteint ses objectifs. Une analyse du problème conduit à traduire les spécifications EB3 dans un langage accepté par un vérificateur de modèles. Il convient donc de faire le choix d'un vérificateur de modèles adapté aux spécifications de systèmes d'information écrites en EB3.Ce mémoire compare deux vérificateurs de modèles, SPIN et CADP, dans le cadre de la vérification de spécifications EB3 . Pour illustrer ce travail, nous avons modélisé un système d'information de bibliothèque dans leurs langages respectifs, PROMELA et LOTOS-NT. Les processus de vérification ont été appliqués à ces spécifications afin de comparer les deux vérificateurs de modèles. Notre objectif ultime est de convertir automatiquement les spécifications EB3 en langage du vérificateur de modèles choisi pour réduire au minimum l'intervention humaine durant le processus de vérification.