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


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) 

Public et conditions d'accès :

Avoir le niveau licence informatique (L3).
Public concerné : Élèves ingénieurs, étudiants en master

Compétences :

conception, programmation et validation d'applications concurrents fiables

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.

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: Méthodes formelles pour les systèmes répartis et coopératifs (Traité IC2, série informatique et systèmes d' information); Ed Lavosier 2006

Cette UE apparaît dans les diplômes et certificats suivants :

  • MR11603A : Master Sciences, technologies, santé mention Informatique parcours Systèmes d'information et business intelligence
  • CYC9101A : Diplôme d'ingénieur Spécialité informatique parcours Architecture et ingénierie des systèmes et des logiciels (AISL)
  • CYC9102A : Diplôme d'ingénieur Spécialité informatique parcours Informatique modélisation optimisation
  • MR11606A : Master Sciences, technologies, santé mention Informatique parcours Réseaux et objets connectés
  • MR11607A : Master Sciences, technologies, santé mention Informatique parcours Sécurité informatique, cybersécurité et cybermenaces En bretagne
  • MR11602A : Master Sciences, technologies, santé mention Informatique parcours Recherche opérationnelle
  • MR11603B : Master Sciences, technologies, santé mention Informatique parcours Systèmes d'information et business intelligence HTT
  • MR11605A : Master Sciences, technologies, santé mention Informatique parcours Préparation à l'agrégation en informatique
  • MR11604A : Master Sciences, technologies, santé mention Informatique parcours Traitement de l'information et exploitation des données

Prochaines sessions de formation

Filtres :
Centre de formation Semestre
2023/2024
Jours de
formation
Modalité Crédits    
Paris Semestre 2 6 crédits (1)

Date de début des cours (*) :

  • 05/02/2024

* Les dates fournies sont d'ordre général à toutes les formations.
  Les cours pour cette formation peuvent potentiellement commencer un peu plus tard dans le semestre.

Ajouter au panier
Contacter le centre
Légende :
Tarif (1) :

Vous pouvez consulter nos tarifs ici.
Selon votre statut, il existe différents dispositifs de financement qui peuvent financer jusqu'à 100 % de votre formation. Nos chargés de formation en centre vous accompagneront pour constituer votre dossier.

Date de début de cours :
  • Île-de-France :
    • 1er semestre et annuel : 02/10/2023
    • 2e semestre : 19/02/2024
  • Paris :
    • 1er semestre et annuel : 18/09/2023
    • 2e semestre : 05/02/2024

Les dates fournies sont d'ordre général à toutes les formations. Les cours pour cette formation peuvent potentiellement commencer un peu plus tard dans le semestre.

Annuel :

Il s'étend de fin septembre / début octobre à début juillet (dates indicatives, renseignez-vous auprès de votre centre).

Semestre 1 :

Il s'étend de fin septembre / début octobre à fin janvier / début février (dates indicatives, renseignez-vous auprès de votre centre).

Semestre 2 :

Il s'étend de fin février / début mars à début juillet (dates indicatives, renseignez-vous auprès de votre centre).

Cours du soir :

Les cours commencent le plus souvent à 18h30 dans les centres.

  Cours en journée :

Se renseigner auprès du centre pour connaître les horaires.

Cours en ligne :

les cours sont diffusés sous forme de séances numériques via une plateforme d’e-learning animées et tutorées par un enseignant. Des séances de regroupement en visio sont proposées.

  Classe virtuelle :

L'enseignant à distance intervient en direct et en visioconférence sur la plateforme d'e-learning. Il complète son intervention par des activités interactives (exercices échanges…)

  Cours en ligne hybride :

Cette modalité associe des cours en ligne tutorées et des regroupements en présentiel obligatoires.

  Cours hybrides :

Cette modalité mixe des cours en présentiel (en cours du soir ou en journée) et des cours en ligne.

  Cours en ligne organisés par un autre
centre CNAM Régional :

Les cours sont diffusés sous forme de séances numériques via une plateforme d'e-learning animées et tutorées par un enseignant.

Recherche en cours