Présentation de la Méthode B
B POUR LA CONCEPTION DE SYSTÈMES ET LES LOGICIELS PROUVÉS
La méthode 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 formelle et la preuve qui lui est associée permettent :
1- D’obtenir des spécifications techniques et des cahiers des charges système clairs, structurés, cohérents et sans ambiguïté,
2- De développer des logiciels garantis contractuellement sans défauts,
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 FORMELLE B
Un développement B débute par l’écriture d’un modèle abstrait, reprenant tous les aspects du besoin. Les principales données sont manipulées par le système et 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 formelle B est donc « une démarche de construction prouvée (dite correcte), sur la base du langage B, du raffinement et de la preuve ».
Le B événementiel est une spécialisation de la méthode formelle B, utilisée pour décrire formellement les systèmes, les événements qui viennent modifier atomiquement leurs états et raisonner mathématiquement sur leurs propriétés.
OBJECTIFS DE LA MÉTHODE B
Inventée par Jean-Raymond Abrial, la méthode formelle B est avant tout une nouvelle approche permettant de spécifier et concevoir des logiciels tout 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 preuve 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 les 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 formelle 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 cette méthode formelle B est grandissant, cela s’explique en premier lieur par la diffusion d’outils majeurs, tels que l’Atelier B, un outil industriel permettant une utilisation opérationnelle de la méthode B pour des développements logiciels prouvés.
CLEARSY en assure le développement avec des outils comme l’Atelier B, en collaboration avec des industriels et des centres de recherche.
VÉRIFICATION FORMELLE GÉNÉRALISÉE
La MÉTHODE B associée à d’autres formalismes est utilisée pour aider à analyser, valider, réorganiser et fournir les éléments qui permettent de compléter les spécifications et cahiers des charges. Cette technique d’analyse de fiabilité des systèmes a la particularité d’être applicable à tous les domaines industriels. La validation formelle est ainsi utilisée aujourd’hui avec succès dans les domaines automobile, bancaire, spatial et nucléaire.
UTILISATEURS DE LA MÉTHODE B
LES UTILISATEURS DE LA MÉTHODE B SONT SOUVENT ISSUS DE MILIEUX DIVERS & VARIÉS, PARMI EUX NOUS POUVONS COMPTER :
1- 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.
2- Des donneurs d’ordre : ils cherchent des réponses à leurs questions fonctionnelles et voient en la méthode B une solution durable.
3- Des experts et spécialistes : individus cherchant des informations sur les méthodes formelles à un niveau hautement technique
4- 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.
5- Des enseignants universitaires et chercheurs : ils enseignent B dans le milieu académique et étudient les évolutions possibles des méthodes formelles.
6- Des élèves : composés de chercheurs ou tout simplement d’élèves souhaitant utiliser les outils B.