Projet

TD

• Td 1 - Modelisation ps
• Td 2 - Verification a la main, apercu de Spin, Modelisation ps
• Tp 3 - Spin - Prise de contact ps et quelques corriges ACM,ACM 2
• Td 4 - LTL + Automates ps
• absent
• Td 5 - LTL + Automates ps - ennonce + corrige
• Journee INT
• Tp 6 - SMV - Prise de contact ps
• Tp 7 - SMV (2) ps et quelques corriges assign, trans Attention aux erreurs suivantes, rencontrees lors du TP : nb-1 -> nb - 1 (avec des espaces), la couverture des cas envisages dans case, le passage des parametres en arguments des modules ...
• Td 8 - LTL vers Automates ps - ennonce + corrige
• Td/Tp 9 - Model checking de CTL ennonce, ennonce corrige
• Tp 10 - Mise en route du projet
• TP 11 - Modelisation de Needham Schroeder ennonce correction
• TD 12 - Les Bdds ennonce corrige
• TD 13 - Model Checking Symbolique - Automates Temporises - Dernier TD, avec demo de UPPAAL si on a le temps -> en salle machine, a 10h30 ennonce corrige partiel

Manuels