Mise en oeuvre de la méthode B

La mise en place d’un logiciel sans défaut reste primordiale pour plusieurs
domaines qui requièrent des applications dites de sécurité comme les
transports. La réalisation d’un modèle formel est l’approche la plus efficace
pour atteindre l'objectif du zéro défaut, que ce soit en termes de temps ou de
maîtrise de la complexité. Ce modèle permet d’analyser et de vérifier le
comportement d’un logiciel. Cet ouvrage présente la méthode B, une méthode
formelle s’appuyant sur la preuve de propriétés qui, sur la base d’une
spécification et de la notion de raffinement, permet d’aller jusqu’à la
production automatique de code. Différents outils découlant de cette méthode
ainsi que des exemples concrets d’utilisations industrielles de différentes
tailles sont aussi exposés dans des domaines tels que l’avionique ou les
systèmes manufacturiers.