Concurrent systems : models and analysis [ LINGI2143 ]
5.0 crédits ECTS
30.0 h + 15.0 h
1q
Teacher(s) |
Pecheur Charles ;
|
Language |
English
|
Place of the course |
Louvain-la-Neuve
|
Online resources |
> https://www.icampus.ucl.ac.be/claroline/course/index.php?cid=INGI2143
|
Prerequisites |
- Basic notions in discrete mathematics (e.g. INGI1101)
- Basic notions in theory of computation (e.g. INGI1123)
- Basic notions in concurrent systems (e.g. INGI1113)
|
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 |
Students completing successfully this course will be able to
- master the mathematic concepts and tools which enable modelling and analysis of concurrent computer systems;
- model an actual concurrent system in a appropriate abstract formalism;
- use automated verification techniques to analyse concurrent systems.
Students will have developed skills and operational methodology. In particular, they have developed their ability to
- model existing software;
- thinking with abstractions and use a formalized approach to infer properties of an existing system.
|
Evaluation methods |
Oral examination (2/3 of the final grade)
- Theory (based on questions available at the end of the semester)
- Exercises
Assignments (1/3 of the final grade)
|
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)
The exercise sessions are closely related to the assignments and help student using similar models and tools on other concurrent systems.
|
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.
|
Bibliography |
Reference book (mandatory)
- J Magee and J Kramer, Concurrency: State Models and Java Programming (2nd Ed.), Wiley, 2006.
Additional references
- 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] in Computer Science and Engineering
> Master [120] in Computer Science
|
Faculty or entity in charge |
> INFO
|
<<< Page précédente
|