0972 311 312 
(prix appel local)

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

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...En lire plus

Compétences

conception, programmation et validation d'applications concurrents fiables

Légende :

  Formation ouverte et à distance (FOAD)

Condition d'accès / publics visés

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

Niveau

Niveau 6 (Bac+3 et Bac+4)

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.

Modalités de validation

Contrôle continu, Projet(s)

Accompagnement et suivi

Sous l’autorité pédagogique du certificateur Cnam, les équipes du Cnam Bretagne vous offrent un accompagnement pendant votre parcours de formation à la fois sur les aspects administratifs, financiers, pédagogiques et techniques.

ECTS : 6

Modalité Volume horaire Employeur France travail Auto-financement
 
45 heures 900 € 260 € 260 €

Indexation officielle

FORMACODES

[Z5] logiciels/outils/applications/services

Mots clés

Informatique - Réseaux informatiques, Sémantique des programmes, Applications réparties

Indicateurs de résultat

En savoir plus

Dernière mise à jour : 01/09/2024

INFOS
PRATIQUES

Durée

45 heures

Modalité

Formation ouverte et à distance (FOAD) 

Date de début des cours

16/02/2026

Date de fin des cours

20/06/2026

Accessibilité handicap

En savoir plus

Comment s’inscrire ?

En savoir plus