Logiciels sûrs

Safe software Development

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)