Objectif

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
  • Vidéoconférence

Pour confirmer le ou les modes d’enseignement disponibles pour une session donnée, veuillez vous référer à l’horaire du cours ci-bas.

Formules pédagogiques

Enseignement magistral

Horaire

Consulter l'horaire de ce cours