v2.11.0 (5596)

Cours scientifiques - CSC_3S008_EP : Formal methods and model checking

Descriptif

Our society relies on software and hardware systems for both safety- and mission-critical applications (e.g., autonomous vehicles, control systems, device drivers, ...) in different domains (e.g., aerospace, avionics, medical devices, ...). However, designing correct and reliable systems is challenging due to the systems' complexity (e.g., system's size, concurrency, ...). Model Checking studies the theory and algorithms that automatically check if a system always behaves "as intended". Such algorithms are successfully used in real life to verify hardware (e.g., in companies designing hardware like Intel, ARM, Apple, ...) and software (e.g., at NASA, Microsoft, ...).

This course is an introduction to Model Checking and will explain how we can specify a system (e.g., a program, the design of a microprocessor, a distributed protocol) and its properties with a mathematical formalisms (e.g., logic) and how we can reason automatically about all the possible system's executions (e.g., to show that a program or the design of a microprocessor do not contain bugs).

At the end of the course, a student will be able to:

- Model discrete systems (e.g., programs) using formal languages to precisely define the system's executions.

- Express different system properties (e.g., safety, liveness) using temporal logic.

- Reason algorithmically about all the possible executions of a system, deciding if a system satisfies a property.

- Implement the basic model checking algorithms for discrete systems and temporal logic properties.

- Manipulate programmatically state machines, automata, and logical formulas.

- Recognize the challenges of (statically) checking a complex system.

The lectures cover the theoretical aspects of Model Checking, introducing the necessary background, algorithms, and proofs showing the correctness of the approaches. During the tutorials, the students will learn how to implement, in practice, such automated reasoning techniques.

The course focuses on the algorithms for discrete, finite-state systems. It is a starting point for model checking more expressive systems, such as infinite-state systems (e.g., real software), probabilistic systems, timed and hybrid systems (e.g., control systems), and machine-learning systems (e.g., neural networks). The course is also a starting point for exploring other problems in formal methods (e.g., automated program synthesis).

Numérique sur 20

Pour les étudiants du diplôme Bachelor of Science de l'Ecole polytechnique

Vos modalités d'acquisition :

The student evaluation will be composed of:

- 50% from the tutorial activities.

Each tutorial will require the students to complete individually various tasks, from modeling and verifying a system to implementing the algorithms explained in class.

- 50% from a final exam (2 hours exam, no external material allowed)

Remedial exam: the remedial exam session will require you to submit a subset of the tutorials (to be agreed before the session) and an oral examination.

Le rattrapage est autorisé (Note de rattrapage conservée écrêtée à une note seuil de 9)
L'UE est acquise si Note finale >= 9
• Crédits ECTS acquis : 4 ECTS

La note obtenue rentre dans le calcul de votre GPA.