Méthode B pour la spécification et la réalisation de logiciels et de systèmes critiques prouvés

INTRODUCTION

1 - COMPLEXITÉ CROISSANTE DES SYSTÈMES ET DES LOGICIELS – LES LOGICIELS CRITIQUES ET LEUR PROCESSUS DE RÉALISATION

• 1.1 - Principales difficultés de réalisation d'un logiciel critique
• 1.2 - Lien entre niveau de qualité du processus (méthodes et outils) et SIL (Safety Integrity Level )
• 1.3 - Analyses de sécurité et exigences de sécurité

2 - PETIT PANORAMA DES MÉTHODES DE FIABILISATION DES LOGICIELS

3 - PRINCIPES DE LA MÉTHODE B

• 3.1 - Principes généraux de la méthode B
• 3.2 - Bases mathématiques
• 3.3 - Niveau de formalisation ?
• 3.4 - Machines abstraites en B
  Figure 1 - Opération dans une machine
• 3.5 - Invariants et propriétés
• 3.6 - Construction du modèle par raffinement successif et décomposition
  Figure 2 - Importation de machines Figure 3 - Arbre d'implantation Figure 4 - Raffinement multiple Figure 5 - Visibilité selon différentes clauses : INCLUDES, USES, SEES et IMPORT
• 3.7 - Preuve mathématique
  Figure 6 - Arbre des preuves
• 3.8 - Pseudo-code B0
• 3.9 - Traduction du B0 en langage informatique puis en code source
• 3.10 - Pourquoi la nécessité des tests fonctionnels, malgré la preuve mathématique ?
• 3.11 - Méthode B et analyse fonctionnelle (type méthode APTE par exemple)

4 - MÉTHODE B ET LE PROCESSUS DE RÉALISATION DES LOGICIELS

5 - AVANTAGES ACTUELS DE LA MÉTHODE B VIS-À-VIS D'AUTRES MÉTHODES

6 - LIMITES DE B

• 6.1 - Lien avec la spécification de plus haut niveau (souvent en langage naturel)
• 6.2 - Paramètres et données (la preuve ne porte pas sur la valeur des données)
• 6.3 - Entrées (acquisition) et sorties (production)
• 6.4 - Parties non-écrites en B (parties non-critiques par exemple)
• 6.5 - Aspect informatique répartie ou redondance matérielle (commutation)

7 - B SYSTÈME OU B ÉVÉNEMENTIEL

• 7.1 - Prolongements de B au niveau système
• 7.2 - Preuve en B système
• 7.3 - Substitution en B événementiel
• 7.4 - Événements en B événementiel
• 7.5 - Raffinement en B Système
• 7.6 - Preuve en B Système
• 7.7 - Méthode B ne s'appliquant pas qu'aux logiciels mais aux systèmes

8 - AUTRES ASPECTS DE B

• 8.1 - Liens avec la spécification en langage naturel
• 8.2 - Peut-on utiliser d'autres méthodes avec B pour un même développement ?
• 8.3 - Bénéfice de la seule formalisation
• 8.4 - Évolution d'un logiciel dans un processus B
• 8.5 - Réutilisation de modules logiciels
• 8.6 - Aspects organisationnels
• 8.7 - Coût d'une telle méthode et ce qu'elle rapporte ?

9 - APPLICATIONS INDUSTRIELLES

• 9.1 - Utilisation de B et les secteurs industriels
• 9.2 - Outillage industriel et atelier B
• 9.3 - Retour d'expérience sur plus de quinze ans de pratique industrielle

10 - PERSPECTIVES D'AVENIR

11 - CONCLUSIONS SUR LA MÉTHODE B