Vous êtes ici :

  • Informatique / Bureautique / Big data / Cybersécurité

Spécification et vérification des systèmes distribués

Spécification et vérification des systèmes distribués
Unité d'enseignement

Accéder aux sections de la fiche

Call to actions

Nous contacter
Choisir mon semestre

Détails

Infos générales

Code
NFP103

Présentation

Objectifs

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) 

Intitulé officiel

Spécification et vérification des systèmes distribués
Masquer les détails supplémentaires

Conditions d'accès

Pré-requis

Formation(s) requise(s)

Aucun prérequis.

Programme

Contenu de la formation

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.

Unités d'enseignement

  • Spécification et vérification des systèmes distribués
    À distance / Partiellement à distance Février à Juin 50 heures 6 crédits

Organisation

Durée et organisation

L'année est organisée en 2 semestres : semestre 1 (S1) d'octobre à février/mars et semestre 2 (S2) de février/mars à juin.
 

Méthodes mobilisées

Pédagogie qui combine apports académiques, études de cas basées sur des pratiques professionnelles et expérience des élèves.
Équipe pédagogique constituée pour partie de professionnels. Un espace numérique de formation (ENF) est utilisé tout au long du cursus.
 

Modalités d'évaluation

Chaque unité (UE/US, UA) fait l'objet d'une évaluation organisée en accord avec l'Établissement public (certificateur) dans le cadre d'un règlement national des examens.
 

Accessibilité public en situation de handicap

Nos formations sont accessibles aux publics en situation de handicap. Un référent Cnam est dédié à l'accompagnement de toute personne en situation de handicap. Pour contacter le référent : handi@cnam-paysdelaloire.fr

Modalités d'inscription

Consultez nos tarifs

Comment s'inscrire ?

Choisissez votre semestre et cliquez sur "Ajouter à ma sélection".
 

Modalités et délais d'accès

Les inscriptions se déroulent dès le mois de mai pour les formations qui débutent en octobre (semestre 1) et dès novembre pour les formations qui débutent en février/mars (semestre 2).

Ces formations peuvent aussi vous intéresser

  • Introduction à la gestion de données à large échelle

    Unité d'enseignement
    Découvrir

  • Maîtrise d'architectures de systèmes informatiques

    Bloc de compétences
    Découvrir