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
Acquis d'apprentissage À l'issue de l'UE, l'élève sera capable de: \- Modéliser, spécifier et vérifier des problèmes de différents types en utilisant les méthodes formelles \- Expliquer et analyser les méthodes théoriques utilisées dans le contexte de la vérification formelle \- Appliquer de manière formelle les algorithmes étudiés aux différents problèmes de vérification \- Expliquer de manière raisonnée les approches utilisées pour résoudre un problème de vérification Compétences de rattachement (et justification) \- BC8.4 – Déterminer les phases et procédures de tests techniques et fonctionnels des composants matériels et logiciels pour assurer la fiabilité, la sécurité et/ou la sûreté de fonctionnement des systèmes; Justification : La vérification formelle a pour objectif principal de garantir la fiabilité, la sécurité et/ou la sûreté de fonctionnement des systèmes. Ainsi, acquérir cette technique donne aux étudiants les bases pour garantir la correction des systèmes. \- BC10.3 – Analyser une résolution par des approches formelles ou mathématiques; Justification : À la base du model checking, des méthodes formelles sont utilisées. Acquérir ces méthodologies garantit l'acquisition de cette compétence.
24 heures en présentiel
40 heures de travail personnel estimé pour l’étudiant.
