Browsing by Author "BOUKHALAT, Youssef"

Now showing 1 - 2 of 2
  • No Thumbnail Available
    ItemOpen Access
    Un Translateur C vers Promela pour la Vérification formelle des programmes C avec Spin Model-checker
    (FACULTE DES MATHEMATIQUES ET DE L’INFORMATIQUE- UNIVERSITE DE M’SILA, 2012) BOUKHALAT, Youssef
    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.
  • Thumbnail Image
    ItemOpen Access
    Un Translateur C vers Promela pour la Vérification formelle des programmes C avec Spin Model-checker
    (University of M'sila, 2012-06-10) BOUKHALAT, Youssef; Rapporteur: BOUHOUITA GUERMECH, Salah Eddine
    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.