Raffinement automatique

Le raffinement est au cœur de la méthode B. Il permet de ne considérer dans un premier temps que l’abstraction d’un logiciel avant de prendre en compte les détails de conception et d’implémentation.

PRÉSENTATION RAFFINEMENT AUTOMATIQUE

Le raffinement est au cœur de la méthode B. Il permet de ne considérer dans un premier temps que l’abstraction d’un logiciel avant de prendre en compte les détails de conception et d’implémentation.
L’automatisation du raffinement permet d’accélérer le développement d’un logiciel en confiant à un outil la transformation mécanique d’un modèle abstrait complet en un modèle implémentable.

Un tel outil, appelé raffineur automatique, transforme une machine en un ensemble de machines, raffinement et implémentations à l’aide d’un ensemble de règles de transformations appelées règles de raffinement.

Le processus de raffinement automatique se décompose alors en un grand nombre de petites transformations (qui conduisent à des obligations de preuve plus simples à prouver).

De manière historique, le premier raffineur automatique pour B a été développé par Matra Transport et utilisé à de nombreuses reprises pour développer des logiciels de sécurité par exemple :

• Pour les métros de Caracas,
• New York (Carnarsie Line),
• La navette automatique de l’aéroport Charles de Gaulle.
• Un autre raffineur automatique, BART B (B Automatic Refiner Tool), a été développé à l’occasion du projet ANR Rimel, puis intégré à l’Atelier B.

Le processus de raffinement est interactif :
L’outil applique les règles de raffinement de manière récursive et s’arrête lorsque aucune règle ne permet de raffiner une variable ou une substitution. L’utilisateur de l’outil doit alors ajouter une règle de raffinement à la base de règle, en créant une de toute pièce ou en adaptant une règle existante. Ce processus se répète jusqu’à ce que la machine cible soit complètement raffinée.
Ni l’outil, ni les règles de raffinement ne doivent subir de validation : les modèles générés doivent être prouvés par la suite – s’ils sont erronés, la preuve ne pourra pas être couronnée de succès.

 

LES AMÉLIORATIONS

– Le processus de raffinement automatique peut induire des conflits lors du raffinement de variables qui peuvent nécessiter d’être à la fois abstraite et implémentée. Les algorithmes du moteur de raffinement automatique ne traitement pas de manière efficace ce genre de situations et les situations de conflit doivent être résolues par l’utilisateur, en modifiant/ajoutant des règles de raffinement ad-hoc. L’automatisation des procédures de résolution de conflit fait l’objet d’un stage.