Sujets de DEA proposés dans l'équipe EP-ATR pour la rentrée 2000-2001

Interprétation de programme par fonction polynomiale sur intervalles

Encadreur : B. Philippe (Bernard.Philippe@irisa.fr), P. Le Guernic (Paul.Leguernic@irisa.fr).

Mots-clés : Interprétation abstraite, Intervalle, Polynômes

Stage en collaboration avec Aladin.

Le fonctionnement le plus sûr possible des systèmes critiques enfouis est évidemment une préoccupation majeure de leurs concepteurs, de leurs utilisateurs et des autorités en charge d'en autoriser le déploiement. Pour atteindre cet objectif différentes techniques sont utilisées allant de la validation du processus de conception à la vérification formelle en passant par le test. Les techniques de vérification formelle apportent l'assurance mathématique du respect par le système des propriétés vérifiées au prix d'algorithmes dont le coût deviendrait vite prohibitif sans l'utilisation de techniques d'interprétations abstraites. Ces techniques permettent d'approcher la fonction que réalise le système par des fonctions sur des domaines finis. Le langage Signal décrit le traitement effectué par le système sous la forme d'un ensemble d'équations explicites sur des données, en particulier réelles. L'objectif du stage est d'étudier une approximation d'un programme Signal en considérant pour les domaines de valeurs, des ensembles finis d'intervalles et pour les fonctions arithmétiques utilisées dans les expressions de définition des variables, une approximation par des polynômes dans les intervalles. Cette interprétation peut, comme toute interprétation, présenter l'inconvénient d'aboutir à des approximations trop grossières pour la vérification de certaines propriétés. Dans le domaine de l'analyse numérique, des techniques permettant d'éviter la décorrélation des expressions, et donc d'obtenir des interprétations plus fines ont été développées. La première partie du stage consistera à étudier ces techniques et leur application dans le contexte de la vérification, en considérant des polynômes sur une puis plusieurs variables. Dans ce contexte de vérification l'espace est représenté par une partition finie, qu'on appellera base d'intervalles, construite à partir d'un ensemble fini de constantes. La seconde partie du stage consistera à étudier les propriétés de stabilité des interprétations d'un programme sur différentes bases en vue de dégager des méthodes permettant de trouver des compromis entre précision et complexité. Selon les goûts et compétences du candidat, à cette seconde partie de nature mathématique pourra être substituée une application des résultats de la première partie à l'interprétation de programmes Signal oeuvre des résultats de la première partie de l'étude.

Références :

