La preuve formelle permet de s’assurer de la cohérence de la spécification formelle. Dans le cadre d’un développement en B, elle permet en particulier de vérifier qu’à chaque étape de raffinement, la spécification raffinée vérifie les exigences amont.

Objectifs :

  • Acquérir les mécanismes essentiels de preuve d’un modèle B
  • Maîtriser les notions avancées du langage B permettant d’optimiser l’activité de preuve

 

Pré-requis :

Connaissance du langage B et de sa mise en œuvre pour la spécification de systèmes complexes.

Programme sur 3 jours :

 

  • Principes de la méthode B et applications dans le cadre d’un développement logiciel
  • Preuve d’un projet B logiciel
  • Preuve des lemmes au travers d’un prouveur interactif
  • Écriture et vérification des règles utilisateurs
  • Enchaînement des activités liées à la preuve et à sa vérification
  • Environnement et outils

Contactez-nous  Catalogue des formations

Activité enregistrée sous le numéro 93 13 12834 13 auprès du préfet de région Provence-Alpes-Côte d’Azur.