Cette thèse traite de la modélisation et la simulation de réseaux de capteurs sans fil afin de fournir des estimations précises de consommations d'énergie. Un cadre de conception et de simulation base sur SystemC au niveau système est proposé, nommé IDEA1. Elle permet l'exploration de l'espace de conception de réseaux de capteurs à un stade amont. Les résultats de simulation comprennent le taux de livraison de paquets, la latence de transmission et les consommations d'énergie. Sur un banc d'essai comportant 9 nœuds, la différence moyen entre les IDEA1 simulations et les mesures expérimentales est 4.6 %. Les performances d'IDEA1 sont comparées avec un autre simulateur largement utilisé, NS-2. Avec la co-simulation matérielle et logicielle, IDEA1 peut apporter des modèles plus détaillés de nœuds de capteurs. Pour fournir les résultats de la simulation au même niveau d'abstraction, IDEA1 réalise les simulations deux fois plus vite que NS-2.Enfin, deux études de cas sont accomplies pour valider le flot de conception d'IDEA1. La performance de l'IEEE 802.15.4 est globalement évaluée pour diverses charges de trafic et configurations de paramètres de protocole. Une application de contrôle actif des vibrations est également étudiée. Les simulations d'IDEA1 trouvent le meilleur choix de protocoles de communication.

Les logiciels critiques nécessitent l'obtention d'une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild'analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d'information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d'outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d'ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d'information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d'uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d'une définition formellede la notion de dépendance, à l'aide de l'assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l'analyse de toléranceaux pannes.

This thesis focuses on the development of an advanced history-based aspect language and approaches to certain related issues ranging from applications to analysis methods. The aspect language, namely VPA-based Aspect Language, is defined upon visibly pushdown au- tomata (VPAs) [21]. This language is essentially an extension from an existing framework [47] of regular aspect languages. It features VPA-based pointcuts and provides, in particu- lar, constructors for the declarative definition of pointcuts based on regular and non-regular structures. We have also extended and developed the technique for detecting automatically potential interactions among VPA-based aspects. Despite several advantages of the class of visibly pushdown automata, there has been no practical support for them available. Therefore, we have realized a library called VPAlib that provides the implementation of essential data structures and operations for the VPA. This library is essential to enable the construction and analysis of VPA-based aspects. For instance, we have successfully performed certain analysis for detecting interactions among aspects using this library. In order to motivate the use of VPA-based aspects, we have studied two basic kinds of distributed applications, one representing typical systems with nested login sessions, and the other representing a grid computing system over peer-to-peer network. We have shown how VPA-based aspects can be useful for the realization of certain functionalities of these typical distributed applications. Thanks to their highly expressive pointcuts, another important application of VPA-based aspects is to define evolution on component-based systems, especially those with explicit component protocols. The use of aspects over component protocols, however, may break the coherence between the components of the system. We have further developed proof methods to establish the preservation of fundamental correctness properties, such as compatibility and substitutability relations between software components after the application of VPA-based aspects. Finally, we have considered the use of model checking techniques to verify systems that are modified by aspects. The goal of the verification is to check whether an aspect violates the global properties of a base system or the properties of other aspects. We have chosen the approach in which we create an abstract model from the VPA model and then run a model checker that is capable of checking the abstract model against the properties. We formally define the abstraction process and demonstrate our model checking approach via examples.

