Le projet MALG reprend les notions enseignées dans le cours MALG. L’idée est d’analyser des programems écrits en C et d’en déduire des propriétés validées à l’aide de la plateforme toolbox TLA et de l’outil Framac. Chaque groupe prendra trois programmes et les analysera selon deux méthodes, en visant la correction partielle et l’absence d’erreurs à l’exécution : — avec la méthode de traduction des algorithmes en PlusCal et la plateforme Toolbox TLAPS — avec l’outil Framac Chaque groupe aura trois algorithmes spécifiques. Il les traduira en un algorithme PlusCal équivalent, vérifiera la correction partielle et l’absence d’erreurs à l’exécution. Il se peut que vous trouviez une optimisation à parrtir de votre analyse et dans ce cas, vous indiquerez comment la méthode vous a permis de le faire. Le rapport à rendre devra expliquer clairement les opérations réalisées. Ce rapport sera synthétique et mettra en avant les difficultés rencontrées et donnera des possibilités d’extension de cet outil. Le dossier final sera une archive contenant les différents éléments concernant la vérification avec chaque outil et le rapport final en pdf. La date de remise des dossiers est le 9 mai 2017 et chaque groupe présentera son travail dans les jours suivants. Un dossier est une archive dont le nom est de la forme nom1-nom2-nom3- nom4-projet.zip (utilisez zip pour compresser). Le sujet du message sera tpmalg. Un groupe est constitué de 4 personnes et vous êtes 52. Il y aura donc 13 groupes. Le fichier excel groupmalg donne la liste des élèves ; les délégués renverront la liste des groupes avec un numéro entre 1 et 13. Cette liste sera renvoyée à Dominique Méry dès que possible.
- Traduire les 3 codes en algo PlusCal
- Ajouter les asserts dans le code C sur Frama-C
- Verifier la correction partielle
- Verifier absence d'erreurs à l'exécution
- Si possible et si motivé, optimisez le code (FACULTATIF)
- Ecrire le rapport avec (Opérations réalisées / Difficultés / Possibilité d'extension des 2 outils)
- Envoyé par mail avant le 9 mai un dossier au nom chone-hell-jamet-raoux-projet.zip contenant
- Code + traduction + vérification
- Rapport