Spécification et vérification d’un système d’ascenseur par la méthode B
Loading...
Date
2018
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
FACULTE DES MATHEMATIQUES ET DE L’INFORMATIQUE DEPARTEMENT D’INFORMATIQUE
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.
Description
Keywords
Méthode B; développement formel ; vérification formelle ; Atelier B ; Raffinement ; Machine abstraite.