5 crédits
30.0 h + 15.0 h
Q1
Enseignants
Pecheur Charles;
Langue
d'enseignement
d'enseignement
Anglais
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
d'apprentissage
A la fin de cette unité d’enseignement, l’étudiant est capable de : | |
| 1 | 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 :
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 :
Les étudiants ayant suivi avec fruit ce cours seront capables de
Les étudiants auront développé des compétences méthodologiques et opérationnelles. En particulier, ils auront développé leur capacité à
|
La contribution de cette UE au développement et à la maîtrise des compétences et acquis du (des) programme(s) est accessible à la fin de cette fiche, dans la partie « Programmes/formations proposant cette unité d’enseignement (UE) ».
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.
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)
Modes d'évaluation
des acquis des étudiants
des acquis des étudiants
- 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.
Les missions devront être présentées lors du quadrimestre de cours. Ils ne pourront pas être représentées au cours des sessions d'examens ultérieures.
Autres infos
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
Ressources
en ligne
en ligne
Bibliographie
Livre de référence (obligatoire)
- J Magee and J Kramer, Concurrency: State Models and Java Programming (2nd Ed.), Wiley, 2006.
- 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.
Faculté ou entité
en charge
en charge
INFO
Programmes / formations proposant cette unité d'enseignement (UE)
Intitulé du programme
Sigle
Crédits
Prérequis
Acquis
d'apprentissage
d'apprentissage
Master [120] : ingénieur civil en science des données
Master [120] : ingénieur civil en informatique
Master [120] en sciences informatiques
Master [120] en science des données, orientation technologies de l'information