Concurrent systems : models and analysis [ LINGI2143 ]

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

• 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)

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

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.

• 3 missions, 25% of the final grade.
•  Exercises: test at the end of the first period, 25% of the final grade.
• Theory: oral exam, 50% of the final grade. A list of questions is provided at the end of the first period.

Missions and test exercises can be presented again in the second session

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

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.