v2.11.0 (5776)

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

Domaine > Informatique.

Descriptif

Course content

The aim of this module is to introduce key concepts related to the formal verification of concurrent and distributed systems.

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

Objectives

At the end of the course the student will be able to:

- model, specify, and verify problems of different kinds using the above mentioned theoretical methods;

- explain and analyze the theoretical methods used in the context of formal verification;

- apply in a formal way the studied algorithms to the different verification problems;

- explain in a reasoned way the approaches used to solve a verification problem.

 

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 M2 PDS - Parallel and Distributed Systems

L'UE est acquise si Note finale >= 10
  • Crédits ECTS acquis : 2.5 ECTS

Pour les étudiants du diplôme M1 PDS - Parallel and Distributed Systems

L'UE est acquise si Note finale >= 10
  • Crédits ECTS acquis : 2.5 ECTS

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

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.

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