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
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 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 Parallel & Distributed Systems
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.
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.