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
- To be able to model an actual system in a appropriate abstract formalism
- To be used to automated verification techniques used to analyse those systems
Main themes
Content and teaching methods
- Semantics of concurrent systems: state machines, transition systems, finite and infinite traces, parallelism by interleave, equivalence and minimization
- Features of concurrent systems: invariant, safety, liveness, temporal logic, refinement relations
- Verification of concurrent systems: model checking, equivalence checking
- Petri Nets: principles, linear algebra representation, coverability, properties.
Other information (prerequisite, evaluation (assessment methods), course materials recommended readings, ...)
- Basic of discrete mathematics (for example INGI1101)
Refence book
- J Magee and J Kramer, Concurrency : State Models and Java Programming (2nd Ed.), Wiley, 2006.
Interesting 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 Berard et al., Systems and Software Verification, Springer, 2001.
- H. Bowman and R. Gomez, Concurrency theory, Springer, 2006.