v2.3.2 (2689)

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

Domaine > Informatique.

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 3 approches pour la vérification : les Algèbres de Processus, la Logique Temporelle et les Réseaux de Petri.

nombre d'heure en présentiel

24

nombre de blocs

16

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 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é

Contenu

Seront traités, notamment, les aspects suivants :

- Introduction et rôle de la vérification dans le processus de développement, modélisation de comportement, modélisation des propriétés fiables, sémantique formelle.

- vérification par exploration des états, vérification par preuve.

- Propriétés remarquables : non déterminisme, blocage, livelock, équité, famine, etc.

- Approche basées Algèbres des processus pour la description des comportements. Systèmes de transitions étiquetés.

- Équivalences entre comportements : comportements  traces-équivalents, test équivalents,  similaires, bi-similaires.

- Logiques temporelles (LTL et CTL) pour l'expression de propriétés vérifiables,  structure de kripke pour l'expression des comportements, vérification par Model Checking, automate de Buchi, point fixe.

- Réseaux de Petri, modélisation de la concurrence, de la synchronisation, du conflit.

- Vérification de propriétés comportementales, invariants.

Méthodes pédagogiques

Leçons, TP sur outils
Veuillez patienter