Concurrent systems : models and analysis

lingi2143  2017-2018  Louvain-la-Neuve

Concurrent systems : models and analysis
5 credits
30.0 h + 15.0 h
Q1
Teacher(s)
Pecheur Charles;
Language
English
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:

  • INFO1.1-3
  • INFO2.2-3, INFO2.5
  • INFO5.2, INFO5.5
  • INFO6.1, INFO6.4

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.1, SINF6.4

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.
 

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)
The exercise sessions are closely related to the assignments and help student using similar models and tools on other concurrent systems.
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.
The asssignments can only be presented during the quadrimester of the course.  They cannot be represented in subsequent exam sessions.
Other information
Background:
  • INGI1101 : Basic notions in discrete mathematics
  • INGI1123 : Basic notions in theory of computation
  • INGI1131 : Basic notions in concurrent systems
Online resources
http://icampus.uclouvain.be/claroline/course/index.php?cid=ingi2143
Bibliography
Livre de référence (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.
Faculty or entity
INFO


Programmes / formations proposant cette unité d'enseignement (UE)

Title of the programme
Sigle
Credits
Prerequisites
Aims
Master [120] in Data Science Engineering
DATE2M
5
Master [120] in Computer Science and Engineering
INFO2M
5
Master [120] in Computer Science
SINF2M
5
Master [120] in data Science: Information technology
DATI2M
5