logo
v2.10.0 (4913)

Enseignement scientifique & technique - SLR204 : Bases de la vérification des systèmes distribués

Domaine > Informatique.

Descriptif

Objectives
 
The aim of this module is to introduce key concepts related to the formal verification of concurrent and distributed systems.
 
Syllabus
 
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

L'objectif de l'UE est d'introduire les concepts de base de la vérification des systèmes répartis et concurrents selon 2 approches pour la vérification: la Logique Temporelle et les Réseaux de Petri.
 

24 heures en présentiel (16 blocs ou créneaux)

Parcours de rattachement

Format des notes

Numérique sur 20

Littérale/grade européen

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

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.

Méthodes pédagogiques

Leçons, TP sur outils
Veuillez patienter