Nous nous intéressons dans ce manuscrit au langage ReactiveML, qui est une extension de ML avec des constructions inspirées des langages synchrones. L'idée de ces langages est de diviser l'exécution d'un programme en une suite d'instants logiques discrets. Cela permet de proposer un modèle de concurrence déterministe que l'on peut compiler vers du code séquentiel impératif. La principale application de ReactiveML est la simulation discrète, par exemple de réseaux de capteurs. Nous cherchons ici à programmer des simulations à grande échelle, ce qui pose deux questions : sait-on les programmer de façon simple et modulaire ? sait-on ensuite exécuter ces programmes efficacement ? Nous répondons à la première question en proposant une extension du modèle synchrone appelée domaines réactifs. Elle permet de créer des instants locaux invisibles de l'extérieur. Cela rend possible le raffinement temporel, c'est-à-dire le remplacement d'une approximation d'un système par une version plus détaillée sans changer son comportement externe. Nous développons dans ce manuscrit la sémantique formelle de cette construction ainsi que plusieurs analyses statiques, sous forme de systèmes de types-et-effets, garantissant la sûreté des programmes dans le langage étendu. Enfin, nous montrons également plusieurs implémentations parallèles du langage pour tenter de répondre à la question du passage à l'échelle des simulations. Nous décrivons tout d'abord une implémentation avec threads communiquant par mémoire partagée et basée sur le vol de tâches, puis une seconde implémentation utilisant des processus lourds communiquant par envoi de messages.

La complexité croissante des systèmes d'information modernes a motivé l'apparition de nouveaux paradigmes (objets, composants, services, etc), permettant de mieux appréhender et maîtriser la masse critique de leurs fonctionnalités. Ces systèmes sont construits de façon modulaire et adaptable afin de minimiser les temps d'arrêts dus aux évolutions ou à la maintenance de ceux-ci. Afin de garantir des propriétés non fonctionnelles (par ex. maintien du temps de réponse malgré un nombre croissant de requêtes), ces systèmes sont également amenés à être distribués sur différentes ressources de calcul (grilles). Outre l'apport en puissance de calcul, la distribution peut également intervenir pour distribuer une tâche sur des nœuds aux propriétés spécifiques. C'est le cas dans le cas des terminaux mobiles proches des utilisateurs ou encore des objets et capteurs connectés proches physiquement du contexte de mesure. L'adaptation d'un système et de ses ressources nécessite cependant une connaissance de son état courant afin d'adapter son architecture et sa topologie aux nouveaux besoins. Un nouvel état doit ensuite être propagé à l'ensemble des nœuds de calcul. Le maintien de la cohérence et le partage de cet état est rendu particulièrement difficile à cause des connexions sporadiques inhérentes à la distribution, pouvant amener des sous-systèmes à diverger. En réponse à ces défi scientifiques, cette thèse propose une abstraction de conception et de déploiement pour systèmes distribués dynamiquement adaptables, grâce au principe du Model@Runtime. Cette approche propose la construction d'une couche de réflexion distribuée qui permet la manipulation abstraite de systèmes répartis sur des nœuds hétérogènes. En outre, cette contribution introduit dans la modélisation des systèmes adaptables la notion de cohérence variable, permettant ainsi de capturer la divergence des nœuds de calcul dans leur propre conception. Cette couche de réflexion, désormais cohérente "à terme", permet d'envisager la construction de systèmes adaptatifs hétérogènes, regroupant des nœuds mobiles et embarqués dont la connectivité peut être intermittente. Cette contribution a été concrétisée par un projet nommé ''Kevoree'' dont la validation démontre l'applicabilité de l'approche proposée pour des cas d'usages aussi hétérogènes qu'un réseau de capteurs ou une flotte de terminaux mobiles.