Lors de l'exécution des applications à base d'objets, plusieurs millions d'objets peuvent être créés, utilisés et enfin détruits s'ils ne sont plus référencés. Néanmoins, des dysfonc- tionnements peuvent apparaître, quand des objets qui ne sont plus utilisés ne peuvent être détruits car ils sont référencés. De tels objets gaspillent la mémoire principale et les ap- plications utilisent donc davantage de mémoire que ce qui est effectivement requis. Nous affirmons que l'utilisation du gestionnaire de mémoire virtuel du système d'exploitation ne convient pas toujours, car ce dernier est totalement isolé des applications. Le système d'exploitation ne peut pas prendre en compte ni le domaine ni la structure des applications. De plus, les applications n'ont aucun moyen de contrôler ou influencer la gestion de la mémoire virtuelle. Dans cette thèse, nous présentons Marea, un gestionnaire de mémoire virtuelle piloté par les applications à base d'objets. Il constitue une solution originale qui permet aux développeurs de gérer la mémoire virtuelle au niveau applicatif. Les développeurs d'une application peuvent ordonner à notre système de libérer la mémoire principale en trans- férant les objets inutilisés, mais encore référencés vers une mémoire secondaire (telle qu'un disque dur). En plus de la description du modèle et des algorithmes sous-jacents à Marea, nous présentons notre implémentation dans le langage Pharo. Notre approche a été validée à la fois qualitativement et quantitativement. Ainsi, nous avons réalisés des expérimentations et des mesures sur des applications grandeur-nature pour montrer que Marea peut réduire l'empreinte mémoire de 25% et jusqu'à 40%.

Dans cette thèse, nous explorons les diverses contributions que les systèmes multi-agents (SMA) et les architectures à base de composants (CBSA) peuvent mutuellement et complémentairement s'apporter l'un à l'autre. Dans un premier temps, nous définissons, illustrons, analysons et discutons une méthodologie du développement des SMA, un modèle de composants (SpeAD), un langage de description d'architecture (SpeADL) et une méthode de conception (SpEArAF) qui facilitent et guident la description et l'implémentation des SMA. Cette réponse complète au développement des SMA est assistée par un outil (MAY) et a été appliquée à un grand nombre d'applications. Dans un second temps, nous explorons à travers divers expériences l'aide que peuvent apporter les SMA auto-adaptatif aux CBSA. Les agents et leur réorganisation continuelle jouent à la fois le rôle de moteur de la construction et de l'adaptation dynamique de l'architecture, mais aussi du conteneur qui connecte ses éléments en pratique.

Cette thèse rend compte d'une recherche sur l'émergence de l'investissement socialement responsable en France. Une démarche qualitative et interprétative est adoptée. Il s'agit de comprendre le processus d'intégration de l'investissement socialement responsable au sein du marché financier, en se focalisant sur le rôle des sociétés de gestion. L'interprétation fait appel à la théorie de la légitimité, en particulier aux travaux de Suchman (1995). Le dispositif méthodologique est fondé sur des entretiens semi-directifs et des données complémentaires. L'analyse des entretiens est effectuée à l'aide du logiciel d'analyse de données qualitatives NVivo. L'interprétation fait émerger des processus de légitimation. Les résultats soulignent l'importance de la stratégie de création mise en œuvre par les agences de notation sociétale, considérées comme des prescripteurs de valeurs. En particulier, la diffusion d'un nouveau modèle d'évaluation de la performance des entreprises apparaît comme le vecteur d'intégration de l'investissement socialement responsable au sein du marché financier.

Les applications embarquées actuelles imposent des contraintes de plus en plus sévères. La puissance sans cesse croissante de calcul et de communication implique l'utilisation d'architectures multiprocesseurs, la portabilité implique des architectures monopuces et la faible consommation et faible coût impliquent des architectures dédiées. Ajouté à cela, les méthodes de conception évoluent moins vite que les possibilités technologiques d'intégration. Ainsi, une approche systématique partant d'un niveau d'abstraction plus élevé que le RTL est nécessaire pour réduire le temps de mise sur le marché et maîtriser la complexité.<br />Le sujet de cette thèse porte sur la mise en œuvre d'une nouvelle approche de conception systématique d'architectures multiprocesseurs monopuces dédiées à des application spécifiques. <br />Ainsi, un modèle architectural multiprocesseur générique est proposé. Ce modèle est modulaire, flexible et extensible, permettant de couvrir un large domaine d'applications. Les composants de traitement sont dissociés du réseau de communication via des interfaces génériques de communication jouant le rôle de coprocesseurs. <br />Un flot de conception complet est constitué de deux étapes principales. La première étape est l'étape d'exploration d'architecture. Concernant cette étape, une méthode d'estimation de performance au niveau système est proposée. Cette méthode permet une exploration rapide de l'espace de solutions architecturales pour trouver l'architecture système optimale pour l'application à concevoir. Le but de cette étape est de fixer les paramètres architecturaux (optimaux) dédiés à l'application. Ces paramètres sont utilisés dans la seconde étape –qui est l'étape d'implémentation– pour produire l'architecture RTL. Cette étape comporte trois types d'actions : la conception des composants logiciels, la conception des composants matériels et la conception du réseau de communication permettant d'intégrer les composants de base. Cette étape est réalisée de façon systématique basée sur l'instanciation et la configuration de composants dans une bibliothèque.<br />L'approche proposée permet de réduire significativement le temps de mise sur le marché de systèmes multiprocesseurs monopuces complexes. Plusieurs applications industrielles ont été réalisées pour valider et évaluer les performances de cette approche.

Cette thèse s'inscrit dans le domaine de l'ingénierie des Interfaces Homme-Machine. Elle a pour thème la conception et la réalisation des modèles d'IHM de la méthode MACAO. Nous étudions l'axe de création des interfaces utilisateur en différenciant trois niveaux de la conception à la réalisation. L'approche adoptée s'appuie sur une analyse théorique et sur des cas d'expériences pratiques des modèles. Cette démarche entre dans le cadre très en vogue des modèles et des transformations de modèles. Cette étude nous conduit à distinguer les étapes de conception d'une IHM en milieu industriel et à mettre en place un processus pour la réalisation des modèles et des maquettes dans la phase de recueil des besoins. En étudiant sur des projets réels la conception des IHM utilisant une représentation abstraite, nous soulignons toute l'importance de traiter de l'interface utilisateur avec l'utilisateur final et l'importance de la concevoir comme un élément de l'architecture générale dès les phases de conception. Nous proposons un procédé de conception de l'architecture de l'IHM qui répond aux besoins de la conception d'une IHM. Ce processus est complété par des modèles à des niveaux de raffinement différents. Nous proposons des métamodèles de ces différentes vues de la création des IHM. Et nous proposons un outil de génie logiciel qui permet d'éditer et d'utiliser le modèle du SNI. De part ses critères et ses techniques de représentation, MACAO représente une des plus douces et progressives façons d'implémenter une interface homme-machine.

Nous proposons de nouveaux algorithmes et de nouvelles structures de données pour la vérifi cation formelle de systèmes réactifs nis sur architectures parallèles. Ces travaux se basent sur les techniques de véri cation par model checking. Notre approche cible des architectures multi-processeurs et multi-coeurs, avec mémoire partagée, qui correspondent aux générations de serveurs les plus performants disponibles actuellement. Dans ce contexte, notre objectif principal est de proposer des approches qui soient à la fois effi caces au niveau des performances, mais aussi compatibles avec les politiques de partage dynamique du travail utilisées par les algorithmes de génération d'espaces d'états en parallèle ; ainsi, nous ne plaçons pas de contraintes sur la manière dont le travail ou les données sont partagés entre les processeurs. Parallèlement à la défi nition de nouveaux algorithmes de model checking pour machines multi-coeurs, nous nous intéressons également aux algorithmes de vérifi cation probabiliste. Par probabiliste, nous entendons des algorithmes de model checking qui ont une forte probabilité de visiter tous les états durant la vérifi cation d'un système. La véri fication probabiliste permet des gains importants au niveau de la mémoire utilisée, en échange d'une faible probabilité de ne pas être exhaustif ; il s'agit donc d'une stratégie permettant de répondre au problème de l'explosion combinatoire.

Les recherches présentées dans ce mémoire visent à inventer des méthodes de conception ou des composants de méthodes (c'est-à-dire des modèles de produits, de processus, et des outils) de nature à soutenir le développement de Systèmes d'Information (SI) innovants, bénéficiant des avancées technologiques pour assurer à l'utilisateur une qualité en tout contexte d'usage. Elles se situent ainsi à la croisée de trois communautés, introduisant chacune une préoccupation : l'Interaction Homme-Machine (IHM) pour la prise en compte de l'utilisateur final ; les Systèmes d'Information (SI) pour la considération du contexte organisationnel ; et le Génie Logiciel (GL) pour l'étude et l'invention des techniques et outils supports. Les contributions s'articulent autour de trois axes : 1) la mise en commun des pratiques des domaines de l'IHM et des SI pour favoriser la prise en compte des spécificités de ces deux domaines ; 2) l'étude conjointe de l'auto-explication pour avancer, avec les spécificités de chacun, vers le défi commun des modèles interactifs ; 3) les pratiques et outils de gestion de modèles au delà des domaines de l'IHM et des SI.