v2.6.0 (3585)

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 software.

Syllabus - The following aspects are addressed:
- Introduction, role of verification in the development process. Modelling of behaviour and formal semantics.
- Temporal logics (LTL et CTL) and Model Checking, Kripke structure, Buchi Automata, Fix point.
- Behavioural Properties (non determinism, deadlock, livelock, fairness, starvation, etc.)
- Petri Nets, modelling of concurrency, synchronisation, conflict. Finiteness. Linear 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)

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 Echange international non diplomant

La note obtenue rentre dans le calcul de votre GPA.

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.

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.

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

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

- 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