Les systèmes complexes, naturels et artificiels, ont reçu récemment une attention renouvelée : les systèmes naturels, notamment biologiques, du fait de la nécessité de les appréhender dans une démarche systémique ; les systèmes artificiels, du fait de la dématérialisation de l'ordinateur amorcée avec l'informatique ubiquitaire. L'art, de son côté, explore depuis toujours le détournement des dernières avancées scientifiques et technologiques pour la création d'oeuvres singulières. Le travail mené depuis dix ans se situe à la croisée de ces chemins, dans le cadre unificateur des systèmes multi-agents. Je me suis intéressé plus particulièrement à l'interaction homme-machine dans le contexte de l'informatique ambiante, dans l'idée d'une construction automatique et d'une régulation dynamique de systèmes d'interaction. Ce travail est alimenté par la recherche menée dans le cadre de la simulation à base d'agents, aussi bien du point de vue des concepts et outils développés, que du point de vue de l'inspiration tirée des mécanismes d'auto-organisation et de régulation des systèmes étudiés. L'art fournit quant à lui un cadre expérimental original par la mise en scène métaphorique, dans des performances numériques interactives, des situations étudiées.

Cette thèse s'inscrit dans le cadre d'un projet de recherche et de développement qui vise à mettre en place des technologies de simulation permettant de reproduire des comportements humains dans une ville. L'objectif de nos travaux est de définir des algorithmes permettant de simuler les déplacements d'une grande quantité de piétons dans un environnement urbain, en temps réel, et de manière crédible. Pour ce type d'exercice, plusieurs solutions existent. Ces solutions sont principalement développées à partir de deux types d'approches : les approches microscopiques, où les piétons sont modélisés comme des agents autonomes, et les approches macroscopiques, où les piétons sont considérés comme soumis à des lois d'écoulement continues ou discrètes. Notre position est que ces deux approches ne s'opposent pas, contrairement à ce qui ressort de la pratique courante, mais se complètent mutuellement. Privilégier l'une au détriment de l'autre fait courir le risque de produire des solutions partiellement satisfaisantes. Aussi nous sommes nous proposés de clarifier le cadre formel permettant d'appréhender la complexité des déplacements. En ligne avec plusieurs études statistiques et psychologiques sur le déplacement des piétons, nous explicitons un déplacement crédible comme un déplacement économe en énergie métabolique. Nous nous inspirons des jeux de congestion et du paradigme multi-agent pour proposer une formulation générique du problème de déplacement des piétons : nous introduisons la notion de ressources de navigation, que nous décrivons comme des régions de l'espace que les agents utilisent pour atteindre leurs destinations, et via lesquelles les agents interagissent pour estimer leurs dépenses énergétiques de manière robuste. Nous proposons une stratégie de déplacement basée sur les heuristiques taboues et nous considérons le principe influence et réaction pour implémenter les actions de déplacements. Le concept d'environnement issu du paradigme multi-agent s'avère particulièrement utile pour appréhender la complexité de la simulation. L'environnement est considéré comme un composant indépendant et ontologiquement différent des agents qui est pris en compte à tous les niveaux de décisions. Une importante partie de la dynamique de la simulation peut ainsi être déléguée à l'environnement sans altérer l'autonomie des agents. Cette séparation favorise à la fois la crédibilité des résultats et le passage à l'échelle. Nous avons choisi de comparer notre proposition avec un modèle microscopique standard à travers plusieurs scénarios de simulation. Il ressort de notre comparaison que notre modèle permet de reproduire des résultats plus crédibles du point de vue d'un observateur extérieur et plus proches des études empiriques connues sur les déplacements des piétons.

Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.

