Méthode B

La méthode B a pour ambition de fournir un cadre rigoureux à la construction de logiciels. Elle vise plus particulièrement les logiciels pour lesquels certaines propriétés importantes, voire critiques, exprimées au plus haut niveau de la spécification, doivent être garanties. Pour cela, elle s'appuie sur des notions logiques de la théorie des programmes et elle est instrumentée par un ensemble d'outils intégrés. C'est cette association : bases mathématiques solides et outils industriels, qui en font une méthode utilisable pour la réalisation, en vraie grandeur, de logiciels sécuritaires. Des applications variées de cette méthode, réalisées par des équipes industrielles sont ici présentées. La méthode B n'est pas uniquement destinée à réaliser des développements complets et prouvés (bien qu'elle soit la seule méthode formelle à pouvoir le faire), mais elle peut être utilisée à divers stades d'un projet informatique et notamment lors de la définition des besoins. Le lecteur découvrira que les recherches sur ce sujet sont très actives et que des avancées sont possibles pour améliorer la méthode et les outil