Conception et Spécification des Systèmes Concurrents
NFP103
Objectifs pédagogiques :
De par le développement 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
- de comprendre les problèmes fondamentaux des systèmes concurrents
- et d'acquérir des notions de spécification de ces systèmes
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, “thread”, 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 :
* Expressions régulières et automates finis à états
* automates, automates synchronisés
* Preuve de programme:
* contrat de fonction, pré-post-conditions, invariants de boucles
* terminaison
* structures de Kripke, logiques temporelles
Bibliographie :
- Michel Raynal: Concurrent Programming: Algorithms, Principles, and Foundations
- Peter Linz, Susan H. Rodger: An Introduction to Formal Languages and Automata
Cette UE apparaît dans les diplômes et certificats suivants :
- MR11602A : Master Sciences, technologies, santé mention Informatique parcours Recherche opérationnelle
- MR11603A : Master Sciences, technologies, santé mention Informatique parcours Systèmes d'information et business intelligence
- MR11603B : Master Sciences, technologies, santé mention Informatique parcours Systèmes d'information et business intelligence HTT
- MR11604A : Master Sciences, technologies, santé mention Informatique parcours Traitement de l'information et exploitation des données
- MR11606A : Master Sciences, technologies, santé mention Informatique parcours Réseaux et objets connectés
- MR11605A : Master Sciences, technologies, santé mention Informatique parcours Préparation à l'agrégation en informatique
- MR11607A : Master Sciences, technologies, santé mention Informatique parcours Sécurité informatique, cybersécurité et cybermenaces en Bretagne
- CYC9101A : Diplôme d'ingénieur Spécialité informatique parcours Architecture et ingénierie des systèmes et des logiciels (AISL)
