Techniques de vérification et de validation
- Enseignant: Michael Blondin
- Plan de cours:
- Horaire:
– mardi: 13h30 à 15h20 au D3-2029
– mercredi: 15h30 à 16h20 au D3-2029
- Examen final: mercredi 24 avril de 09h00 à 12h00 au local D3-2029
- Disponibilité sans rendez-vous: jeudi de 14h30 à 15h30
- Consultation de l'examen final: vendredi 26 avril de 9h30 à 14h00
- Rétroaction de mi-session
Calendrier
Matériel
Références
- Notes de cours: toute la matière de la session
- Autres références externes:
- Systèmes à pile
- Diagrammes de décision binaire
- Vérification de protocoles de population
- Protocole de
Needham-Schroeder: explications
et code Promela
(Vous pouvez lire les sections 1 et 2 du PDF; les autres sections couvrent la majeure partie du cours!)
- Manuel principal:
- Christel Baier, Joost-Pieter Katoen: Principles of Model Checking. MIT Press, 2008.
- Errata du manuel:
- Exemples faits en classe: Ex. 5.4 (sem. 2, p. 234), Ex. 6.3 et 6.7 (sem. 6), Ex. 6.26 (sem. 7, p. 349)
Outils
- Solveurs logiques: Z3 (démo en ligne), Z3, CVC4
- LoLA peut être téléchargé à partir d'ici . Système modélisé en classe:
- NuSMV peut être téléchargé à partir d'ici . Systèmes modélisés en classe:
- Spin peut être téléchargé à partir d'ici . L'interface graphique utilisée en classe est iSpin; elle également disponible sur ce site Web. Il existe une autre interface nommée jSpin. Vous pouvez alternativement utiliser l'interface Web développée à Chalmers University of Technology.
Introduction
- Diaporama:
- Code Promela des trois exemples des diapositives: