Descriptif
L'objectif de ce module est d'introduire les concepts clés liés à la vérification formelle des systèmes logiciels et matériels.
Ce module présente la vérification des systèmes monolithiques et multi-agents. Les aspects suivants sont abordés :
- Introduction et rôle de la vérification dans le processus de développement.
- Modélisation des systèmes monolithiques et multi-agents.
- Logiques temporelles et stratégiques pour exprimer des propriétés vérifiables.
- Vérification par Model Checking.
Objectifs pédagogiques
À la fin du cours, l'étudiant sera capable de :
- modéliser, spécifier et vérifier des problèmes de différentes natures en utilisant les méthodes théoriques mentionnées dans le descriptif ;
- expliquer et analyser les méthodes théoriques utilisées dans le contexte de la vérification formelle ;
- appliquer de manière formelle les algorithmes étudiés aux différents problèmes de vérification ;
- expliquer de manière raisonnée les approches utilisées pour résoudre un problème de vérification.
Diplôme(s) concerné(s)
Parcours de rattachement
Format des notes
Numérique sur 20Littérale/grade européenPour les étudiants du diplôme Diplôme d'ingénieur
Vos modalités d'acquisition :
Examen écrit
L'UE est acquise si Note finale >= 10- Crédits ECTS acquis : 2.5 ECTS
- Crédit d'UE électives acquis : 2.5
La note obtenue rentre dans le calcul de votre GPA.
Pour les étudiants du diplôme Echange international non diplomant
Vos modalités d'acquisition :
Examen écrit
L'UE est acquise si Note finale >= 10- Crédits ECTS acquis : 2.5 ECTS
La note obtenue rentre dans le calcul de votre GPA.
Programme détaillé
Mots clés
Méthodes formelles, model checking, systèmes multi-agents, logiques modales, logiques temporelles, logiques stratégiques, théorie des automates, théorie des jeuxSupport pédagogique multimédia
