Jonathan Julou : Mix DSL et Méthode B pour la preuve et l'exécution d'un algorithme d'inférence de modèles

De Ensiwiki
Aller à : navigation, rechercher
Cornues.png
Titre du projet Mix DSL et Méthode B pour la preuve et l'exécution d'un algorithme d'inférence de modèles
Cadre IRL

Labo LIG
Équipe VASCO
Encadrants Akram Idani et Roland Groz



Liens utiles

Le rapport est disponible ici: Fichier:Rapport IRL julouj.pdf

Gitlab contenant les sources du projet : https://gricad-gitlab.univ-grenoble-alpes.fr/julouj/irl


Introduction

Cette IRL a consisté à appliquer la méthode B à un algorithme d'inférence de modèles. Ce fut donc une introduction a ces deux domaines.

Inférence de Modèles

L'inférence de modèles est une branche du machine learning cherchant pour un système à en obtenir un modèle approché en observant son comportement.

Cela prend tout son sens par exemple dans le cas où on cherche à analyser un système qui comporte des "boites noires", des composants dont on ignore la nature, mais pour lesquels on peut obtenir des traces d'entrées-sorties. Dans les faits, ces boites noires peuvent être des composants au fonctionnement flou, mal documentés, ou encore des composants extérieurs qui peuvent intéragir avec le système. Cet exemple est un des principaux axes d'étude de l'équipe VASCO.

Méthode B

La méthode B est un processus de développement formel centré autours du langage de programmation B. L'objectif est de pouvoir concevoir une spécification du logiciel que l'on veut développer, et en tirer un programme informatique qui découle directement des spécifications.

Le principe général est d'écrire une machine B de très haut niveau, dite abstraite, qui spécifie notamment toutes les contraintes que doit respecter le logiciel. Elle est ensuite raffinée, c'est à dire que des machines B de plus en plus concrètes sont codées de sorte a respecter les contraintes de la machine abstraite. A la fin, si on a suffisamment raffiné, il est possible d'automatiquement traduire le code B en code compilable par une transformation prouvée correcte, et ainsi obtenir un logiciel utilisable. Le but est de pouvoir relier chaque raffinement à la machine abstraite par une preuve de consistance.

Cela se fait au moyen d'un invariant: un ensemble de propriétés qui doivent être vérifiées tout au long du programme (un peu comme un invariant de boucle dans sa boucle !). Le logiciel AtelierB permet de faire ces preuves statiquement et automatiquement.

On utilise aussi ProB, qui peut animer des machines B, ce qui revient à les executer alors qu'elles ne sont pas finies. Cela permet de comparer plus pratiquement le résultat intermédiaire aux spécifications.


Motivations

l’outil Meeduse, développé par Akram Idani, est un plugin de l’Eclipse Modelling Framework qui permet de faire des preuves formelles sur des langages dédiés (Domain Specific Languages, ou DSL), tout en ayant une fonctionnalité d’animation pas à pas du DSL sur un exemple. Pour cela, on spécifie le DSL dans un langage usuel pour cela (on a utilisé Xtext pendant l'IRL), puis il est traduit en machine B. Ensuite Meeduse peut se connecter à ProB pour animer le modèle. On peut bien sûr aussi prouver le code B généré, et le raffiner.

La majeure partie de l’IRL aura consisté à essayer d’adapter un algorithme d’inférence demodèles en B, pour être utilisable dans Meeduse et avoir des garanties simples sur l’éxecution.

Algorithme étudié

L’algorithme d’inférence de modèles auquel on s’intéresse s’appelle Minimally Adequate Synthetizer(MAS). Il a été décrit par Mäkinen et Systä (https://dl.acm.org/doi/pdf/10.5555/381473.381475). Il s’applique dans le cas où on veut modéliser un système pour lequel on peut facilement obtenir des diagrammes de séquence, afin d’en tirer un automate décrivant le système.

Un diagramme de séquence est un ensemble de lignes de vie, une par composant du système, entre lesquelles on peut placer des messages que s’échangent les composants.

En sortie, on obtient un diagramme état-transition de Harel [7]. Il s’agit d’une extension par rapport aux automates état-transition classiques (machines de Moore ou de Mealy notamment) ajoutant la notion de hiérarchie, de communication, et d’exécution concurrente.

MAS est basé sur un algorithme plus simple, L*, qui infère des automates finis déterministes reconnaissant un langage inconnu.

Pour ces deux algorithmes, l'inférence est active, c'est à dire que l'algorithme interagit avec le système que l'on veut modéliser en lui posant des questions, par opposition à une inférence passive sur une base de données d'exemples.

Type de travail réalisé

Cette IRL a eu une très importante composante bibliographique. Il a notamment fallu beaucoup de temps pour comprendre le fonctionnement de MAS.

Au delà de cela, j'ai exploré diverses pistes d’implémentation de L* et de MAS en B.

Résultats

Au final, on a quelques prototypes en B à la fois pour L* et MAS.

Par exemple pour l'entrée:

Exemple inspiré de la domotique, avec une personne intéragissant avec plusieurs objets. On veut modéliser l'humain

L'implémentation de MAS obtient en sortie:

Diagramme état-transition de Harel obtenu avec l'implémentation de MAS réalisée pendant l'IRL

Les machines B en l’état ne sont très probablement pas utilisables pratiquement, mais les solutions trouvées pour implémentées certaines parties non-triviales des algorithmes pourraient servir de base à une meilleure version. Il y a aussi quelques bugs connus qui sont expliqués dans le rapport.

Au final, la partie preuve a été négligée pour se concentrer sur l’obtention d’un algorithme fonctionnel.