Spécification et vérification d’un système d’ascenseur par la méthode B

Abstract

Notre travail entre dans le cadre de génie logiciel. Cette mémoire s’intéresse à la spécification et vérification formelle des logiciels. Nous avons utilisé les méthodes formelles pour développer un système informatique. Nous avons utilisé en particulier la méthode B et son atelier B pour construire une spécification formelle B d’un système de contrôle d’ascenseur. Ensuite, nous avons effectuée une vérification B de la spécification obtenue du système afin de vérifier certaines propriétés (les obligations de preuve) et pour garantir sa consistance et faciliter la détection et la correction des erreurs avant de générer le code C équivalent.