proposition d'ARC locale

Ctrl-a

Programmation par aspects et systèmes réactifs

mai 2003


Nous nous intéressons aux relations entre d'une part, les systèmes réactifs, pour lesquels nous disposons de langages à la sémantique formellement bien fondée dans les systèmes de transitions étiquetées, et d'autre part, la programmation par aspect, qui permet de concevoir des systèmes en dissociant la spécification de différents aspects ou vues, pour obtenir le système résultant par une opération de tissage. Un sujet innovant consiste à considérer les aspects dans le cadre des systèmes réactifs, ce qui permet d'enrichir les langages réactifs et les fonctionnalités offertes à leurs utilisateurs, et aussi de proposer dans ce cadre spécifique une définition formelle des aspects, sur laquelle fonder des outils automatisés de tissage.

Dans le domaine de la programmation sûre des systèmes embarqués, combiner modularité de la conception et outils formels est difficile. L'approche peut faire avancer l'utilisabilité des méthodes formelles par des non-spécialistes, en l'intégrant dans un processus de compilation ou synthèse.

La proposition d'ARC regroupe les équipes POP ART de l'INRIA et synchrone de VERIMAG (ce qui concrétiserait des contacts jusqu'ici très informels).


Thème scientifique

Les systèmes réactifs auxquels nous nous intéressons sont des systèmes embarqués critiques, comme ceux que l'on trouve dans l'avionique, le transport terrestre, ou le nucléaire. Ces systèmes sont, d'une part intrinsèquement complexes, d'autre part soumis à des contraintes de qualité très fortes. Leur programmation demande des langages dédiés offrant des constructions adéquates pour l'expression de la réactivité et du parallélisme. Leur validation ne peut être que statique, car un défaut en cours d'exploitation, même s'il est détecté, ne peut en général pas être réparé.

La programmation dite synchrone des systèmes réactifs embarqués critiques (langages Esterel à Sophia-Antipolis, Signal à Rennes, Lustre à Grenoble) a apporté des techniques formelles, et des outils automatisés de validation et génération de code. Ces langages sont utilisés en vraie grandeur, dans des contextes industriels critiques, par exemple par Airbus. La définition formelle d'un langage synchrone s'accompagne d'un ensemble d'outils de validation et transformation (génération de tests, vérification, synthèse de contrôleurs, etc.) qui exploitent la sémantique formelle du langage et manipulent différentes sortes de modèles internes (systèmes d'équations, automates interprétés, etc.). La compilation d'un langage synchrone comporte une phase amont de production d'une telle forme interne, à partir de styles de langages assez différents (flot de données textuel ou graphique en Lustre et Signal, impératif textuel ou automates graphiques en Esterel). Les outils aval de production de code ou de validation, qui manipulent ces formes internes, sont en revanche assez comparables. Il existe donc dans ce cadre un consensus clair sur les bons modèles sémantiques pour la programmation des systèmes réactifs.

La programmation orientée aspects s'intéresse de manière très générale à des démarches de programmation dans lesquelles on identifie une architecture logicielle de départ propre et modulaire, et des aspects dont l'implémentation exige en quelque sorte de casser cette modularité, parce qu'ils sont complètement transversaux à la structure de départ. La programmation par aspect propose :

Les techniques de tissage peuvent être vues comme des techniques particulières de transformation de programme. La communauté aspects s'intéresse principalement aux problèmes d'expressivité, d'application et d'implémentation des aspects, et peu à une formalisation de l'approche.

Notre intérêt est d'exploiter leur potentiel d'interactions. La programmation des systèmes réactifs met en évidence de nombreux cas qui relèvent des préoccupations de la programmation par aspects : reconfiguration dynamique pour la tolérance aux pannes ; adaptation du comportement en fonction de politiques de gestion de qualité et de consommation des ressources ; réalisation de propriétés de sûreté globales, etc. Pourtant nous ne connaissons pas d'approches pour la prise en compte d'aspects dans la programmation réactive. Tous les cas cités ci-dessus sont envisagés indépendamment les uns des autres, et reçoivent des solutions particulières.

Une confrontation des besoins du domaine réactif avec les approches générales de la programmation par aspects pourrait permettre d'identifier une classe de problèmes exprimables de manière similaire, et traitables à l'aide des mêmes outils. En outre, il y a bien sûr de nombreux travaux sur la programmation sûre des systèmes réactifs, avec des approches basées sur des techniques de vérification formelle. Mais l'approche ``programmation par aspects'' aurait l'intérêt de conduire plutôt à la correction par construction.

Enfin les approches de programmation par aspects se préoccupent peu de sémantique. La communauté aspects s'intéresse principalement aux problèmes d'expressivité, d'application et d'implémentation des aspects. Si les langages d'aspects existants (e.g. AspectJ) sont extrêmement expressifs, ils fournissent en revanche très peu de garde-fous. Il est très délicat de raisonner sur les programmes et de contrôler l'impact sémantique du tissage. De plus, pour des raisons historiques, la majorité des travaux se place dans des modèles objets complexes (e.g. Java). Il y est difficile d'établir les fondements théoriques qui font défaut à la programmation par aspects. Se placer dans un cadre plus spécialisé comme les langages réactifs devrait permettre d'éviter ces problèmes. En cela, notre proposition est nouvelle, et différente des autres travaux sur la programmation par aspects.


Objectifs recherchés

L'objectif de ce projet est d'étudier précisément l'idée originale de programmation par aspects des systèmes réactifs, appuyée sur des modèles formels à base de systèmes de transitions étiquetés. Cela recouvre plusieurs thèmes, articulés comme suit :

Partenaires

équipe POP ART, INRIA Rhône-Alpes

Le thème de l'équipe est le contrôle-commande sûr; les activités concernent divers aspects de la génération automatique d'exécutifs temps-réel corrects, sur la base de modèles formels à base de syst\`emes de transitions étiquetées. Nous nous intéressons aux différentes utilisations de ces modèles, et surtout aux utilisations automatisées relevant de la compilation, de la génération de mises en oeuvre distribuées et/ou tolérantes aux pannes, et des applications de la synthèse de contrôleur.

Sur ce dernier point, on s'intéresse à mettre sur pied des méthodologies d'utilisations de cette technique qui ne requièrent pas de la part des utilisateurs de compétences formelles pointues. La généralisation de ce thème dans une approche langage est une des perspective les plus prometteuses. Cette proposition d'ARC s'inscrit dans cette droite ligne. Elle est liée à des contacts existants avec les projets VERTECS (H. Marchand) et LANDE (P. Fradet) à l'IRISA/INRIA-Rennes.

équipe synchrone, laboratoire VERIMAG

Le laboratoire VERIMAG s'intéresse au développement sûr des systèmes embarqués critiques. Pendant les 10 dernières années, Verimag a contribué activement au développement de l'état de l'art en langages synchrones, vérification (model-checking), test, et modélisation des systèmes. Les résultats trouvent de nombreuses applications industrielles, notamment dans des outils pour le développement des logiciels et systèmes embarqués.

F. Maraninchi travaille depuis longtemps sur les problèmes ``langage'' dans l'approche synchrone~: définition d'extensions de Lustre (programmation multi-langages, automates de modes), débogage, prise en compte de la structure des programmes pour la preuve, etc.) K. Altisen a rejoint récemment l'équipe synchrone. Son travail de thèse concerne l'ordonnancement d'un système temps-réel en utilisant des techniques de synthèse de contrôleur.


Importance et impact pour les partenaires

Le sujet est important pour POP ART en ce qu'il entame concrètement la généralisation dans une approche langage de l'axe génération de contrôleurs sûrs.

Cette ARC locale serait l'occasion d'une toute première officialisation de la coopération qui a démarré informellement entre POP ART et VERIMAG, notamment à l'occasion du post-doc de Karine Altisen en 2002.

On notera par ailleurs que nous souhaitons démarrer à cette occasion des contacts avec d'autres laboratoires Grenoblois autour de ce thème.


Programme de travail

Étude comparée des techniques Missions dans les workshops et conférences sur les sujets utiles, systèmes réactifs et programmation par aspects, et en visite dans des équipes d'experts du domaine; Rédaction d'une synthèse de l'état de l'art.

Des contacts seront donc pris avec d'autres équipes s'intéressant à la programmation par aspects sous d'autres angles, plus généraux que notre biais systèmes réactifs, ou plus proches de l'opérationnel que du formel. Nous pensons notamment localement au projet SARDES et à l'équipe ADELE du LSR. Sur des aspects sémantique des langages de programmation, ce thème intéresse aussi Sylvain Boulmé de l'équipe VASCO du LSR.

Proposition d'un cadre formel pour la programmation par aspects des systèmes réactifs Proposition d'un cadre de définition formelle des aspects et du tissage dans ce cadre restreint; caractérisation d'exemples typiques d'aspects.

Démonstrations de faisabilité Traitement d'exemples et études de cas, en utilisant les outils synchrones selon adéquation.


Ressources demandées

durée : 1 an

budget : 8 kEUR