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

Objectifs

• Acquérir une connaissance pratique des "bons" patrons de la programmation concurrente (Java)


• Comprendre les problèmes fondamentaux des systèmes concurrents


• S'initier à des méthodes et techniques de vérification automatique de ces systèmes (model-checking, logiques temporelles) 

Programme 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.

Validation et sanction

Attestation de formation

Type de formation

Non certifiante

Sortie

Sans niveau spécifique