Contenu
Méthodes de spécification formelle: automates, expressions régulières, logiques classiques et temporelles, notation B, Z et CCS. Génération automatique de tests, notions de couverture, exécution symbolique dynamique. Le monitoring et l'analyse de traces: exemples, algorithme. Outils de monitoring: Java-MOP, BeepBeep. Le modèle checking et la vérification statique: exemples, algorithmes. Méthodes de réduction de l'espace d'état, abstraction et raffinement. Outils de vérification: Concurrency Workbench, Java Pathfinder, SPIN et NuSMV.
Mode(s) de prestation
Présence
Présence de la professeure ou du professeur, de la personne chargée de cours ou de l’équipe pédagogique et des personnes étudiantes à un moment commun dans un lieu de formation déterminé (ex. : salle de classe physique, laboratoire, sortie sur le terrain).
Vidéoconférence
Cours offert simultanément par vidéoconférence à partir d’un site d’enseignement origine, où l’enseignement se fait en présence, sur un ou des sites (lieux de formation) distants identifiés par l’UQAR, selon les procédures et règlements en vigueur. Le cours est suivi de façon simultanée par tous.