Descriptif
Course content
The aim of this module is to introduce key concepts related to the formal verification of concurrent and distributed systems.
This module presents the basis of two approaches for verification: Model Checking and Petri Nets. The following aspects are addressed:
- Introduction and role of verification in the development process.
- Kripke structures for modeling systems.
- Temporal logics (LTL and CTL) for expressing verifiable properties.
- Model Checking verification: solving LTL model checking via Buchi Automata.
- Model Checking verification: solving CTL model checking via Labeling procedure.
- Petri Nets, modeling of concurrency, basic properties.
- Verification of behavioral properties and invariants.
Objectifs pédagogiques
Acquis d'apprentissageÀ l'issue de l'UE, l'élève sera capable de:
- Modéliser, spécifier et vérifier des problèmes de différents types en utilisant les méthodes formelles
- 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
Compétences de rattachement (et justification)
- BC8.4 – Déterminer les phases et procédures de tests techniques et fonctionnels des composants matériels et logiciels pour assurer la fiabilité, la sécurité et/ou la sûreté de fonctionnement des systèmes; Justification : La vérification formelle a pour objectif principal de garantir la fiabilité, la sécurité et/ou la sûreté de fonctionnement des systèmes. Ainsi, acquérir cette technique donne aux étudiants les bases pour garantir la correction des systèmes.
- BC10.3 – Analyser une résolution par des approches formelles ou mathématiques; Justification : À la base du model checking, des méthodes formelles sont utilisées. Acquérir ces méthodologies garantit l'acquisition de cette compétence.
Diplôme(s) concerné(s)
Parcours de rattachement
Pour les étudiants du diplôme Diplôme d'ingénieur
aucun
Format des notes
Numérique sur 20Littérale/grade européenPour les étudiants du diplôme Echange international non diplomant
Vos modalités d'acquisition :
Un 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.
Pour les étudiants du diplôme Diplôme d'ingénieur
Vos modalités d'acquisition :
Un 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 M1 PDS - Parallel and Distributed Systems
Vos modalités d'acquisition :
Un examen écrit.
L'UE est acquise si Note finale >= 10- Crédits ECTS acquis : 2.5 ECTS
Pour les étudiants du diplôme M2 PDS - Parallel and Distributed Systems
Vos modalités d'acquisition :
Un examen écrit.
L'UE est acquise si Note finale >= 10- Crédits ECTS acquis : 2.5 ECTS
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.
Méthodes pédagogiques
Les concepts clés sont présentés en cours magistral et mis en application en TD.Ressources : diapositives du cours