Vérification Formelle Basée Maude Du Code C
Résumé: Ce travail s'inscrit à l'axe de recherche général de la preuve formelle de la conformité d'un programme impératif écrit en C par rapport à sa spécification en se basant sur les capacités offertes par l'environnement Maude qui est un candidat idéal pour la spécification de système. Notre but est la génération automatique d'une spécification Maude à partir du code C. Cette transformation est faite par l'intermédiaire du graphe de flot de contrôle et de données qui est généré automatiquement à partir du code C. Ce dernier sera utilisé ensuite pour générer automatiquement un module système Maude. Plusieurs propriétés orientées contrôle et données peuvent être vérifiées en utilisant les outils offerts par Maude et en particulier le model checker.
Mots-clès:
Nos services universitaires et académiques
Thèses-Algérie vous propose ses divers services d’édition: mise en page, révision, correction, traduction, analyse du plagiat, ainsi que la réalisation des supports graphiques et de présentation (Slideshows).
Obtenez dès à présent et en toute facilité votre devis gratuit et une estimation de la durée de réalisation et bénéficiez d'une qualité de travail irréprochable et d'un temps de livraison imbattable!
Aucun fichier associé
Si le fichier est volumineux, l'affichage peut échouer. Vous pouvez obtenir le fichier directement en cliquant sur le bouton "Télécharger".
