La
méthode B a été élaborée par Jean-Raymond Abrial pour
spécifier, concevoir et coder des systèmes logiciels. Elle
est utilisée dans l'industrie, notamment dans les systèmes
de sécurité, de protection et de contrôle de vitesse des
trains.
Spécification formelle avec B est une
introduction à la notation B et à la méthode B. Le concept
de base est celui de machine abstraite dont l'état est
décrit par un invariant. La méthode consiste à prouver
formellement que les opérations respectent bien
l'invariant, puis à raffiner les machines abstraites en
machines implantables, et à prouver que ce raffinage est
correct. Le logiciel est ainsi prouvé par construction
relativement à sa spécification. L'architecture du logiciel
préconisée est l'architecture en couche.
A partir d'exemples simples de spécifications, l'ouvrage
propose un développement complet en B. Il présente les
bases mathématiques et logiques mises en oeuvre et détaille
les éléments du langage B, en allant de la spécification à
l'implantation.
Sommaire
1. Les sources de B
2. Re-rédaction d'un cahier des charges et introduction au
concept de machine abstraite
3. Introduction au développement d'un logiciel en B par un
exemple
4. La logique de la preuve
5. Ensembles
6. Relations et fonctions
7. Objet mathématique. nombres naturels, suite,
arbres
8. Structure d'une machine abstraite et preuve
d'opération
9. Les substitutions
10 :Choix de modèlisations ensemblistes
11. L'approche base de données, les contraintes dynamiques
et l'hypothèse du déterminisme linguistique de Sapir-
Whorf
12. Le raffinage
13. Séquencement et boucle
14. Composition des machines et des raffinements
16. l'implantation finales et la structure d'un projet
B
17. B évènementiel
18. B,VDM,Z et Spécifications algébriques
19. Glossaire
20. Bibliographie