UCL - Concurrent systems : models and analysis

[INGI2143]

[30h + 15h] 5 credits

This course is taught in the 1st semester.

Teacher(s): Charles Pecheur

Language: English

Level: Second

Aims
Main themes
Content and teaching methods
Other information (prerequisite, evaluation (assessment methods), course materials recommended readings, ...)

Aims

- To master mathematic concepts and tools which enable modelling and analysis of concurrent computer systems
- To be able to model an actual system in a appropriate abstract formalism
- To be used to automated verification technics used to analyse those systems

Main themes

This course studies the principles, formalisms and tools used to model and analyse concurrent computer systems.

Content and teaching methods

- Modelling of concurrent systems: processes and actions, conditions and choice, concurrency, synchonization, process algebra
- Semantics of concurrent systems: state machines, transition systems, finite and infinite traces, parallelism by interleave, equivalence and minimization
- Features of concurrent systems: invariant, safety, agility, temporal logic, refinement relations
- Verification of concurrent systems: model checking, equivalence checking

Other information (prerequisite, evaluation (assessment methods), course materials recommended readings, ...)

pre requisites
- Basic of discrete mathematics (for example INGI1101)

Refence book
- J Magee and J Kramer, Concurrency : State Models and Java Programming (2nd Ed.), Wiley, 2006.

Interresting books
- 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.