Logiciels sûrs

Safe software Development

Description: This course will enable students to discover the basic concepts of the formal Event-B method through modeling and proof activities using Atelier Rodin, the main IDE for the Event-B method. The application of a top-down specification approach will enable students to use refinement, which is one of the basic operations of the Event-B method, and automatically generate verified C code that complies with the initial specification. The animation of Event-B models using the ProB tool is also covered. Finally, to cover the verification needs of existing critical code, formal verification techniques will also be presented and put into practice with the WP and MetAcsl plugins of the Frama-C platform.

Learning outcomes: At the end of this course, students will be able to apply a complete critical software development process, from specification to automatic source code generation.

Evaluated skills:

  • Development
  • Certification

Course supervisor: Idir Ait Sadoune

Geode ID: SPM-INF-023

CM:

  1. Introduction à la méthode Event-B (1.5 h)
  2. L’activité de preuve dans la méthode Event-B (1.5 h)
  3. Le raffinement d’un modèle Event-B (1.5 h)
  4. Introduction au Model-Checking (1.5 h)
  5. Validation d’une spécification Event-B par Model-Checking (1.5 h)
  6. Spécification et vérification formelle avec Frama-C/WP (3.0 h)
  7. Vérification formelle de propriété de sécurité avec Frama-C/MetAcsl (3.0 h)

TD:

  1. Introduction à la méthode Event-B (1.5 h)
  2. L’activité de preuve dans la méthode Event-B (1.5 h)
  3. Le raffinement d’un modèle Event-B (1.5 h)
  4. Introduction au Model-Checking (1.5 h)
  5. Validation d’une spécification Event-B par Model-Checking (1.5 h)

TP:

  1. Etude de cas - s1 (3.0 h)
  2. Etude de cas - s2 (3.0 h)