Un Translateur C Vers Promela Pour La Vérification Formelle Des Programmes C Avec Spin Model-checker

Résumé: La transformation d'une spécification du langage vers un langage pris en charge par un outil de vérification est un moyen largement adopté en vérification formelle. Il permet la réutilisation des langages et des outils existants. Le Model-checker est une approche pour la vérification formelle. Il est utilisé dans la phase de conception d'un système. Dans model-checking un modèle est construit à partir d'une conception existante et ce modèle est ensuite utilisé pour vérifier la conception. Spin model-checker est un vérificateur de modèle. Le modèle que Spin vérifié est écrit dans Promela. Aujourd'hui, le coût des erreurs de programme est en augmentation de jour en jour, ce qui fait que la fiabilité du logiciel devient un problème Critique pour le monde entier. C est un langage de programmation largement utilisé pour développer tous types de logiciels. Par conséquent, la sécurité des logiciels écrits en C représente la proportion importante de la fiabilité des logiciels. Ce mémoire décrit une méthode médiate de model checking codes C pour trouver les problèmes potentiels à l'aide de Spin. Le traducteur que nous avons développé utilise une technique inspiré par la technique de traduction dirigée par la syntaxe pour faire la traduction de C à Promela. C # a été le langage utilisé pour l'implémentation.

Publié dans la revue: