Modeling and analysis of concurrent systems

Lecturers

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.

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.

HECS-2