Click here for English. 
Le Cycle de Développement logiciel adopté est représenté par le schéma ci-dessous.
Cette étape consiste à lister l'ensemble des exigences listées dans le Cahier des Charges (exigences fonctionnelles et contraintes opérationnelles).
Chaque exigence est référencée dans le Cahier des Charges, elle est notée [Exx] où xx est le numéro de l'exigence. Les exigences qui peuvent se déduire d'exigences déjà référencées ne sont pas introduites.
Cette étape consiste à proposer un modèle fonctionnel sous la forme de planches SADT (décomposition en activité). Ce modèle participe à l'élaboration de la Spécification formelle B.
Cette étape permet la construction du modèle B, à partir des planches SADT du Dossier de Spécification fonctionnelle.
L'étape de spécification formelle consiste à construire un premier modèle B à partir des planches SADT du dossier de Spécification Formelle.
L'étape de Conception Formelle consiste, ensuite, à raffiner le premier modèle et s'achève lorsque toutes les implantations sont obtenues.
Nous allons décrire la méthode employée pour l'étape de Spécification Formelle, pour plus de renseignements consulter la rubrique Informations méthodologiques.
Chaque activité décrite dans les planches SADT devient une opération B; il reste à déterminer dans quels composants B ces opérations sont définies.
Soit l'exemple suivant : dans un logiciel de contrôle commande l'activité principale (c'est à dire un cycle de traitement) est décomposée par une activité d'acquisition de données puis une activité de traitement et enfin une phase d'émission des résultats.
L'activité de plus haut niveau est en fait décomposée en trois sous-activité. De la même façon l'opération B de plus haut niveau, correspondant au cycle de traitement, utilise les opérations B dédiées à l'acquisition de données puis au traitement de ces données et enfin à l'émission des résultats.
Chaque activité présente dans le schéma précédent est transformée en une opération B. La modélisation B obtenue est présentée dans le schéma suivant.
La construction du modèle s'accompagne d'une étape de vérification formelle; les Obligations de Preuve produites doivent être démontrées.
Pour chaque composant, le prouveur automatique est utilisé pour démontrer les Obligations de Preuve. Les OP restantes sont vérifiées "visuellement", le développeur note simplement, pour chaque obligation de preuve restant à démontrer, la démonstration qui permet de confirmer la validité de l'OP. Le travail de preuve interactive n'est pas réalisée lors de cette étape.
Lorsque le modèle B est entièrement construit et lorsque toutes les obligations de preuve restant à démontrer sont vérifiées, le travail de preuve interactive peut commencer.
L'utilisation des plateformes de traduction de l'Atelier B rend cette étape automatique.
Cette étape de génération de code informatique est décomposée en deux phases :
La première étape peut s'accompagner de tests préliminaires qui s'effectuent sur le modèle B traduit. Les "coquilles vides" des implantations des machines de base spécifient des tests (pour la machine de base associée à la carte bancaire, la coquille vide spécifie un code, une date de validité, le montant maximum du retrait...). Ces implantations sont traduites automatiquement et permettent la génération d'un exécutable complet. On vérifie ainsi, en modifiant les informations contenues dans les implantations des machines de base, puis en regénérant l'exécutable, que le modèle B traduit se comporte normalement. Cette phase de prototypage sera complétée par l'utilisation de l' Animateur de l'Atelier B. Cet outil réalise l'exécution symbolique d'un composant logiciel, d'une partie du modèle B ou de l'ensemble du modèle.
L'étape de prototypage ou d'animation est importante puisqu'elle permet de détecter les possibles problèmes de formalisation (mauvaise prise en compte des exigences du système) ou des non-dits dans le Cahier des Charges.
Seuls les test unitaires du code associé aux machines de base et de l'Interface Homme Machine sont réalisés sur le projet DAB.
Les tests préliminaires montrent que le logiciel produit à partir du modèle B (dans sa totalité) se comporte correctement.
Les test d'intégration montrent la validité des interfaces entre les différents composants logiciels; les interfaces entre les composants logiciels issus du modèle B sont correctes, seules les interfaces entre les composants B et non B sont testées.
Les tests de validation sont identiques à ceux réalisés pour un développement classique. Ils s'exécutent sur le logiciel complet, les scenarii de tests de validation doivent couvrir l'ensemble des exigences du Cahier des Charges ; pour cela une matrice de traçabilité est fournie.