<- Archives UCL - Programme d'études ->



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

 > http://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
> Master [120] in Computer Science and Engineering
Faculty or entity
in charge
> INFO


<<< Page précédente