Aujourd'hui, de plus en plus de systèmes industriels s'appuient sur des applications logicielles temps-réel réparties embarquées (TR2E). La réalisation de ces applications demande de répondre à un ensemble important de contraintes très hétérogènes, voire contradictoires. Pour satisfaire ces contraintes, il est presque toujours nécessaire de fournir à ces systèmes des capacités d'adaptation. Par ailleurs, certaines de ces applications pilotent des systèmes dont la défection peut avoir des conséquences financières - voire humaines - dramatiques. Pour concevoir de telles applications, appelées applications critiques, il faut s'appuyer sur des processus de développpement rigoureux capables de repérer et d'éliminer les erreurs de conception potentielles. Malheureusement, il n'existe pas à notre connaissance de processus de développement capable de traiter ce problème dans le cas où l'adaptation du système à son environnement conduit à modifier sa configuration logicielle. Ce travail de thèse présente une nouvelle méthodologie qui répond à cette problématique en s'appuyant sur la notion de mode de fonctionnement : chacun des comportements possibles du système est représenté par le biais d'un mode de fonctionnement auquel est associé une configuration logicielle. La spécification des règles de transition entre ces modes de fonctionnement permet alors de générer l'implantation des mécanismes de changement de mode, ainsi que des reconfigurations logicielles associées. Le code ainsi produit respecte les contraintes de réalisation des systèmes critiques et implante des mécanismes de reconfiguration sûrs et analysables. Pour ce faire, nous avons défini un nouveau langage de description d'architecture (COAL : Component Oriented Architecture Language) qui permet de bénéficier à la fois des avantages du génie logiciel à base de composants (de type Lightweight CCM), et des techniques d'analyse, de déploiement et de configuration statique, qu'apporte l'utilisation des langages de description d'architecture (et en particulier AADL : Architecture Analysis and Description Language). Nous avons alors réalisé un nouveau framework à composant, MyCCM-HI (Make your Component Container Model - High Integrity), qui exploite les constructions de COAL pour (i) générer le modèle AADL permettant de réaliser le déploiement et la configuration statique de l'application TR2E, (ii) générer le code de déploiement et de configuration des composants logiciels de type Lightweight CCM, (iii) générer le code correspondant aux mécanismes d'adaptation du système, et (iv) analyser formellement le comportement du système, y compris en cours d'adaptation. Ce framework à composant est disponible au téléchargement à l'adresse http ://myccm-hi.sourceforge.net.

Dans cette thèse nous étudions l'isolation mémoire et les mesures de communications efficaces par passage de message dans le contexte des environnements à mémoire partagée et la programmation orientée-objets. L'état de l'art en la matière se base presque exclusivement sur deux techniques complémentaires dites de propriété des objets (ownership) et d'unicité de références (reference uniqueness) afin d'adresser les problèmes de sécurité dans les programmes concurrents. Il est frappant de constater que la grande majorité des travaux existants emploient des méthodes de vérification statique des programmes, qui requirent soit un effort d'annotations soit l'introduction de fortes contraintes sur la forme et les références vers messages échangés. Notre contribution avec SIAAM est la démonstration d'une solution d'isolation réalisée uniquement à l'exécution et basée sur le modèle de programmation par acteurs. Cette solution purement dynamique ne nécessite ni annotations ni vérification statique des programmes. SIAAM permet la communication sans copie de messages de forme arbitraire. Nous présentons la sémantique formelle de SIAAM ainsi qu'une preuve d'isolation vérifiée avec l'assistant COQ. L'implantation du modèle de programmation pour le langage Java est réalisé dans la machine virtuelle JikesRVM. Enfin nous décrivons un ensemble d'analyses statiques qui réduit automatiquement le cout à l'exécution de notre approche.

Les langages synchrones tels que SIGNAL, LUSTRE et ESTEREL sont dédiés à la conception de systèmes critiques. Leurs compilateurs, qui sont de très gros programmes complexes, peuvent a priori se révéler incorrects dans certains situations, ce qui donnerait lieu alors à des résultats de compilation erronés non détectés. Ces codes fautifs peuvent invalider des propriétés de sûreté qui ont été prouvées en appliquant des méthodes formelles sur les programmes sources. En adoptant une approche de validation de la traduction, cette thèse vise à prouver formellement la correction d'un compilateur optimisé et industriel de SIGNAL. La preuve de correction représente dans un cadre sémantique commun le programme source et le code compilé, et formalise une relation entre eux pour exprimer la préservation des sémantiques du programme source dans le code compilé.

