Note from June 29, 2020
Although we do not yet know how long the social distancing related to the Covid-19 pandemic will last, and regardless of the changes that had to be made in the evaluation of the June 2020 session in relation to what is provided for in this learning unit description, new learnig unit evaluation methods may still be adopted by the teachers; details of these methods have been - or will be - communicated to the students by the teachers, as soon as possible.
Although we do not yet know how long the social distancing related to the Covid-19 pandemic will last, and regardless of the changes that had to be made in the evaluation of the June 2020 session in relation to what is provided for in this learning unit description, new learnig unit evaluation methods may still be adopted by the teachers; details of these methods have been - or will be - communicated to the students by the teachers, as soon as possible.
5 credits
30.0 h + 15.0 h
Q1
Teacher(s)
Pecheur Charles;
Language
English
Prerequisites
Basic notions in discrete mathematics (such as LINFO1114 or LEPL1108), theory of computation (such as LINFO1123), and concurrent systems (such as LINFO1104).
Main themes
This course studies the principles, formalisms and tools used to model and analyse concurrent computer systems.
- Models of Concurrent Systems
- Semantics of Concurrent Systems
- Properties of Concurrent Systems
- Verification of Concurrent Systems
Aims
At the end of this learning unit, the student is able to : | |
| 1 |
Given the learning outcomes of the "Master in Computer Science and Engineering" program, this course contributes to the development, acquisition and evaluation of the following learning outcomes:
|
The contribution of this Teaching Unit to the development and command of the skills and learning outcomes of the programme(s) can be accessed at the end of this sheet, in the section entitled “Programmes/courses offering this Teaching Unit”.
Content
- Models of Concurrent Systems: processes and actions, conditions and choices, concurrency, synchronization, process algebras.
- Semantics of Concurrent Systems: state machines and transition systems, finite and infinite traces, concurrency by interleaving, equivalences and minimization.
- Properties of Concurrent Systems: invariants, safety and liveness properties, temporal logic, refinement relations.
- Verification of Concurrent Systems: model checking, equivalence checking.
Teaching methods
- Lectures
- Exercises (theoretical exercises to master the concepts, followed by computer room session to apply these on concurrent systems)
- Assignments (performed conjointly by two students)
Evaluation methods
- 3 assignments, 30% of the final grade.
- Exercises: test at the end of the first period, 30% of the final grade.
- Theory: oral exam, 40% of the final grade. A list of questions is provided at the end of the course.
Online resources
Bibliography
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.
Faculty or entity
INFO
