Représentation de programmes SMALA grâce à la théorie des bigraphes

Dans le secteur aéronautique comme dans de nombreux autres, les humains interagissent avec des systèmes toujours plus nombreux et critiques, y compris pour leur sécurité. Un système interactif est manipulé par des humains et doit en réponse réagir de façon correcte, fiable voire certifiée. Un système interactif-reactif réagit aux entrées utilisateurs mais aussi à d’autres (issues de capteurs par exemple). La plupart des langages de programmation ne facilitent pas le passage de la phase de design à celles de conception, architecture et développement, compliquant la création de logiciels interactifs. Ce constat motive le développement de SMALA, un langage réactif [1] mettant l’accent sur l’aspect interactif des programmes. Il permet de décrire un programme à la manière des systèmes basés composant [2]. On y retrouve des entités qu’on peut composer et connecter entre elles afin de les coordonner. SMALA repose sur de larges bibliothèques de composants, notamment graphiques, développés en C++. Il est surtout utilisé pour concevoir des IHM pour l’aviation, comme l’interface du tableau de bord de l’hélicoptère électrique Volta [3]. Pour pouvoir utiliser un langage dans la conception de systèmes critiques il faut fournir des garanties sur l’exécution de ses programmes. Ainsi, nous envisageons de vérifier le compilateur de SMALA en commençant par s’assurer de la préservation des liens de causalité entre les entités. Pour cela, nous nous inspirons de l’approche des compilateurs Vélus [4] et CompCert [5] : nous implémentons et vérifions un compilateur SMALA grâce à l’assistant de preuve Coq. Pour l’instant, nous ignorons la partie graphique du langage. De plus, pour faciliter la vérification, nous travaillons avec SMALIGHT, un sous-ensemble de SMALA, couvrant ses principes de base et permettant de redéfinir les bibliothèques actuelles en C++.

Notre première définition formelle de ce sous-ensemble [6] a soulevé plusieurs problèmes. En effet, l’ensemble choisi était trop petit, ne permettant pas de couvrir tous les concepts de SMALA. De plus, l’expression de l’ordre d’exécution des entités du programme nécessitait l’introduction de trop nombreux paramètres, rendant les règles peu intuitives et difficiles à faire évoluer. De même que le lambda calcul est approprié pour définir les sémantiques opérationnelles de langages fonctionnels, nous voulons exprimer notre sémantique avec une théorie mathématique adaptée. La sémantique de SMALA est basée sur une double structure d’arbre et de graphe définissant les règles d’activation des entités du programme. Mais dans notre première approche, nous avons exprimé la priorité d’exécution avec une liste d’ensembles, compliquant la compréhension. Étant donnée la structure de SMALA, nous avons décidé d’utiliser la théorie des bigraphes pour formaliser la sémantique d’une version étendue de SMALIGHT. La capacité des bigraphes à modéliser et implémenter des langages de programmation a déjà été démontrée [7]. Ils ont ainsi été utilisés pour exprimer la sémantique du langage Kappa basé sur des règles d’interaction entre protéines [8]. Ici, nous utilisons la théorie des bigraphes pour modéliser la structure d’un programme SMALIGHT et les règles d’activation de ses éléments.

Réduction de SMALA en SMALIGHT

SMALA repose sur deux concepts : les processus et une notion de dynamicité.

Processus

Un processus est une entité qui a une sémantique et un état (Activé ou Désactivé). Si un processus est Activé, il s’exécute selon sa sémantique. S’il est Désactivé, il est inactif. De plus, un processus peut être persistant (son activation perdure jusqu’à la fin de l’exécution ou sa désactivation par un autre processus) ou transitoire (il s’exécute selon sa sémantique à l’activation puis se désactive immédiatement). Les processus de SMALA couvrent tous les aspects du langage : graphiques, interactifs, structures de contrôle, création de composants, gestion de l’activation et de la mémoire. Néanmoins, la plupart peuvent être vus comme la composition de processus plus élémentaires. Dans SMALIGHT, nous visons à identifier l’ensemble minimal de ces processus permettant la redéfinition de tous les autres. Ainsi, actuellement, les processus de SMALIGHT (en omettant la partie graphique) sont :
— binding : processus persistant permettant à un processus p1 (le notifiant) de communiquer son état d’activation à un processus p2 (l’abonné). Ainsi, le binding p1 → p2 active p2 quand p1 s’active. Il en existe trois autres types :
➤ Le binding p1 →! p2 désactive p2 quand p1 s’active
➤ Le binding p1 !→ p2 active p2 quand p1 se désactive
➤ Le binding p1 !→! p2 désactive p2 quand p1 se désactive
— component : processus persistant correspondant à un contenant nommé. On appelle enfants les processus qu’il contient. Ils sont activés dans l’ordre de leur définition dans le code (figure 1a) lorsque le component est activé.
— spike : processus transitoire dont la sémantique est de ne rien faire. Il est généralement utilisé pour notifier ses abonnés d’un changement d’état.
— property : processus persistant encapsulant une valeur stockée en mémoire et notifiant ses abonnés lorsque cette valeur change. Il en existe de différents types mais SMALIGHT contient seulement les IntProperty pour l’instant, sur lesquelles on peut effectuer des opérations arithmétiques.
— assignment : processus transitoire noté =:. Ainsi, e1 =: p2 copie la valeur de l’expression e1 dans la property p2 lorsqu’il est activé.

La dynamicité

