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

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) 

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.

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

Chargement du résultat...
Patientez
Intitulé de la formation
Type
Modalité(s)
Lieu(x)
Lieu(x) À la carte
Lieu(x) Paris
Intitulé de la formation Master Réseaux et Objets Connectés
Lieu(x) À la carte
Lieu(x) À la carte
Lieu(x) Paris
Lieu(x)
Lieu(x)
Lieu(x) Alternance
Lieu(x) Occitanie
Lieu(x) À la carte
Lieu(x) Alternance
Lieu(x) Occitanie
Lieu(x) Package
Lieu(x) Grand-Est
Lieu(x) À la carte
Intitulé de la formation Type Modalité(s) Lieu(x)

Contact

EPN05 - Informatique
2 rue Conté
75003 Paris
Tel :01 40 27 22 58
Swathi Rajaselvam

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.

UE

    • Paris
      • Centre Cnam Paris
        • 2022-2023 2nd semestre : FOAD 100%
        Comment est organisée cette formation ?

        Organisation de la modalité FOAD 100%

        Planning

        Aucun planning pour le moment

        Précision sur la modalité pédagogique

        • Regroupements physiques facultatifs : Aucun

        Organisation du déploiement de l'unité

        • Nombre d'élèves maximum à distance par classe : 40
        • Nombre d'heures d'enseignement par élève : 40
        • Délai maximum de réponse à une solicitation : sous 96 heures (Jours ouvrés)

        Modes d'animation de la formation

        • Forum
        • Messagerie intégrée à la plateforme
        • Visioconférence
        • Outils numériques de travail collaboratif
        • Organisation d'une séance de démarrage
        • Evaluation de la satisfaction
        • Hot line technique

        Ressources mises à disposition sur l'Espace Numérique de Formation

        • Documents de cours
        • Enregistrement de cours
        • Documents d'exercices, études de cas ou autres activités pédagogiques
        • Outils spécifiques (exerciseur, simulateurs, etc)
        • Bibliographie et Webographie

        Activités "jalons" de progression pédagogique prévues sans notation obligatoire à rendre ou en auto-évaluation

        • 1 exercice
        • 1 étude de cas, projet collectif
        • 1 étude de cas, projet individuel

        Modalité de contrôle de l'acquisition des compétences et des connaissances (validation de l'UE)

        • Examens en ligne
        • Projet(s) individuel(s)
        • Projet(s) collectif(s)
        :