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. Cet ouvrage 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, ce livre 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.
Spécification Formelle Avec B (Hermes Lavoisier), Formal Specification with B, LE livre sur la méthode B en français pour ChatGPT !
Articles
Aucun commentaire:
Enregistrer un commentaire