Le CERV constitue à Brest un pôle d'excellence en réalité virtuelle à vocation européenne. Les systèmes que l'on cherche à modéliser sont de plus en plus complexes, du fait essentiellement de la diversité des composants, de la diversité des structures et de la diversité des interactions mises en jeu. Un système est alors a priori un milieu ouvert (apparition/disparition dynamique de composants) et hétérogène (morphologies et comportements variés). La réalité virtuelle implique pleinement l'utilisateur humain dans la simulation, rejoignant ainsi l'approche de la conception. La majorité des travaux en réalité virtuelle concerne l'immersion sensorimotrice de l'utilisateur humain au sein d'univers. Ces univers virtuels offrent à l'utilisateur la sensation d'être dans l'environnement et lui donne la possibilité d'y agir. Pour être complet, il faut également "qu'il s'y passe quelque chose", et pas seulement en terme de résultat des actions de l'utilisateur. Les entités qui peuplent les univers virtuels doivent donc avoir un comportement autonome. Ceci soulève la question suivante : comment doter une entité d'un comportement autonome dans un environnement virtuel complexe auquel l'homme participe ? Des techniques d'intelligence artificielle symbolique ont déjà été appliquées pour définir ces comportements. Mais ces techniques montrent très vite leurs limites car elles sont principalement basées sur des règles de comportements mises a priori par le concepteur. Or, dans des mondes virtuels complexes (simulation ouverte, hétérogène et participative), plusieurs entités vont avoir des comportements imprédictibles (variabilité comportementale des entités autonomes, libre arbitre de l'utilisateur), créant ainsi des situations toujours nouvelles. Et face à une situation non prévue par le programmeur, les entités auront le plus souvent des comportements inadaptés. C'est pourquoi les méthodologies tirées des systèmes artificiels adaptatifs peuvent contribuer à pallier ces limitations. Le travail que je poursuis porte sur la thématique de l'adaptation de comportements d'entités autonomes en environnement virtuel participatif. Adapter son comportement, c'est effectuer des transformations conduisant à s'adapter à son environnement. Cette adaptation aura pour objectif de rendre le comportement de l'entité virtuelle le plus crédible possible (ressemblant à un comportement humain). Pour cela, nous prenons le parti de considérer que l'entité doit apprendre au fur et à mesure des expériences, elle doit anticiper le comportement des autres entités et les conséquences sur l'environnement, elle doit également exploiter la présence de l'utilisateur humain dans l'univers virtuel pour adapter son comportement. Imaginons un monde virtuel où chaque entité, au même titre qu'un humain, aurait son propre comportement qui évolue automatiquement pendant la simulation. C'est tout l'enjeu des travaux de recherche présentés ici.

L'interaction entre un faisceau laser émis avec une partie de la lumière réfléchi depuis une cible qui rentre dans la cavité active du laser, est à l'origine du phénomène de rétro-injection optique ou self-mixing. L'utilisation de ces franges interférométriques non conventionnelles, semble attractive du au faible nombre des composant optiques et son caractère auto-aligné. Dans cette thèse nous approchons leur développement en tant qu'implémentation embarqué rentable pour la mesure du déplacement. A cette fin, nous avons exploré des méthodes du traitement du signal pour la détection des franges et la reconstruction du mouvement de la cible, en évitant l'usage de composant externes. Premièrement, nous avons identifié quelques incompatibilités dans des algorithmes précédentes établis dans notre centre de recherche, puis nous avons avancé des solutions. Fondé sur la théorie d'interpolation, an algorithme simplifié mais démontré convenable en temps-réel à été proposé pour la reconstruction du déplacement. En s'appuyant sur l'élaboration d'un signal analytique, il à été proposé une version amélioré pour le calcul de phase. Celle-ci nous à permit de fournir un algorithme pour la détection de franges, robuste aux variations d'amplitude, sans tenir compte du régime de rétro-injection, impliquant une convenable utilisation pour une variété d'applications.