• O. Beaumont. Algorithmes pour les intervalles : Comment obtenir un résultat sûr quand les données sont incertaines. Thèse Université de Renneqs 1, 12 janvier 1999.
• M. Daumas et J.M. Muller. Qualité des calculs sur ordinateurs. Masson, Informatique, 1997.
• F. Besson, T. Jensen, J.-P. Talpin: Timed polyhedra analysis for synchronous languages. Proceedings of the 10th International Conference on Concurrency Theory (CONCUR'99), LNCS volume 1664, Springer Verlag, 1999

Annotations Signal de descriptions UML

La place et la complexité croissantes des applications temps réel multi-tâche dans les systèmes industriels pose la question de la maîtrise et de l'automatisation de leur mise en oeuvre. D'un côté les approches synchrones telles que celle adoptée pour le langage à flots de données Signal proposent des méthodes formelles pour le développement et la validation des applications. Parallèlement, l'émergence de la technologie "objets" dans l'industrie, notamment avec UML, permet d'aborder des applications complexes tout en leur assurant une bonne modularité. Il y a donc un défi intéressant à rechercher l'intégration des deux approches. On se place ici dans un cadre où l'on va chercher à annoter les descriptions UML par des propriétés complémentaires de type "multi-horloges" telles qu'elles peuvent être exprimées en Signal (la démarche à terme est de contribuer à l'évolution de la norme UML). Le but est d'utiliser les outils synchrones pour analyser les modèles ainsi annotés afin de vérifier qu'une application a les bonnes propriétés (caractère borné de la mémoire nécessaire, des temps d'exécution entre événements d'entrée-sortie, etc.). Il est souhaitable, dans le cadre de cette démarche, de définir les "bonnes" expressions Signal devant servir à ces annotations. Le sujet proposé consiste donc à définir et réaliser les constructions à ajouter autour du langage Signal dans l'optique d'une meilleure expression d'une part des événements et calculs périodiques, d'autre part du séquencement d'actions.

Description et évaluation d'architectures de communication avec Signal

Le développement d'applications critiques dans un langage temps réel synchrone tel que Signal ou Lustre permet de disposer à la fois d'outils de vérification de propriétés de programmes et d'outils de génération automatique de code. Une méthodologie de distribution des programmes synchrones Signal consiste, par des transformations de programmes respectant la sémantique du programme d'origine, à obtenir un nouveau programme reflétant l'architecture d'implantation considérée. Les communications entre processeurs sont représentées par les communications synchrones usuelles ; sur chacun des processeurs, le programme peut être mono ou multi-tâche. Afin de permettre une mise en oeuvre effective sur une architecture multi-processeur générale (communications asynchrones...), il y a lieu d'une part de permettre la désynchronisation des communications, et d'autre part de faire éventuellement appel aux primitives d'un OS temps réel (typiquement, modèle Arinc) pour la communication et la gestion des tâches. Le sujet proposé consiste à modéliser les architectures de communication considérées en définissant en Signal un ensemble de primitives génériques, et à utiliser cette modélisation pour permettre l'évaluation temporelle de l'application décrite sur l'architecture d'implémentation. Les modèles considérés devront permettre d'étudier des ordonnancements préemptifs.

Accélérations du temps en Signal

Parmi les langages synchrones, une caractéristique propre au langage Signal consiste en la possibqilité de créer des instants entre deux instants d'une horloge existante. On a ainsi un mécanisme, appelé sur-échantillonnage, de création d'horloges "plus grandes" (plus fréquentes) que les horloges d'origine.

Les techniques de synthèse du contrôle implémentées dans le compilateur du langage Signal reposent sur la construction d'une arborescence d'horloges dont les racines sont des bornes supérieures des horloges du programme. Lorsqu'il y a une seule racine (une borne supérieure), il est possible de générer du code indépendant du contexte du programme, l'horloge de base pour cette génération étant cette racine. S'il y a plusieurs racines, on peut se ramener au cas précédent en ajoutant une racine artificielle ; l'utilisateur devra alors en général fournir des informations supplémentaires sur la présence des signaux d'interface (ajout de booléens). Lorsque plusieurs sur-échantillonnages sont utilisés dans un programme, les horloges créées par ces sur-échantillonnages ne sont pas toujours comparables ; si de plus le nombre d'instants créés dépend de conditions internes au programme, il n'est pas forcément souhaitable de faire "remonter" ces informations au niveau de l'interface. On s'attachera dans ce travail à étudier les divers aspects du sur-échantillonnage, tant du point de vue du modèle que de son implémentation. On déterminera par exemple des conditions dans lesquelles des horloges sur-échantillonnées peuvent être comparables, ou au contraire sont suffisamment indépendantes pour qu'il soit possible de générer du code selon des schémas à préciser. Les études s'appuieront notamment sur l'utilisation du sur-échantillonnage dans le cadre de l'interfaçage synchrone-asynchrone (exemple de programmes évoluant de manière concurrente hors de leurs points de synchronisation). D'autres applications peuvent aussi être considérées : simulation de boucles "while" parallèles, chaque itération correspondant à un instant dans une horloge sur-échantillonnée...

Synthèse de contrôleurs optimaux sur des systèmes à événements discrets hiérarchiques.

Le problème de la synthèse de contrôleur sur des systèmes à événements discrets consiste, à partir d'une spécification du système et d'un ensemble de propriétés attendues de celui-ci, à dériver/synthétiser un contrôleur qui, une fois placé dans son environnement, va contraindre le comportement du système de manière à garantir l'ensemble des propriétés. À l'heure actuelle, l'un des problèmes majeurs de la synthèse de contrôleurs réside dans la méthodologie appliquée: alors même que les systèmes à contrôler ont été à l'origine spécifiés de manière hiérarchique (analyse descendante en génie logiciel), la synthèse s'applique sur le système mis à plat (toute la modularité verticale a été oubliée). Ceci combiné au fait que la complexité des algorithmes de calcul croit exponentiellement avec la taille des systèmes, les techniques actuelles constituent un goulot d'étranglement à la diffusion de ces méthodes dans les milieux industriels.

L'objectif de ce stage portera sur l'étude de systèmes hiérarchiques et de leur critère de contrôlabilité. Plus précisément, le sujet portera sur une extension au cas hiérarchique des algorithmes de commande optimale développés par [1]. L'idée est de synthétiser un contrôleur qui ``force'' le système à terminer une tâche tout en minimisant un certain critère de performance. Ce travail pourra se mener de front avec l'étude d'algorithmes symboliques pour la synthèse de contrôleurs sur des systèmes hiérarchiques. Finalement ces différentes techniques pourront être expérimentées dans le cadre d'applications portant sur la sécurité des systèmes informatiques.

[1] R. Sengupta et S. Lafortune. An Optimal Control Theory for Discrete Event Systems, SIAM Journal on Control and Optimization 36(2), mars 1998

Supervision de systèmes dynamiques

Stage en collaboration avec Aida.

Vu la complexité croissante des réseaux, les applications de l'intelligence artificielle tiennent une place de plus en plus importante dans les systèmes de diagnostic et de supervision et en particulier dans l'industrie des télécommunications. Nous avons mis en place des algorithmes de supervision s'appuyant sur des techniques à base de modèles. Le principe est d'inverser un modèle de fonctionnement (automate permettant de passer des pannes aux alarmes) de façon à obtenir un nouvel automate appelé diagnostiqueur, permettant de passer directement des alarmes aux pannes. Ces algorithmes (tout comme les techniques de supervision utilisées aujourd'hui pour le diagnostic) sont basés sur une représentation explicite du système et les algorithmes associés sont énumératifs.

L'objectif de ce stage sera de regarder l'apport des techniques symboliques pour la supervision de systèmes dynamiques. L'idée est de trouver des algorithmes de plus haut niveau basés sur des représentations implicites du modèle sous forme de relations. De cette manière, au lieu d'énumérer les états et les transitions en les considérant explicitement, il sera possible de manipuler symboliquement les relations qui caractérisent ces ensembles. Ces techniques symboliques ne sont pas nouvelles; elles ont été utilisées avec succès en ``Model-Checking'' ou en synthèse de contrôleurs sur des systèmes industriels. Toutefois, il n'existe peu ou pas de méthodes permettant de calculer de manière symbolique un diagnostiqueur.

Après une étude bibliographique, ce stage consistera à :

• définir une modélisation symbolique du modèle et du diagnostiqueur,
• développer un algorithme de construction du diagnostiqueur symbolique,
• comparer l'approche symbolique avec l'approche pré-existante (dont un prototype Dyp a été développé en C++).

Génération de tests par la synthèse de contrôleurs

Stage en collaboration avec Pampa.

Dans le domaine de la commande de systèmes réactifs, le problème de la synthèse de contrôleur est le suivant : à partir d'une spécification du système et d'une propriété attendue de celui-ci, il s'agit de synthétiser un contrôleur qui, placé dans l'environnement et disposant de la spécification, va garantir que les exécutions possibles du système valident cette propriété. Les propriétés sont du type atteignabilité, inévitabilité, invariant, etc. Les spécifications sont en général supposées déterministes.

Malgré l'effort de vérification formelle qui peut être fait sur la spécification, les implémentations du système peuvent contenir des erreurs. Les tests qui sont constitués de séquences de contrôle et d'observation entre l'implémentation et le testeur, fournissent alors le moyen de (in)valider l'implémentation par rapport à une relation de conformité donnée. La génération automatique de tests consiste alors à générer automatiquement des tests à partir de la spécification et d'un objectif de test (qui peut être décrit par une propriété logique ou un automate). Les spécifications peuvent être non-déterministes et posséder des actions internes (non observables et non contrôlables). Dans le domaine du test de conformité de protocoles, différentes techniques permettent de produire ces tests avec des critères de longueur minimale, de contrôle optimal, etc.

On peut voir que les notions de testeur et de contrôleur sont proches. Il y a cependant quelques différences. Le problème de la synthèse n'a pas toujours de solution car le système n'est pas forcément contrôlable. La génération de test en a toujours même si le test ne pourra pas complètement contrôler le système. Il faut alors relâcher les contraintes de la synthèse (existence d'un contrôleur) pour produire un test optimal du point de vue contrôle. La vision théorie des jeux peut être utile de ce point de vue: la recherche d'un test optimal s'apparente au calcul d'une stratégie pour un jeu entre implémentation et testeur. On pourra aussi faire le lien avec la théorie du contrôle des systèmes à événements discrets de Ramadge et Wonham.

Nous proposons donc d'étudier les liens entre génération de tests et synthèse de contrôleur. Plusieurs axes de recherche en découlent :

• l'étude de la description des propriétés à tester (ou encore objectifs de tests) : comment décrire les objectifs de tests de sorte qu'ils puissent être appliqués à la synthèse de contrôleur?
• l'étude de l'existence et de la génération de contrôleurs pour engendrer les tests (des exigences d'optimalité, en la taille ou en termes de contrôle du test par exemple, pourront être prises en compte).

Modélisation de l'hypothèse synchrone dans un langage orienté-objet

Mots-clés : Sémantique, programmation synchrone, langage Java

Les langages de programmation synchrones, comme par example Signal, ont été conçus afin de permettre une mise en oeuvre progressive, structurée et sécurisée des systèmes temps-réel en accompagnant leur réalisation des étapes préliminaires de spécification jusqu'aux étapes finales de codage et de validation. Les langages de programmation par objets, comme Java, favorisent quant à eux des objectifs complémentaires de modularité et de réutilisabilité.

Avec l'avènement de la norme Java temps-réel et l'intrusion de l'informatique embarquée, qui dans son téléphone mobile, qui dans son Palmtop, l'un des mondes tend peu à peu, et sous l'impulsion de1 récentes avancées technologiques, à rejoindre l'autre. Existe-t-il un meilleur de ces deux mondes?

L'objectif de ce stage sera d'élaborer une réflexion autour de cette question. Cette réflexion se traduira par la modélisation et la mise en oeuvre de ``l'hypothèse synchrone'' dans le langage de programmation Java.

Le travail consistera à étudier les différents formalismes de la programmation synchrone, à proposer une formalisation de ces modèles comme une extension de Java (au travers par example d'annotations de programmes ou bien encore de classes abstraites) et enfin à élaborer des techniques de compilation ou de traduction de cette extension en utilisant des techniques et des outils de compilation synchrone existants.

Ce sujet participe aux réalisations d'un projet auquel sont associés l'IRISA, Verimag, Aonix, Silicomp et Thomson-CSF.

Certification des ressources de programmes Java réactifs

Mots-clés : Analyse de programmes, systèmes réactifs enfouis, langage de programmation Java

La spécification et la mise en oeuvre d'un système réactif nécéssite une analyse comportementale précise afin d'en assurer la sureté de fonctionnement et de garantir une exécution efficace et sans pannes.

L'avènement de standard de programmation orienté-objet autour du langage Java (qui se décline en Java temps-réel) d'une part, et d'autre part l'intrusion de l'informatique embarquée, qui dans son téléphone mobile, qui dans son Palmtop, marque une forte avancée technologique qui bouleverse quelque peu les modèles et outils classiques de spécification, de programmation et de vérification.

Ainsi, les outils de spécification à base d'automates et les techniques dites de ``model-checking'' doivent maintenant être complémentées par d'autres techniques d'analyse sémantique (typage, interprétation abstraite) qui vont prendre une part de plus en plus importante dans la mise en oeuvre de systèmes enfouis, lors des phases de développement des systèmes et de leur déploiement sur une architecture cible donnée.

L'objectif de ce stage sera d'étudier les techniques d'analyse de programme (interprétation abstraite, résolution de contraintes, théorie des types) à même de résoudre les problèmes que posent la programmation de systèmes enfouis au moyen du langage de programmation Java.

Le coeur du sujet consistera à proposer une représentation symbolique des ressources utilisées par un programme (taille des données, temps de calcul, topologie des communications) dans le souci de vérifier des propriétés de conformité d'une mise en oeuvre donnée à une architecture donnée (non-débordement de l'utilisation de la mémoire, finitude du nombre de tâches) et dans le but de proposer des optimisations de programmes, comme par exemple l'élimination des tests d'accès aux tableaux, l'élimination des synchronisations inutiles lors des accès des ressources partagées par plusieurs tâches, etc ...

Ce sujet participe aux réalisations d'un projet auquel sont associés l'IRISA, Verimag, Aonix, Silicomp et Thomson-CSF.

Hiérarchisation des systèmes de transitions synchrones

Mots-clés : Systèmes de transitions, programmation synchrone, analyse de programmes.

La spécification et la mise en oeuvre de systèmes réactifs nécéssite une analyse comportementale précise afin d'assurer la sureté de fonctionnement et de garantir l'exécution efficace. L'utilisation de langages de programmation synchrone facilitent la réalisation de systèmes critiques remplissant ces critères.

Dans ce processus d'analyse, une représentation symbolique du système, par exemple sous forme d'arbres de décision binaires, ou bien sous forme de systèmes de transitions hiérarchiques, joue un rôle primordial afin d'en analyser, d'en vérifier et d'en optimiser la structure.

L'objectif de ce stage sera de définir un ensemble d'algorithmiques efficaces pour la représentation hiérarchiques de systèmes de transition symboliques. Il pourra également aborder l'étude de la décision de propriétés de sureté (par exemple l'endochronie) dans les systèmes de transitions hiérarchiques.