Le travail décrit dans cette thèse s'inscrit dans le contexte du développement et de la validation des systèmes réactifs synchrones. Il vise à tirer parti de certaines formes de structuration des programmes durant le processus de développement et de validation. Nous étudions premièrement l'utilisation d'opérateurs réguliers de types "itérateurs" qui permettent d'exprimer assez facilement des programmes réguliers manipulant des tableaux. Nous montrons aussi comment, au moment de la validation, on peut tirer partie de ces structures régulières pour rendre la preuve d'une propriété plus<br />simple. Nous nous intéressons ensuite à la spécification dite "par contrat" où un couple (assume, guarantee) est associé à chaque composant pour spécifier les hypothèses sur l'environnement et les<br />propriétés satisfaites par le composant sous ces hypothèses. Nous montrons l'intérêt de tels contrats à la fois en terme de spécification et de vérification pour le cas particulier des systèmes synchrones.<br />Nous proposons une série d'algorithmes de transformations de programmes (aussi bien autour de l'utilisation des itérateurs que des contrats) utilisable comme pre-processeur d'objectifs de preuve pour les outils de validation. Nos propositions, notamment sur l'aspect langage des itérateurs, ont répondu à des besoins rencontrés dans les applications industrielles, particulièrement autour du langage Lustre, auquel nous appliquons nos résultat. Ces propositions seront bientôt incluses dans la version industrielle du langage.

Notre thèse se situe dans le domaine des méthodes formelles appliquées aux systèmes réactifs. Nous modélisons et traitons ces systèmes, en continuelle interaction avec leur environnement, grâce au langage<br />synchrone Lustre.<br /><br />D'abord, sur la base d'un travail précurseur, nous établissons pour Lustre une méthode de preuve inductive des propriétés de sûreté. Cette méthode est optimisée, afin de prendre en compte au mieux la dynamique des systèmes. Elle est implémentée dans un outil de preuve, Gloups.<br /><br />Ensuite, suivant le modèle de la méthode B, nous définissons un calcul de raffinement pour Lustre. Ce calcul est à la fois adapté à Lustre et exprimé en ce langage. Les obligations de preuve qui assurent la<br />correction du raffinement peuvent être traitées par Gloups. Pour faciliter le développement, un autre outil, Flush, génère automatiquement les obligations pour Gloups.<br /><br />Ainsi, nous utilisons Lustre à la fois comme langage de programmation et comme cadre formel d'un développement maîtrisé. L'intérêt de ce<br />procédé réside dans la simplicité du langage et dans son adaptation aux systèmes réactifs : en ce domaine, notre méthode de raffinement est suffisamment expressive, sans être inutilement compliquée. Des exemples viennent démontrer l'intérêt de la méthode.

Le travail présenté dans cette thèse porte sur la conception de logiciels pour systèmes embarqués. Outre les contraintes de programmation provenant des faibles quantité de mémoire et capacité de calcul, ces plates-formes matérielles ne disposent parfois que de peu d'énergie pour fonctionner. Les applications usuelles de ces systèmes imposent de plus des objectifs en matière de réactivité et de durée de vie. Par ailleurs, quelques-unes des ressources fournies sont partagées entre les composants, qu'il s'agisse de l'énergie délivrée par une batterie, ou encore des bus de communication qui les relient. Il est donc nécessaire de pouvoir assurer des propriétés globales portant sur l'ensemble de la plate-forme, telles que le contrôle des accès aux bus, ou encore la maîtrise de la puissance électrique consommée. Cependant, les pilotes des différents périphériques sont d'ordinaire programmés individuellement. La connaissance nécessaire à l'implantation d'une politique de contrôle global est alors distribuée parmi diverses portions du logiciel. Nous exposons une solution au problème du contrôle global des ressources, basée sur une vue centralisée des états des composants matériels de la plate-forme. Bâtie sur un principe de para-virtualisation, notre approche consiste en l'introduction d'une couche de contrôle ; le système d'exploitation invité est adapté afin de communiquer avec le matériel à l'aide de celle-ci. La couche de contrôle incorpore les pilotes des périphériques, conçus à partir d'automates dont les états correspondent aux modes de fonctionnement ou de consommation du composant géré. Un contrôleur est ajouté, dont le rôle est d'assurer les propriétés globales. L'ensemble de ces automates est programmé à l'aide d'un langage synchrone, puis compilé en code séquentiel. Nous proposons une implantation de la couche de contrôle pour une architecture de nœuds de réseaux de capteurs sans fil, qui constitue une plate-forme représentative des systèmes embarqués contraints. Nous évaluons qualitativement et quantitativement ce prototype afin de montrer la viabilité de l'approche. Son impact sur le reste du logiciel est également apprécié, que celui-ci soit construit selon un modèle d'exécution purement événementiel ou multi-fils. Enfin, nous passons en revue plusieurs extensions possibles, et identifions quelques bonnes pratiques pour son usage dans d'autres contextes.

Le travail présenté dans cette thèse porte sur la conception de logiciels pour systèmes embarqués. Outre les contraintes de programmation provenant des faibles quantité de mémoire et capacité de calcul, ces plates-formes matérielles ne disposent parfois que de peu d'énergie pour fonctionner. Les applications usuelles de ces systèmes imposent de plus des objectifs en matière de réactivité et de durée de vie. Par ailleurs, quelques-unes des ressources fournies sont partagées entre les composants, qu'il s'agisse de l'énergie délivrée par une batterie, ou encore des bus de communication qui les relient. Il est donc nécessaire de pouvoir assurer des propriétés globales portant sur l'ensemble de la plate-forme, telles que le contrôle des accès aux bus, ou encore la maîtrise de la puissance électrique consommée. Cependant, les pilotes des différents périphériques sont d'ordinaire programmés individuellement. La connaissance nécessaire à l'implantation d'une politique de contrôle global est alors distribuée parmi diverses portions du logiciel. Nous exposons une solution au problème du contrôle global des ressources, basée sur une vue centralisée des états des composants matériels de la plate-forme. Bâtie sur un principe de para-virtualisation, notre approche consiste en l'introduction d'une couche de contrôle ; le système d'exploitation invité est adapté afin de communiquer avec le matériel à l'aide de celle-ci. La couche de contrôle incorpore les pilotes des périphériques, conçus à partir d'automates dont les états correspondent aux modes de fonctionnement ou de consommation du composant géré. Un contrôleur est ajouté, dont le rôle est d'assurer les propriétés globales. L'ensemble de ces automates est programmé à l'aide d'un langage synchrone, puis compilé en code séquentiel. Nous proposons une implantation de la couche de contrôle pour une architecture de nœuds de réseaux de capteurs sans fil, qui constitue une plate-forme représentative des systèmes embarqués contraints. Nous évaluons qualitativement et quantitativement ce prototype afin de montrer la viabilité de l'approche. Son impact sur le reste du logiciel est également apprécié, que celui-ci soit construit selon un modèle d'exécution purement événementiel ou multi-fils. Enfin, nous passons en revue plusieurs extensions possibles, et identifions quelques bonnes pratiques pour son usage dans d'autres contextes. / This thesis is about the design of software for embedded systems. The hardware platforms usually employed in these systems provide a limited amount of memory, computational power and energy. The software they execute is then constrained by such limited resources. Usual applications involve further objectives, such as reactivity and lifetime. In addition, these platforms comprise shared resources like buses or even the energy provided by a battery. Hence, global properties concerning the whole platform must be enforced, for instance to control concurrent accesses to a bus or power consumption. As device drivers are commonly developed individually, the knowledge necessary to implement global control policies is distributed among several pieces of software. We propose a global control approach, based on a centralized view of the devices' states. Built upon para-virtualization principles, it operates on the hardware/software interface. It involves a simple adaptation of the guest operating system, to communicate with the hardware via a control layer. The control layer itself is built from a set of simple automata: the device drivers, whose states correspond to functional or power consumption modes, and a controller to enforce global properties. All these automata are programmed using a synchronous language, and compiled into a single piece of sequential code. As a suitable representative of embedded systems hardware, we choose the node of a wireless sensor network. To show that our approach is practical, we propose a proof-of-concept implementation of the control layer to manage this platform, and evaluate it both qualitatively and quantitatively. We also demonstrate its use and benefits with an event-driven or multithreading operating system, and estimate the impact of the adaptation on guest software. Finally, we audit several extensions and draw guidelines for its use in other contexts.

Ce document retrace de manière synthétique mes travaux de recherche depuis septembre 1999, date à laquelle j'ai été recruté sur un poste de Maître de Conférences à l'université Joseph Fourier (Grenoble 1).<br />Ces travaux, menés au sein de l'équipe VASCO du laboratoire LIG, portent sur le test des logiciels et sont étroitement liés aux recherches effectuées de 1993 à 1997, période pendant laquelle j'ai été thésard, puis chercheur contractuel dans cette même équipe.<br />Le test logiciel est une discipline qui embrasse l'ensemble du cycle de développement.<br />En effet, dès l'analyse des besoins d'une application, apparaissent des exigences et des propriétés à tester dont la caractérisation et l'identification font partie des compétences des testeurs. Il en est de même pour la spécification du produit, la conception de son architecture technique ou la programmation. <br />Le test logiciel est également une discipline qui se veut étroitement liée et utile à la pratique professionnelle. La prise en compte des problématiques issues de cette dernière s'est faite, entre autres, au moyen de nombreuses collaborations industrielles qui ont ponctué mes travaux, en particulier dans le cadre de projets nationaux (RNRT, RNTL).

Ce travail porte sur la programmation et la verification des systemes reactifs. Il consiste dans une premiere partie en la definition d'un langage mixte imperatif/declaratif, nomme ArgoLus, fonde sur les langages synchrones Argos et Lustre. Argos est un langage imperatif a base d'automates paralleles et hierarchises. Lustre est un langage declaratif fonde sur le modele flots de donnees. Le langage ArgoLus permet de melanger au niveau source ces deux langages. La definition des traductions structurelles d'ArgoLus en Argos ou en Lustre offre deux solutions interessantes pour mettre en oeuvre ce langage, tout en profitant des environnements deja existants. Dans un deuxieme temps la semantique d'Argos en termes de graphes temporises a ete definie. Initialement, celle-ci est definie en termes de systemes de transitions etiquetees. L'inconvenient de ce modele est lie au phenomene d'explosion du nombre d'etats qui limite les possibilites de verification formelle. Une des causes de cette explosion est la presence dans les programmes de compteurs d'occurrences d'evenement. Les graphes temporises sont des automates etendus avec des compteurs de temps, dont la taille est independante des valeurs limites des compteurs du programme. Par consequent, ils sont moins sensibles au phenomene d'explosion du nombre d'etats, d'ou une amelioration des possibilites de verification formelle. De plus, il est possible grace a ce modele d'exprimer des proprietes quantitatives faisant reference au temps. Enfin, un troisieme aspect de ce travail porte sur l'utilisation pour les systemes reactifs d'outils de verification formelle, non concus exactement pour ce type de systemes.

La programmation synchrone est utilisée pour faciliter la description des systèmes réactifs, devant réagir de façon continue avec leur environnement physique. Ces systèmes sont souvent répartis, pour des raisons d'implantation physique ou de tolérance aux fautes. D'autre part, de tels systèmes sont aussi critiques et temps-réel. Le but de ce travail est d'étudier des méthodologies d'implantation de tels systèmes sur des réseaux de calculateurs. Nous montrons comment l'application de la programmation synchrone pose des problèmes de robustesse pour la programmation de tels systèmes en raison de la non correspondance du temps logique au temps réel. Nous étudions la robustesse dans divers cas: systèmes continus et systèmes discrets. En particulier nous fournissons des outils de simulation pour des architectures réparties quasi-synchrones et des outils de vérification de la robustesse. Nous proposons aussi un protocole de synchronisation dans les cas de systèmes non robustes. Nous proposons enfin une approche de tolérance aux fautes pour les systèmes répartis quasi-synchrones.

Nous nous intéressons à la conception sûre de systèmes répartis. Nous montrons qu'avec la complexité et l'intégration croissante des systèmes embarqués, la structure fonctionnelle du système peut entrer en conflit avec la structure de son architecture. L'approche traditionnelle de conception par raffinement de cette architecture compromet alors la modularité fonctionnelle du système. Nous proposons donc une méthode permettant de concevoir un système réparti défini comme un programme unique, dont la structure fonctionnelle est indépendante de l'architecture du système. Cette méthode est basée sur l'ajout de primitives de répartition à un langage flots de données synchrone. Ces primitives permettent d'une part de déclarer l'architecture sous la forme d'un graphe définissant les ressources existantes et les liens de communication existant entre ces ressources, et d'autre part de spécifier par des annotations la localisation de certaines valeurs et calculs du programme. Nous définissons ensuite la sémantique formelle de ce langage étendu. Cette sémantique a pour but de rendre compte de manière formelle l'effet des annotations ajoutées par le programmeur. Un système de types à effets permet ensuite de vérifier la cohérence de ces annotations. Ce système de types est muni d'un mécanisme d'inférence, qui permet d'inférer, à partir des annotations du programmeur, la localisation des calculs non annotés. Nous définissons ensuite, à partir de ce système de types, une méthode de répartition automatique permettant d'obtenir, à partir d'un programme annoté, un fragment de programme par ressource de l'architecture. La correction du système de types avec la sémantique du langage est prouvée, ainsi que l'équivalence sémantique de l'exécution des fragments obtenus par la méthode de répartition automatique avec le programme initial. Cette méthode a été implémentée dans le compilateur du langage Lucid Synchrone, et testée sur un exemple de radio logicielle.

La programmation synchrone a ete proposee pour faciliter la conception et la programmation des systemes reactifs (systemes dont le role est de reagir continument a leur environnement physique, celui-ci etant incapable de se synchroniser avec le systeme). Ces systemes sont tres souvent repartis, que ce soit pour des raisons d'implantation physique, d'amelioration des performances ou de tolerance aux pannes. En outre, les travaux sur la compilation des langages synchrones ont conduit a utiliser une representation interne des programmes sous forme d'un automate d'etats fini : c'est le format OC. Ce travail porte donc sur la repartition automatique des programmes OC. La principale difficulte est d'assurer l'equivalence fonctionnelle et temporelle entre le programme centralise initial et le programme reparti, et de prouver cette equivalence, ce qui est indispensable dans le domaine du temps reel critique. Nous nous attachons egalement a minimiser localement la structure de controle de chaque programme reparti. Pour cela nous developpons un algorithme original de reduction des tests ``a la volee'' utilisant des techniques de bisimulation. D'autre part nous definissons completement l'environnement d'execution des programmes repartis. Ici notre principal souci est de fournir une solution la plus proche possible de l'execution centralisee. Enfin dans le but d'expliquer les desynchronisations introduites par la repartition, nous proposons une semantique originale du langage synchrone Lustre, semantique definie par des ordres partiels.

Les systemes temps reel sont des dispositifs constitues de materiels et de logiciels soumis a des contraintes a la fois fonctionnelles et temporelles pour realiser des traitements, et agir sur leur environnement. Des exemples de domaines o u on rencontre de tels systemes sont les telecommunications, le nucl eaire, l'avionique ou le medical. Ces systemes sont souvent critiques a cause d'enjeux humains et economiques importants. Leur developpement exige donc des methodes tres ables. L'approche synchrone a et e proposee dans le but de repondre a cette attente. Ses fondements mathematiques o rent un cadre formel propice a la description et la validation des systemes temps reel. Parmi les modeles de specification synchrone, le modele multi-horloge ou polychrone se distingue par le fait qu'il permet de decrire des systemes o u chaque composant peut avoir sa propre horloge d'activation. Outre la validation formelle, il favorise des approches orientees composants et le d eveloppement modulaire de systemes a grande echelle. Cette these propose une m ethodologie de conception de syst emes temps reel en utilisant comme formalisme de description le langage synchrone Signal fond e sur le mod ele polychrone. Elle utilise les outils et techniques formels bas es sur ce modele pour verifier des proprietes comportementales portant sur des aspects tant fonctionnels que non fonctionnels. Cette demarche facilite l' evaluation des choix de conception. La methodologie propos ee permet de concevoir des systemes comportant des m ecanismes asynchrones a l'aide de l'approche synchrone. Elle illustre la caracterisation de comportements temps r eel dans le modele polychrone. L'avionique est le domaine d'application privilegie par la these. Cette derniere s'inscrit dans le cadre du projet europ een IST SafeAir (Advanced Design Tools for Aircraft Systems and Airborne Software), regroupant plusieurs industriels. Nous nous sommes particulierement interesses a la conception d'applications suivant le mod ele d'architecture IMA (Integrated Modular Avionics) sur lequel repose la norme avionique ARINC. Cela a conduit a la r ealisation d'une bibliotheque Signal de composants, constituee en majeure partie de services d'un ex ecutif temps reel d e nis par ARINC.