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
Objectives
At the end of the course the student will be able to:
- model, specify, and verify problems of different kinds using the above mentioned theoretical methods;
- explain and analyze the theoretical methods used in the context of formal verification;
- apply in a formal way the studied algorithms to the different verification problems;
- explain in a reasoned way the approaches used to solve a verification problem.
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 M2 PDS - Parallel and Distributed Systems
L'UE est acquise si Note finale >= 10- Crédits ECTS acquis : 2.5 ECTS
Pour les étudiants du diplôme M1 PDS - Parallel and Distributed Systems
L'UE est acquise si Note finale >= 10- Crédits ECTS acquis : 2.5 ECTS
Pour 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
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é
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.