v2.6.0 (3548)

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.
- Process Algebras and Labelled Transition Systems (LTS).
- Behavioural Properties (non determinism, deadlock, livelock, fairness, starvation, etc.)
- Remarkable equivalences and pre-orders: trace, testing, simulation, bi-simulation.
- Temporal logics (LTL et CTL) and Model Checking, Kripke structure, Buchi Automata, Fix point.
- 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.

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