La notion de dynamicité dans SMALA couvre trois aspects : la propagation (seule traité pour l’instant), la mémoire et la création dynamique de processus. La propagation concerne toutes les modifications dues à des changements d’état de processus dans un programme SMALA. Ces propagations sont de deux types différents : celles issues des components et celles issues des bindings. La définition d’un component induit la création d’une relation hiérarchique avec ses enfants, représentée par un arbre (figure 1c). Si la racine change d’état, on propage ce changement aux enfants en parcourant les dans l’ordre de leur déclaration et récursivement. De plus, un enfant est Activé seulement si son parent l’est aussi. Un binding ou un assignment crée une relation entre les processus qui peut être représentée par un graphe orienté acyclique (figure 1b). Ainsi, si un processus source (i. e., n’ayant pas de prédécesseur) change d’état, ce changement est propagé aux autres processus du graphe en suivant un ordre total issu d’un tri topologique.

La théorie des bigraphes

La théorie des bigraphes, formellement définie par Milner [9], représente les relations et les interactions entre des entités grâce à un système réactif bigraphique consistant en une paire de graphes (graphe de places et graphe de liens, représentant respectivement l’imbrication des entités les unes dans les autres et leurs relations) appelée bigraphe et un ensemble de règles de réaction sur ce bigraphe. Le graphe de places (figure 2b) est une forêt d’arbres qui permet de décrire la localisation des nœuds et en particulier leur imbrication les uns dans les autres. La racine de ses arbres est une région (une entité qui peut en contenir d’autres mais ne peut être contenue; dans la figure 2a ce sont les rectangles blancs, dans la figure 2b, les racines) et leurs feuilles sont des nœuds ou des sites (une entité qui peut être contenue par une région ou des nœuds et pouvant être substituée par un graphe de places; dans la figure 2a, c’est le rectangle grisé et dans la figure 2b, la feuille ’0’). Les régions et les sites permettent de composer des graphes de places entre eux. Le graphe de liens (figure 2c) est un hypergraphe décrivant des relations entre entités par des hyperarêtes (arêtes connectant plusieurs nœuds). Ses nœuds ont des ports permettant aux arêtes de se fixer. Les arêtes brisées ont une extrémité non connectée et permettent la composition de graphes de liens (’e4’ en figure 2). Une règle de réaction R est une paire de bigraphes (G, D) ayant autant de sites, de régions et d’arêtes brisées. On la note R : G → D. Appliquer R à un bigraphe B consiste à remplacer une occurrence de G se trouvant dans B par D.

De SMALIGHT vers les bigraphes 

Nous avons choisi de représenter les règles d’activation d’un programme SMALIGHT en l’assimilant à un système réactif bigraphique. L’assignment et la property ne sont pas présentés ici. En effet, bien qu’ils possèdent un mécanisme de propagation d’activation, une part important de leur fonctionnement est liée à la mémoire qui n’est pas traitée dans cet article.

Représentation générique des processus

Nous proposons tout d’abord une représentation générique des processus de SMALIGHT qui nous permet d’appliquer les règles de réaction de façon efficace. Ainsi, un processus est représenté par un nœud Process. Il contient un ensemble de nœuds, possédant chacun un site, décrivant ses attributs (voir figure 3a). A ce stade, nous avons identifié 4 attributs qui suffisent pour décrire totalement n’importe quel processus de SMALIGHT. Ils sont décrits ici avec les conventions graphiques utilisées le cas échéant : un identifiant, (représenté si nécessaire par une police cursive), une sémantique (component, spike, etc. représentant un processus), un état (un nœud Activé est violet; Désactivé, il est bleu) et un type (transitoire est représenté par un losange, persistant par un hexagone). Nous ne représentons les ports que si la règle de réaction concerne le graphe de liens. Nous décrivons l’activation et la désactivation des processus par un ensemble de règles de réaction, afin de représenter l’exécution d’un programme SMALIGHT.

Instanciation sur les processus de SMALIGHT

Ces modèles généraux sont instanciés ici pour le component et le binding. Le spike est représenté comme un nœud Spike unique . La property et l’assignment, utilisant la mémoire pas encore traitée, ne sont pas présentés.

Le component

Le component est un processus qui en contient d’autres. On le représente par un nœud Component possédant un enfant Children contenant tous ses enfants. Pour activer un Component, et donc tous ses enfants, on doit connaître les processus restant à activer à chaque application d’une règle de réaction. De plus l’activation d’un enfant dépend de son type (transitoire ou persistant). Nous avons donc ajouté deux autres sites comme enfants de Component pour gérer cela. Ainsi, à l’activation d’un Component, ses enfants persistants sont déplacés dans un nœud Updated  et ses enfants transitoires dans un nœud Unchanged. Lorsque tous les nœuds ont été traités, le nœud Children est vide. On peut alors passer l’état du component à Activé et replacer l’ensemble des enfants dans le nœud Children.

Le binding
Le binding est représenté comme un nœud ayant deux enfants Source et Target. Chacun comprend un port qui le lie à un nœud Process correspondant au processus source, respectivement cible, du binding. Ainsi, les règles de réaction du binding → correspondent à la recherche de bindings dont le processus source est activé et le processus cible pas encore . Les autres bindings suivent le même principe.

Table des matières

I)INTRODUCTION
II) GENERALITES
III) METHODOLOGIE
IV) RESULTATS
V) COMMENTAIRES ET DISCUSSION
VI) CONCLUSION  
VII) REFERENCES
ANNEXES
RESUME

Lire le rapport complet