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

• 3.5 - Invariants et propriétés

• 3.6 - Construction du modèle par raffinement successif et décomposition

• 3.7 - Preuve mathématique

• 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