Concurrent systems : models and analysis

Teacher(s)

Pecheur Charles;

Language

English
> French-friendly

Prerequisites

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

Learning outcomes

At the end of this learning unit, the student is able to :

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: INFO1.1-3 INFO2.2-3, INFO2.5 INFO5.2, INFO5.5 INFO6.5 Given the learning outcomes of the "Master [120] in Computer Science" program, this course contributes to the development, acquisition and evaluation of the following learning outcomes: SINF1.M1, SINF1.M2 SINF2.2-3, SINF2.5 SINF5.2, SINF5.5 SINF6.5 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.

Content

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.
Due to circumstances,all or part of the lectures and exercises may be streamed and recorded for distance learning.

Evaluation methods

• 3 assignments, 10% each = 30% of the final grade.
•  Written exam, 70% of the final grade.

The exam consists of an exercise part (40%) and a theory part (30%).  The theory part covers all material presented in the lectures and covered in the course material.  This is a closed-book exam.
The assignments can only be presented during the quadrimester of the course.  They cannot be represented in subsequent exam sessions; the grade remains acquired for subsequent sessions.
The use of artificial intelligence tools is allowed within the limits of the guidelines set forth by the University (accountability, autheticity, transparency).  In particular, AI can never help to solve exercises or missions, and its usage must always be explicitly documented.

Online resources

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

Bibliography

Livre de référence (non 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.

Teaching materials

• Les diapositives de cours ainsi que d'autres informations pertinentes et pratiques relatives au cours seront accessibles sur Moodle.
• Lecture slides and other relevant information pertaining to the course are available on Moodle.
• J Magee and J Kramer, Concurrency: State Models and Java Programming (2nd Ed.), Wiley, 2006.

Faculty or entity

> INFO