Descriptif
Objectifs pédagogiques
Parcours de rattachement
Format des notes
Numérique sur 20Littérale/grade européenPour les étudiants du diplôme Diplôme d'ingénieur
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
La note obtenue rentre dans le calcul de votre GPA.
Programme détaillé
Programme
Ce module présente les bases de deux approches de vérification: Model Checking et Petri Nets. Les aspects suivants sont abordés:
- Introduction et rôle de la vérification dans le processus de développement.
- Structures de Kripke pour la modélisation des systèmes.
- Logiques temporelles (LTL et CTL) pour exprimer des propriétés vérifiables.
- Vérification du Model Checking: résolution pour propriété LTL via Buchi Automata.
- Vérification du Model Checking: résolution pour propriété CTL via procédure d'étiquetage.
- Réseaux de Petri, modélisation de la concurrence, propriétés de base.
- Vérification des propriétés comportementales et des invariants.