<- Archives UCL - Programme d'études ->



Concurrent systems : models and analysis [ LINGI2143 ]


5.0 crédits ECTS  30.0 h + 15.0 h   1q 

Enseignant(s) Pecheur Charles ;
Langue
d'enseignement:
Anglais
Lieu de l'activité Louvain-la-Neuve
Ressources
en ligne

 > http://www.icampus.ucl.ac.be/claroline/course/index.php?cid=INGI2143

Préalables
  • Notions de base en mathématiques discrètes (p.e. INGI1101)
  • Notions de base de calculabilité (p.e. INGI1123)
  • Notions de base sur les systèmes concurrents (p.e. INGI1113)
Thèmes abordés

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
Acquis
d'apprentissage

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.
Modes d'évaluation
des acquis des étudiants

Examen oral (2/3 de la note finale)

  • Theorie (basé sur des questions disponibles à la fin du quadrimestre)
  • Exercices

Missions (1/3 de la note finale)

Méthodes d'enseignement
  • 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.

Contenu
  • 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.
Bibliographie

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.
Cycle et année
d'étude
> Master [120] en sciences informatiques
> Master [120] : ingénieur civil en informatique
Faculté ou entité
en charge
> INFO


<<< Page précédente