Langages et Atelier Intégré pour le Développement de Composants Embarqués Sûrs Ce projet est une ACI "Sécurité & Informatique"

Au menu Accueil / Home Participants Liens / Links Réunions Paris, ma. 07 Grenoble, ju. 06 Grenoble, sep. 05 Paris, mai 05 Grenoble, fév. 05 Paris, oct. 04 Documents Rapport à mi-parcours (html) (pdf) Poster présenté aux journées PaRI-STIC, nov. 2006 (format a4) (format a1) Publications

Lutin, un langage de modélisation de l'environnement Les systèmes embarqués sont généralement destinés à entretenir une interaction continuelle avec leur environnement. Dans le cadre d'un atelier intégré de développement et de simulation, il est donc nécessaire de pouvoir décrire et simuler ces environnements. Les environnements sont généralement indéterministes, mais pas quelconques : ils sont connus par des propriétés de haut niveau que toute simulation réaliste doit satisfaire. Une solution pour décrire les environnements serait d'utiliser des langages de programmation réactive (comme Lustre) en leur rajoutant des primitives pseudo-aléatoires pour simuler l'indéterminisme. Cette démarche n'est cependant pas très satisfaisante, car la distance est souvent très grande entre les spécifications de haut niveau de l'environnement et un programme concret sensé les simuler. C'est pourquoi Verimag suit la démarche inverse qui consiste à proposer des formalismes de description intrinsèquement indéterministes [19]. Plus précisément, Verimag érudit : un modèle exécutable simple, basé sur des automates finis et des relations d'entrées/sorties, un langage de haut niveau, «user-friendly », proposant des structures de contrôle sophistiquées et pouvant être compilé dans le modèle exécutable. Dans le modèle de base, Lucky, le comportement est décrit par un automate fini indéterministe dont les transitions représentent les réactions atomiques. Chaque transition est étiquetée par : une relation entre les variables d'entrée/sortie qui doit être satisfaite au cours de la réaction ; par exemple, soit x une entrée et a une sortie, x and (0.0 < a) and (a > 10.0) stipule que x doit être vraie et a comprise entre $0$ et $10$. Dans une telle relation, les entrées, qui sont fournie par le système embarqué, sont incontrôlables. Il peut donc arriver que la relation soit insatisfiable, auquel cas la transition est irréalisable (c'est le cas dans l'exemple quand x est fausse) ; un poids, c'est-à-dire une indication numérique représentant la probabilité relative de prendre cette transition plutôt qu'un transition concurrente (une transition réalisable de poids $3$ a $3/2 = 1,5$ fois plus de chance d'être choisie qu'une transition réalisable de poids $2$). L'algorithme de simulation est assez simple : dans un état courant, une transition est élue parmi toutes celle qui sont réalisables, en tenant compte de leurs poids relatifs. La contrainte associée est alors résolue et une solution particulière est choisie pour être envoyée au système embarqué. Si aucune transition n'est réalisable, l'exécution stoppe, sinon, elle continue à partir de l'état but de la transition. Le modèle d'automate de Lucky est suffisamment riche pour décrire des comportements complexes. Cependant, programmer directement en automate explicite devient vite rédhibitoire. C'est pourquoi un langage de plus niveau est proposé. Les bases de ce langage, Lutin, sont présentées dans [20]. Comme dans Lucky, les atomes sont des réactions atomiques indéterministes, mais la structure de contrôle est construite à partir d'instructions inspirées par les expressions régulières : séquence, choix indéterministe et boucle indéterminée. La nouvelle version du langage, développée dans le cadre d'Alidecs, est enrichie de nouvelles structures de contrôle : exécution concurrente, levée et interception d'exceptions. Le langage est aussi enrichi d'un couche fonctionnelle pour permettre une programmation modulaire. L'utilisateur peut par exemple construire et réutiliser ses propres structures de contrôle adaptées.