Aller au menu Aller au contenu
Une voie, plusieurs choix
Informatique et Mathématiques appliquées
Une voie, plusieurs choix

> Formation > Cursus ingénieur

System Design - WMM9MO70

A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail cet article Facebook Twitter Linked In
  • Number of hours

    • Lectures : 36.0
    • Tutorials : -
    • Laboratory works : -
    • Projects : -
    • Internship : -
    • Written tests : -
    ECTS : 6.0
  • Officials : Frederic LANG


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.


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.


The exam is given in english only FR


The course exists in the following branches:

  • Curriculum - Master in Computer Science - Semester 9 (this course is given in english only EN)
see the course schedule for 2022-2023

Additional Information

Course ID : WMM9MO70
Course language(s): FR

You can find this course among all other courses.

A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail cet article Facebook Twitter Linked In

Date of update September 21, 2022

Université Grenoble Alpes