Spécification et vérification des systèmes distribués
Code UE : NFP103
- Cours + travaux pratiques
- 6 crédits
- Volume horaire de référence
(+ ou - 10%) : 50 heures
Responsable(s)
Kamel BARKAOUI
Public, conditions d’accès et prérequis
Avoir le niveau licence informatique (L3).
Public concerné : Élèves ingénieurs, étudiants en master
Public concerné : Élèves ingénieurs, étudiants en master
Objectifs pédagogiques
De par le développement des technologies Web, des langages de programmation concurrente, des outils de programmation réseau et celui des processeurs multi-cœurs, le calcul concurrent est aujourd'hui omniprésent dans la construction de systèmes comme les systèmes d'exploitation, les systèmes distribués et les systèmes temps réel. Cependant, la conception de tels systèmes et la preuve de leur correction sont des tâches très difficiles.
Ce cours a pour objectif :
- d'acquérir une connaissance pratique des "bons" patrons de la programmation concurrente (Java)
- de comprendre les problèmes fondamentaux des systèmes concurrents
- et de s'initier à des méthodes et techniques de vérification automatique de ces systèmes (model-checking, logiques temporelles)
Ce cours a pour objectif :
- d'acquérir une connaissance pratique des "bons" patrons de la programmation concurrente (Java)
- de comprendre les problèmes fondamentaux des systèmes concurrents
- et de s'initier à des méthodes et techniques de vérification automatique de ces systèmes (model-checking, logiques temporelles)
Compétences visées
conception, programmation et validation d'applications concurrents fiables
Contenu
Structuration des applications concurrentes
Contrôle de concurrence dans les systèmes transactionnels, les systèmes d'information répartis, les applications temps réel.
Les paradigmes de la concurrence et les archétypes de programmation ('design patterns').
Exclusion mutuelle, élection, producteur consommateur, lecteurs rédacteurs, client-serveur, "peer to peer", problèmes liés aux pannes, diffusion atomique ordonnée, inter-blocage, famine, équité, terminaison.
Mécanismes de bases (processus, sémaphores, moniteurs, la classe "thread" et les méthodes "synchronized" dans Java, tâches et objets protégés dans ADA95, communication synchrone et asynchrone, messages, boîtes aux lettres, invocation à distance, rendez-vous). Modularité et objets concurrents.
Spécification et vérification de propriétés de systèmes concurrents
Aperçu des méthodes de spécification : automates, automates synchronisés, réseaux de Petri, structures de Kripke, logiques temporelles.
Techniques d'analyse : analyse structurelle (réseaux de Petri), model-checking (Logique temporelle). Utilisation d' outils (open source) de simulation et de vérification : Spin, Design/CPN.
Contrôle de concurrence dans les systèmes transactionnels, les systèmes d'information répartis, les applications temps réel.
Les paradigmes de la concurrence et les archétypes de programmation ('design patterns').
Exclusion mutuelle, élection, producteur consommateur, lecteurs rédacteurs, client-serveur, "peer to peer", problèmes liés aux pannes, diffusion atomique ordonnée, inter-blocage, famine, équité, terminaison.
Mécanismes de bases (processus, sémaphores, moniteurs, la classe "thread" et les méthodes "synchronized" dans Java, tâches et objets protégés dans ADA95, communication synchrone et asynchrone, messages, boîtes aux lettres, invocation à distance, rendez-vous). Modularité et objets concurrents.
Spécification et vérification de propriétés de systèmes concurrents
Aperçu des méthodes de spécification : automates, automates synchronisés, réseaux de Petri, structures de Kripke, logiques temporelles.
Techniques d'analyse : analyse structurelle (réseaux de Petri), model-checking (Logique temporelle). Utilisation d' outils (open source) de simulation et de vérification : Spin, Design/CPN.
Modalité d'évaluation
- Contrôle continu
- Projet(s)
Bibliographie
- M. Ben-Ari : Principles of Concurrent and Distributed Programming , Addison-Wesley, 2006.
- Brian Goetz : Programmation concurrente en Java. Éditions Pearson Education , Collection Référence, 2009
- S. Haddad & al : Ed Lavosier 2006
Cette UE apparaît dans les diplômes et certificats suivants
Rechercher une formation
RECHERCHE MULTI-CRITERES
-
Vous pouvez sélectionner des formations grâce à un mot ou à une expression présent dans l’intitulé ou dans les index (discipline ou métier visé).
Des index vous sont suggérés à partir du 3e caractère saisi, mais vous pouvez aussi saisir librement tout autre mot . - Les différents items sélectionnés sont croisés.
ex: "Comptabilité" et "Région Grand Est" - Validez par le bouton « Rechercher » ou par la touche Entrée.
- Cette recherche affiche aussi les fiches UE et certificats régionales. Leurs codes les distinguent des fiches nationales par le suffixe de la région (ex : « -IDF » ).
Par défaut, les fiches régionales reprennent le contenu de la fiche nationale correspondante. Mais dans certains cas, des informations régionales ont pu être ajoutées. - Certains diplômes se déclinent selon plusieurs parcours. Pour afficher tous les parcours, tapez la racine du code (ex : « LG035 »).
- Certains stages ont un double code : leur code propre et le code de l’UE ou du certificat équivalent.
- Dans tous les cas, veillez à ne pas insérer d'espace ni de ponctuation supplémentaire.
- Validez par le bouton « OK » (et non pas par la touche Entrée).
Chargement du résultat...
Contact
Voir le calendrier, le tarif, les conditions d'accessibilité et les modalités d'inscription dans le(s) centre(s) d'enseignement qui propose(nt) cette formation.
Enseignement non encore programmé
Code UE : NFP103
- Cours + travaux pratiques
- 6 crédits
- Volume horaire de référence
(+ ou - 10%) : 50 heures
Responsable(s)
Kamel BARKAOUI