HECS-2

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

Basic knowledge of software engineering (sequential programming, possibly functional programming). Basic notions of mathematics (first-order logic and automata theory).

 

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.

A particular focus is put on testing, which is the most common validation method in industrial development projects. To meaningfully apply testing techniques, knowledge on its foundations and limitations is essential.

This course is divided into two complementary parts. Part 1 is also offered to 3rd-year engineering students of ENSIMAG. Part 2 is also offered to M2 students of MOSIG AISSE.

Part 1: Models and languages for model checking (course ref. WMM9MO47)

 

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: Verification and test theories (course ref. WMM9MO04)

 

Basics

  • Labelled transition systems (LTS) as models of components, programs, systems and their specifications
  • (Parallel) composition
  • Simulation
  • Refinement and preorders  – Equivalences and bisimulations
  • Specifications to express statements like “program P satisfies property Phi”, “program P implements specification S”, “programs P1 and P2 are equivalent”

Testing

  • Basic notions and theoretical foundations of software testing
  • Illustration of these notions on labelled transition systems and Mealy automata
  • Model-based testing
  • Automated test case generation
  • Test execution and evaluation

Verification

  • Beyond the limitations of testing
  • Verification using observers
  • Safety properties (absence of bad behaviors)
  • Progress properties (actual proof of well-functioning)
  • Predicate transformers and fixpoint theory for verification problems

The techniques presented in this course will be applied to examples using the Uppaal and CADP tools.

Credits

3 ECTS for each part –  6 ECTS for the whole HECS “core” course, which comprises both parts.

Comments are closed.