Modeling and analysis of concurrent systems
Lecturers
- Gwen Salaün (principal)
- Frédéric Lang
- Radu Mateescu
- Wendelin Serwe
Target skills
- Understand the key concepts of concurrent systems: parallel and interleaved execution, mutual exclusion, race conditions, deadlocks, livelocks.
- Acquire methodologies to build correct systems at first, to avoid painful issues of debugging poorly-designed systems.
- Discover modern ways of modelling concurrent systems using formal languages
- Get acquainted with software tools that automatically find design mistakes in concurrent systems.
- Discover the ideas of famous computer scientists: Dijkstra, Hoare, Milner, Clarke, Emerson, Sifakis, who all received the prestigious Türing award.
Prerequisite
Knowledge of sequential programming. Some notions of functional programming and/or first-order logic would be a plus.
Contents
Today, most execution platforms are concurrent, ranging from multi-core laptops and mobile devices to large-scale cloud computing and Web services. Thus, the amount of systems that must deal with parallel and distributed aspects is steadily growing. However, it is well-known that such systems are harder to design and more error-prone that sequential software, but there bow exist methodologies and tools that help designing correct systems.
The objective of this course is to study models and languages for concurrent systems, covering software, hardware, and networking protocols. The central topic of this course is concurrency theory, with an overview of high-level languages, lower-level models, and formal semantics. The course also presents verification methods for concurrent systems, including temporal logics, model checking, and equivalence checking to verify the proper behaviour of concurrent systems.
This course is divided into two complementary parts. Part 1 is also offered to 3rd-year engineering students of ENSIMAG.
Part 1: Models and languages for model checking
Introduction to concurrency theory
- Concurrency-related issues in real life
- Principal concepts of concurrency: linear-time vs branching time, interleaving vs true concurrency, localities
Automata-based models of concurrency
- Labelled transition systems and Kripke structures
- Communicating automata / communicating state machines
- Timed automata
Higher-level languages for concurrent systems
- Process calculi / process algebra
- A simple calculus: CCS
- Value-passing languages: LNT
- Name-passing calculi and mobility: the pi-calculus
- Possible semantics for concurrency: denotational, axiomatic, operational
- Structured Operational Semantics (Plotkin rules, SOS, GSOS, and other rule formats)
Temporal logic and model-checking verification
- State space, reachability analysis, and state-space explosion issues
- Basic properties: deadlocks, livelocks, starvation, fairness, etc.
- Action-based vs state-based properties
- Explicit-state vs symbolic state-space exploration — related models: BDDs, BESs, etc.
- On-the-fly verification, partial-order reductions, unfoldings, bounded model-checking
- Linear-time vs branching-time logics
- Classical logics: mu-calculus, LTL, CTL, CTL*, PDL
- Predefined temporal-logic patterns
- Examples of model-checking verification tools
Part 2: Advanced verification techniques and applications
Other mainstream models of concurrency
- Symbolic automata
- Petri nets
Behavioural equivalences and equivalence-checking verification
- Behavioural abstractions — visible and hidden actions in concurrency models
- Bisimulations, preorder relations, and other equivalences
- Minimisation vs checking of equivalences and preorders
- Classical algorithms for computing bisimulations: Paige-Tarjan, Groote-Vaandrager, signature-based, etc.
- Congruence results — compositional verification — behavioural interfaces
- Examples of equivalence-checking verification tools
Temporal logic with data
- (to be provided)
Applications
- Realistic use cases taken from protocols, software, and hardware
- Business processes (BPMN)
- Web services
- cloud computing
Credits
3 ECTS for each part – 6 ECTS for the whole HECS “core” course, which comprises both parts.