CentraleSupélec — Département informatique
Plateau de Moulon
3 rue Joliot-Curie
F-91192 Gif-sur-Yvette cedex
Développement de systèmes critiques avec la méthode B

Code : 3IF2250, 21 HPE

PDF de la présentation aux élèves du 7 novembre 2022

Contact

Idir AIT SADOUNE idir.aitsadoune@centralesupelec.fr

Prérequis

FR

Cursus commun en informatique

EN

Computer Science Shared curriculum

Présentation générale

FR

Ce cours présente la méthode B : les concepts de base allant des structures les plus élémentaires comme la machine B à la preuve en utilisant le prouveur interactif de l'Atelier-B. Les étudiants appliqueront un processus de développement de logiciels critiques en partant de la spécification jusqu'au code source en utilisant l'approche de développement formelle B.

EN

This course introduces the B-method: the basic concepts ranging from the most basic structures like the B machine to proofs using the Atelier-B interactive prover. Students will apply a critical software development process from specification to source code using the formal B development approach.

Acquis d’apprentissage visés dans le cours

FR

À l'issu de ce cours, les étudiants seront capables de :

  • modéliser avec la méthode B.
  • manipuler les notions de Machine abstraite et de raffinement.
  • établir la preuve de consistence d'un modèle B et de son raffinement (avec le prouveur de l'Atelier B).
  • animer un modèle B (avec le model-checker Pro-B).
  • générer un code vérifié à partir d'un modèle B
  • développer des logiciels critiques

EN

At the end of the course, students will be able to :

  • model with the B-method.
  • manipulate the notions of abstract machine and refinement.
  • establish the proof of consistency of a B model and its refinement (with the prover of Atelier B).
  • animate a B model (with the Pro-B model-checker).
  • generate verified code from a B model
  • develop critical software

Moyens

FR

Les pratiques utilisés dans ce cours combinent cours magistraux et TD favorisant une pratique concrète sur les outils existants autour de la méthode B.

EN

The practices used in this course combine lectures and tutorials favouring a concrete practice on the existing tools around the B method.

Description des compétences acquises à l'issue du cours

FR

  • C1.4 Spécifier, concevoir, réaliser et valider tout ou partie d'un système complexe
  • C2.1 Avoir approfondi un domaine ou une discipline relatifs aux sciences fondamentales ou aux sciences de l'ingénieur.
  • C6.4 Résoudre des problèmes dans une démarche de pensée computationnelle

EN

  • C1.4 Design, detail and corroborate a whole or part of a complex system.
  • C2.1 Thoroughly master a domain or discipline based on the fundamental sciences or the engineering sciences.
  • C6.4 Solve problems through mastery of computational thinking skills.

Contenu

FR

  • C1-C2 (CM-TD) : Le langage B
    • La théorie des ensembles
    • La logique du 1e ordre et la Logique de Hoare.
    • Les substitutions généralisées et le calcul de la plus faible pré-condition de Dijkstra
  • C3-C4 (CM-TD) : Le modèle B
    • La modélisation d'un système en utilisant la méthode B classique
    • Le raffinement d'un système en B
  • C5-C6 (CM-TD) : La preuve en B
    • Les obligations de preuve d'un modèle B
    • La preuve interactive avec l'atelier B
  • C7-C8 (CM-TD) : Le modèle checking en B
    • Animation de modèles B avec ProB
    • Visualisation de modèles B avec BMotion
  • C9-C10 (CM-TD) : L'implémentation d'un modèle B
    • Génération de code par raffinement
  • C11-C14 (TP) : TP sur machine

EN

  • C1-C2 (CM-TD): The B Language
    • Set theory
    • The 1st Order logic and the Hoare Logic.
    • Generalized substitutions and the Dijkstra weakest precondition.
  • C3-C4 (CM-TD): The B Model
    • Modelling a system using the classical B-method
    • The refinement of a B system
  • C5-C6 (CM-TD): The proof in B method
    • The proof obligations of a B Model
    • Interactive proof with Atelier-B
  • C7-C8 (CM-TD): The checking model in B method
    • B-model animation with ProB
    • Viewing B models with BMotion
  • C9-C10 (CM-TD): The implementation of a B model
    • Code generation by refinement
  • C11-C14 (TP) : lab session on machine

Méthodes pédagogiques

FR

  • Cours magistraux pour présenter les concepts
  • TD/TP pour mettre en œuvre les concepts

EN

  • Lectures to introduce the concepts
  • lab sessions to implement the concepts

Méthodes d'évaluation

FR

L'évaluation consiste en un TP noté.

EN

The grading of the course is based on a graded project.

Bibliographie / supports

REFERENCE MANUAL ]]