S'appuyant sur une expression en Signal des différentes versions
d'un système en cours de conception, la méthodologie que nous développons
consiste en l'application d'une série de transformations de descriptions
respectant le schéma suivant :
- spécification, conception et vérification de l'application
indépendamment de l'architecture cible, grâce à l'hypothèse de
synchronisme et au non-déterminisme permettant de fournir un modèle
du comportement de l'environnement;
- affinement progressif vers l'implémentation (conception détaillée
incluant le partitionnement) guidé par des simulations/vérifications
à différents niveaux; à cette étape, la cible est une architecture
logicielle pouvant être vérifiée et évaluée;
- implantation effective du schéma d'exécution obtenu sur des
architectures éventuellement asynchrones et distribuées, en relâchant
au besoin l'hypothèse de synchronisme (tout en restant dans le
cadre du modèle synchrone), et en garantissant une implémentation
correcte;
- génération de code exécutable, de composants matériels ou de
composants hybrides matériels/logiciels.
Nos activités de recherche concernent les différentes étapes de
ce schéma de conception. Comme certaines de ces activités concernent
plusieurs de ces étapes, nous distinguons ici, pour une meilleure
lisibilité, les thèmes suivants : description d'applications,
étude des propriétés des processus synchrones, méthodes et outils
pour la conception d'architectures de mise en oeuvre, développements
et expérimentations.
Description d'applications
La description d'une application, tant au niveau de la spécification
que de la conception, suppose l'existence d'un langage suffisamment
expressif pour les classes d'applications visées; la réduction des
ruptures dans le cycle de conception est favorisée par le support
logiciel des traitements dans une sémantique homogène. Les études
portant sur l'augmentation du pouvoir d'expression du langage Signal
ont pour but d'étendre le domaine d'application des techniques synchrones,
soit par la définition de relations sémantiques entre les formalismes
synchrones et d'autres formalismes, soit par l'adjonction de nouvelles
primitives ou de nouveaux concepts dans le langage lui-même.
- Avec la société TNI qui commercialise Sildex,
un environnement de programmation fondé sur Signal, nous avons
travaillé à la définition d'une nouvelle version (V4)
dont l'une des principales extensions porte sur la modularité,
qui requiert de nouvelles techniques de compilation ;
- Nous travaillons, sur le plan théorique, à la définition d'un
nouveau cadre pour le typage de processus synchrones prenant en
compte des abstractions de comportements (calcul d'horloges);
ce travail, qui s'inscrit dans une perspective de définition de
la mobilité en Signal, prolonge les travaux entrepris
sur le thème de la compilation séparée.
- Entreprises initialement dans le cadre d'un ancien projet avec
les Laboratoires de Marcoussis, les études sur les liens entre
le paradigme objet et le modèle synchrone trouvent un nouvel élan
dans les travaux auxquels nous participons sur la conception de
BDL; BDL est un formalisme reposant
sur le modèle synchrone pour la spécification de comportements
d'objets.
Le format commun de la programmation synchrone ( DC+)
résulte de travaux menés depuis plusieurs années, tout d'abord par
les équipes françaises dans lesquelles ont été conçus les langages
synchrones Esterel, Lustre et Signal au sein du groupement C2A,
puis dans le cadre d'un projet européen Eureka (Synchron), et actuellement
dans le cadre des projets européens LTR Syrf et R&D Sacres.
La définition de ce format a été décidée en vue de favoriser le
partage de logiciels issus de la communauté synchrone, mais aussi
de permettre une large ouverture vers d'autres formalismes en amont,
et d'autres outils, latéralement et en aval.
Le projet européen Sacres a précisément pour objectif de développer
un environnement de conception multi-formalisme synchrone à destination
des applications critiques enfouies; outre les études sur le format
lui-même, nous y conduisons des travaux sur la traduction de
Statemate en DC+. Une étude comparable concerne
la modélisation et traduction des langages de programmation d'automatismes
industriels de la norme IEC 1131.
Étude des propriétés des
processus synchrones
Un programme Signal décrit le comportement d'un système de transitions
dont divers formalismes permettent d'étudier les propriétés.
Jusqu'à une période récente, nos travaux sur ce thème ont porté
essentiellement sur une modélisation des comportements par des systèmes
dynamiques polynomiaux sur les entiers modulo 3 (permettant
le codage des booléens et de l'absence d'occurrence d'un signal
à un instant donné). Un système de calcul symbolique (Sigali) a
été développé dans ce cadre. C'est dans ce système que sont maintenant
étudiées des techniques de synthèse de contrôleurs, techniques
utilisables pour affiner des spécifications, pour aider à la conduite
de postes de commandes, voire à la génération automatique de tests.
Les systèmes dynamiques permettent d'analyser (partiellement)
les trajectoires des processus dans un ensemble d'états résultant
de la combinaison de variables du programme Signal. Cet ensemble
lui-même est l'objet, dès la compilation, de calculs qui reposent
sur une représentation par hiérarchie de BDD (appelé
calcul d'horloges [TPA95]). Ces calculs sont utilisés en particulier pour effectuer
des transformations de programmes en vue de vérification,
de distribution et de génération de code.
Une approche plus classique pour l'étude des propriétés des programmes
consiste en la génération d'un automate fini qui peut alors être
fourni à des outils de vérification automatique largement développés
et utilisés dans la communauté. Nos travaux portent notamment sur
la génération d'automates prenant en compte la hiérarchie
des horloges, et sur des méthodes de réduction et de comparaison.
Des approches complémentaires pour la vérification de propriétés
sont fournies par les techniques d'interprétation abstraite,
permettant la prise en compte de signaux numériques, par exemple,
et d'autre part par la démonstration interactive de théorèmes.
Les applications temps réel enfouies peuvent être mises en oeuvre
sur des systèmes d'exploitation temps réel offrant différents mécanismes
de gestion de tâches [ER94], incluant éventuellement la préemption. Pour bien comprendre
les effets de ces systèmes d'exploitation sur les mises en oeuvre
obtenues des programmes synchrones, il est important de disposer
d'un cadre sémantique intégrant des primitives de préemption
dans les langages synchrones.
Méthodes et outils pour la conception
d'architectures de mise en oeuvre
La définition de l'architecture supportant l'application temps
réel peut comporter différentes classes de composants comme des
processeurs standards, des DSP, des Asics, etc.,
et c'est donc dans la perspective de mise en oeuvre sur de telles
cibles hétérogènes que nous inscrivons aussi bien nos études sur
la conception détaillée et le codage que des activités relevant
de la conception conjointe matériel/logiciel.
Une première recherche conduite en coopération avec le projet
Api et le soutien du Cnet vise à construire un cadre théorique homogène
pour la conception d'applications comportant à la fois du calcul
régulier et des parties de contrôle irrégulier. Le problème posé
est alors celui de l'interface logiciel/logiciel ou logiciel/matériel
entre ces deux composantes de l'application; nous l'abordons par
l'introduction de fonctions affines sur des horloges, permettant
de transformer un traitement global instantané (par exemple un produit
de matrices) en une succession de communications (de vecteurs ou
d'éléments) avec un opérateur spécifique (par exemple systolique).
Le problème du partitionnement d'un programme flot de données
synchrone est abordé en s'attachant aux propriétés structurelles
du graphe de l'application; supposant donnée une répartition du
code sur une architecture cible (cette répartition peut résulter
d'algorithmes d'optimisation ou être explicitée comme spécification
non fonctionnelle, par exemple pour des raisons de traçabilité),
nous nous proposons de produire, par des transformations locales
à chaque composant de cette architecture, à la fois le code pour
ces composants et les protocoles de communication à mettre en oeuvre.
Cette mise en oeuvre peut être «Globalement Asynchrone Localement
Synchrone» (GALS). Le cadre théorique de nos recherches permet de
caractériser des mises en oeuvre synchrones ou partiellement désynchronisées
en terme de préservations de propriétés de flots, d'ordres partiels,
de taille mémoire, par rapport au programme initial.
Pour la génération de composants matériels ou de code exécutable
sur un processeur programmable, l'approche que nous adoptons est
là encore celle de la transformation de programmes conduisant à
une expression en Signal aussi proche que possible de la structure
du code cible (C ou VHDL actuellement). Cette approche
diminue les risques d'incorrection liés au passage à un autre langage.
Elle est accompagnée d'études sur la modélisation synchrone de
composants matériels en vue du prototypage rapide de circuits spécifiques,
qui participent à l'activité grandissante du projet sur le thème
de la conception conjointe matériel/logiciel.
Dans l'approche synchrone, les durées d'exécution ne sont pas
directement prises en compte. La prise en compte de ces durées,
nécessaire à la vérification de la correction de la mise en oeuvre
en regard des contraintes temps réel, est effectuée en considérant
une interprétation qui, à un programme synchrone et une architecture
donnée, associe un programme synchrone sur nombres entiers; l'image
du programme initial modélise les durées d'exécution de la mise
en oeuvre. On peut alors simuler le programme image ou chercher
à utiliser des techniques analytiques, comme par exemple celles
qu'offre l'algèbre MaxPlus.
Développements et expérimentations
Les travaux théoriques conduits dans le projet aboutissent à des
prototypes mettant en oeuvre les algorithmes conçus au cours de
ces études. Nous nous efforçons de conserver et diffuser ce savoir-faire
du projet par une intégration dans un environnement de conception
construit autour du langage Signal. Une section est consacrée à
la présentation de ce logiciel.
Des expérimentations sont conduites pour valider les algorithmes
en relation avec des industriels. Elles concernent également la
diffusion des principes synchrones par des développements donnant
à des formalismes divers une traduction en Signal. Enfin l'étude
d'applications en coopération avec des industriels ou des projets
académiques est une source importante des problèmes nouveaux que
traite le projet EP-ATR.
|