Présentation de la Méthode B

Sommaire

B pour la conception de systèmes et logiciels prouvés

Validation B est une méthode de spécification formelle qui permet, grâce à un langage adéquat, d'exprimer très rigoureusement les propriétés exigées dans un cahier des charges. Il est alors possible de prouver de manière automatisée que ces propriétés sont non ambiguës, cohérentes et non contradictoires. Cela nous permet de garantir ensuite par preuve mathématique que ces propriétés sont respectées au fur et à mesure des étapes de conception.

Ainsi, cette méthode et la preuve qui lui est associée permettent :

d'obtenir des spécifications techniques et des cahiers des charges système clairs, structurés, cohérents, et sans ambiguïté,
de développer des logiciels garantis contractuellement sans défaut,

dans des domaines tels que le temps réel, les automatismes industriels, les protocoles de communication, les protocoles cryptographiques, l'informatique embarquée...

La Méthode B

La "méthode B" évoque traditionnellement l'ensemble comprenant : le langage B, le raffinement, la preuve, et les outils associés.

Un développement B débute par l'écriture d'un modèle concret, reprenant tous les aspects du besoin. Les principales données sont manipulées par le système sont décrites ainsi que les propriétés fondamentales de ces données. Des services assurent les transformations de ces données tout en préservant leurs propriétés. Le modèle B ainsi obtenu constitue une spécification de ce que devra réaliser le système.

Le modèle B est ensuite transformé (raffiné dans le vocabulaire B), jusqu'à obtenir une implantation logicielle complète du logiciel.

Au final, nous aboutissons alors à un modèle concret, prouvé et sans défaut, transcodable dans le langage C ou Ada.

La méthode B est donc : "une démarche de construction prouvée (dite correcte), sur la base du langage B, du raffinement et de la preuve".

Objectifs de la Méthode B

Inventée par Jean-Raymond Abrial, la méthode B est avant tout une nouvelle approche permettant de spécifier et concevoir des logiciels en s'assurant de leur sûreté ainsi que de leur fiabilité. Ainsi, l'ensemble des processus de spécification, de conception et de codage sont entièrement basés sur la réalisation d'un certain nombre de preuves mathématiques.

Ce n'est qu'après avoir prouvé mathématiquement un modèle qu'il est alors jugé cohérent et sans défaut.

Au final, cette méthode a pour principaux objectifs :

de réaliser des logiciels corrects par construction
de modéliser des systèmes dans leur environnement
de formaliser les spécifications
de simplifier la programmation

Diffusion de la Méthode B

Reconnue pour son efficacité, la méthode B est largement diffusée et reconnue dans le monde industriel et universitaire. Elle permet d'agir dans des secteurs variés, tels que le transport ferroviaire, l'aéronautique, la Défense, ou encore la Recherche et le Développement (R&D).

Si le succès de la méthode B est grandissant, cela s'explique en premier lieu par la diffusion d'outils majeurs, tels que l'Atelier B, un outil industriel permettant une utilisation opérationnelle de la méthde B pour des développement logiciels prouvés.

ClearSy en assure le développement avec des outils comme l'Atelier B, en collaboration avec des industriels, des centres de recherche et Jean Raymond ABRIAL.

Utilisateurs de la Méthode B

Les utilisateurs de la Méthode B sont souvent issus de milieux divers et variés. Parmi eux, nous pouvons compter :

Des industriels : ils cherchent des systèmes sécuritaires faisant appel aux méthodes formelles, ainsi que de nouvelles technologies pouvant répondre à leur besoin.
Des donneurs d'ordre : ils cherchent des réponses à leurs questions fonctionnelles et voient en la Méthode B une solution durable.
Des experts et spécialistes :individus cherchant des informations sur les méthodes formelles à un niveau hautement technique
Des chercheurs spécialisés en R&D : ils agissent pour un développement durable des méthodes formelles afin de développer de nouvelles solutions pour le futur.
Des enseignants universitaires et chercheurs : ils enseignent B dans le milieu académique et étudient les évolutions possibles des méthodes formelles.
Des élèves :composés de chercheurs ou tout simplement d'élèves souhaitant utiliser les outils B.

La Méthode B et ses Outils

Parmi les outils B majeurs, nous pouvons citer :

	Atelier B Outil industriel permettant l'utilisation opérationnelle de la méthode B pour des développements logiciels prouvés. Une formation est disponible pour comprendre, et pratiquer B.

	CompoSys Outil de conception formelle d'architecture système.

	Brama Outil de conception formelle d'architecture système.