System Design - WMM9MO70

Goal(s)

Understand the key concepts of concurrent systems: parallel and interleaved execution, mutual exclusion, race conditions, deadlocks, livelocks.
Understand the key concepts of systems that evolve continuously with time, and how they can be controlled and verified.
Acquire methodologies to build correct concurrent and real-time 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.
Understand cyberphysical embedded systems specifications, design and verify systems with concurrency, real-time, stochastics or hybrid (analog/digital) properties.

Content(s)

This course consists of 2 parts.
Part 1 (3 ECTS), joint with Ensimag (3rd year)

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
-Possible semantics for concurrency: denotational, axiomatic, operational
-Structured Operational Semantics (Plotkin rules, SOS)
Temporal logic and model-checking verification
-State space, reachability analysis, and state-space explosion issues
-Basic properties: deadlocks, livelocks, starvation, fairness, etc.
-On-the-fly verification
-Linear-time vs branching-time logics
-Classical logics: mu-calculus, LTL, CTL, CTL*, PDL
-Predefined temporal-logic patterns
-Examples of model-checking verification tools
Lab exercises

Part 2 (3 ECTS):

Timing analysis of systems
-Response time analysis
-WCET (Worst-case execution time) analysis
-Interference analysis in multicore systems
Probabilistic and stochastic systems
-Probabilistic and stochastic behaviours — Randomized algorithms
-Discrete-Time and Continuous-Time Markov Chains, and their concurrent extensions
-Steady-state and transient analyses — Probabilistic temporal logics
-Safety analysis — Static and dynamic fault-trees
Hybrid systems
-Hybrid automata
-Set-based simulation of continuous-discrete behaviour
-Software tools for analyzing hybrid systems
-Applications to electric circuits, automotive systems, biological systems, etc.
Lab exercises

Basic knowledge of software engineering (sequential programming, possibly functional programming).
Basic notions of mathematics (first-order logic and automata theory).
No specific knowledge about hardware and software systems is required.