Concurrent systems : models and analysis [ LINGI2143 ]

> https://icampus.uclouvain.be/claroline/course/index.php?cid=ingi2143

Ce cours étudie les principes, les formalismes et les outils utilisés pour modélisation et d'analyse de systèmes informatiques concurrents.

• Modèles des systèmes concurrents
  
• Sémantique des systèmes concurrents
• Propriétés des systèmes concurrents
• Vérification de systèmes concurrents

Eu égard au référentiel AA du programme « Master ingénieur civil en informatique », ce cours contribue au développement, à l'acquisition et à l'évaluation des acquis d'apprentissage suivants :

• INFO1.1-3
• INFO2.2-3, INFO2.5
• INFO5.2, INFO5.5
• INFO6.1, INFO6.4

Eu égard au référentiel AA du programme « Master [120] en sciences informatiques », ce cours contribue au développement, à l'acquisition et à l'évaluation des acquis d'apprentissage suivants :

• SINF1.M1, SINF1.M2
• SINF2.2-3, SINF2.5
• SINF5.2, SINF5.5
• SINF6.1, SINF6.4

Les étudiants ayant suivi avec fruit ce cours seront capables de

• maîtriser les concepts et les outils mathématiques qui permettent de modéliser et d'analyser le comportement d'un système informatique concurrent ;
• modéliser et un système concret dans un formalisme abstrait approprié ;
• Se familiariser aux techniques de vérification automatique utilisées pour l'analyse de ces systèmes.

Les étudiants auront développé des compétences méthodologiques et opérationnelles.  En particulier, ils auront développé leur capacité à

• modéliser un logiciel existant;
• penser à l'aide d'abstractions et utiliser un formalise pour déduire des propriétés d'un système existant.

• 3 missions, 30% de la note finale.
• Exercices: test en fin de quadrimestre, 30% de la note finale.
• Théorie: examen oral, 40% de la note finale.  Une liste de questions est fournie à la fin du cours.

• Cours magistraux
• Séances d'exercices (d'abord des exercices plus théoriques pour acquérir les concepts et ensuite, des séances en salle informatique pour appliquer ces concepts à des systèmes concurrents de plus en plus complexes)
• Missions (par groupe de 2 étudiants)

Les séances d'exercices et les missions sont "synchronisées" de manière à ce que les exericices préparent les étudiants à réaliser les tâches nécessaires pour mener à bien la mission en cours.

• Modélisation de systèmes concurrents : processus et actions, conditions et choix, concurrence, synchronisation, algèbre de processus.
• Sémantique de systèmes concurrents : machines d'états et systèmes de transitions, traces finies et infinies, parallélisme par entrelacement, équivalences et minimisation.
• Propriétés de systèmes concurrents : invariants, propriétés de sûreté et de vivacité, logique temporelle, relations de raffinement.
• Vérification de systèmes concurrents : model checking, equivalence checking.

Livre de référence (obligatoire)

• J Magee and J Kramer, Concurrency: State Models and Java Programming (2nd Ed.), Wiley, 2006.

Autres références

• H Bowman and R Gomez, Concurrency Theory: Calculi and Automata for Modelling Untimed and Timed Concurrent Systems, Springer, 2006.
• AW Roscoe, The Theory and Practice of Concurrency, Prentice Hall, 1998 (http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf).
• E Clarke, O Grumberg and D Peled, Model Checking, MIT Press, 1999.
• B Bérard et al., Systems and Software Verification, Springer, 2001.

Préalables :

• INGI1101 : Notions de base en mathématiques discrètes
• INGI1123 : Notions de base de calculabilité
• INGI1131 : Notions de base sur les systèmes concurrents