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%.

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.

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.

Assurer l'interopérabilité de manière dynamique et automatique demeure un enjeu majeur dans le développement et la mise en œuvre des systèmes logiciels modernes. En effet, ces systèmes comprennent souvent plusieurs composants qui fonctionnent conjointement afin de satisfaire aux exigences des utilisateurs. Toutefois, les disparités pouvant exister entre les interfaces et les comportements de ces composants les empêchent de fonctionner ensemble, c'est-à-dire d'interopérer. Les solutions existantes visent à concilier ces disparités à travers la mise en œuvre d'intergiciels ou la génération de médiateurs. La mise en œuvre d'intergiciels n'offre qu'une solution statique, inadaptée aux environnements fortement dynamiques, tels que les environnements ubiquitaires. Les approches pour la génération de médiateurs requièrent que les correspondances entre les interfaces des composants soient préalablement spécifiées, et n'offrent de ce fait qu'une solution partiellement automatique à l'interopérabilité. Ainsi, les solutions existantes se révèlent souvent insuffisantes, particulièrement dans les environnements où les composants devant interopérer ne sont connus qu'à l'exécution. Dans cette thèse, nous définissons une approche à l'interopérabilité basée sur la synthèse automatique de médiateurs. Tout d'abord, nous intégrons la programmation par contraintes et le raisonnement ontologique afin d'inférer les traductions nécessaires pour pallier les différences entre les interfaces des composants. Ces traductions servent de base à la synthèse de médiateurs qui coordonnent les comportements des composants afin de garantir l'absence d'interblocage lors de leurs interactions. Enfin, nous procédons à l'analyse et la génération des messages au niveau intergiciel de façon à implémenter ces médiateurs. Pour valider notre approche, nous avons développé un prototype, appelé MICS, qui effectue la synthèse dynamique de médiateurs afin d'assurer l'interopérabilité entre composants en dépit de leurs différences aussi bien au niveau applicatif qu'au niveau intergiciel. Nous avons également expérimenté MICS en considérant plusieurs cas d'études allant de la médiation entre messageries instantanées à la gestion de l'interopérabilité dans les systèmes de systèmes. Cela nous a permis d'une part de démontrer la viabilité de notre solution et d'autre part d'évaluer son efficacité.

L'élaboration de plannings de travail de personnel représente un problème majeur auquel sont confrontées la plupart des organisations. Nous nous préoccupons ici de l'automatisation de cette tâche, liant négociation et calcul combinatoire. Les modèles préférentiels sur lesquels se base l'évaluation des plannings sont complètement révisés. Une nouvelle représentation combinatoire des préférences est proposée, couplant le concept de relation binaire de préférence à celui de contrainte souple. Elle est mieux adaptée à la formulation des opinions de chaque acteur et intègre la notion d'aide à la décision et d'interactivité en admettant l'incomparabilité et l'intransitivité. Ensuite, l'agrégation des préférences individuelles est réalisée par la méthode axiomatique en usant de plusieurs principes éthiques : l'équité (Pigou-Dalton, Suppes-Sen) et l'efficacité (Pareto). Divers algorithmes de filtrage et de recherche de solution adaptés à la forme particulière des préférences et critères sont conçus. Un système interactif d'élaboration de plannings infirmiers est décrit.

Leveraging our experience with the traditional approach to ambient assisted living (AAL) which relies on a large spread of heterogeneous technologies in deployments, this thesis studies the possibility of a more "stripped down" and complementary approach, where only a reduced hardware subset is deployed, probing a transfer of complexity towards the software side, and enhancing the large scale deployability of the solution. Focused on the reasoning aspects in AAL systems, this work has allowed the finding of a suitable semantic inference engine for the peculiar use in these systems, responding to a need in this scientific community. Considering the coarse granularity of situational data available, dedicated rule-sets with adapted inference strategies are proposed, implemented, and validated using this engine. A novel semantic reasoning mechanism is proposed based on a cognitively inspired reasoning architecture. Finally, the whole reasoning system is integrated in a fully featured context-aware service framework, powering its context awareness by performing live event processing through complex ontological manipulation. the overall system is validated through in-situ deployments in a nursing home as well as private homes over a few months period, which itself is noticeable in a mainly laboratory-bound research domain

Le doctorat s'inscrit dans le cadre d'une bourse CIFRE et d'un partenariat entre l'ENSTA Bretagne, l'IRISA et Thales Air Systems. Les préoccupations de ce dernier, et plus particulièrement de l'équipe de rattachement, sont de réaliser des systèmes à logiciels prépondérants embarqués. La complexité de ces systèmes et les besoins de compétitivité associés font émerger la notion de "Model-Based Product Lines(MBPLs)". Celles-ci tendent à réaliser une synergie de l'abstraction de l'Ingénierie Dirigée par les Modèles (IDM) et de la capacité de gestion de la capitalisation et réutilisation des Lignes de Produits (LdPs). La nature irrévocablement dynamique des systèmes réels induit une évolution permanente des LdPs afin de répondre aux nouvelles exigences des clients et pour refléter les changements des artefacts internes de la LdP. L'objectif de cette thèse est unique, maîtriser des incréments d'évolution d'une ligne de produits de systèmes complexes, les contributions pour y parvenir sont duales. La thèse est que 1) une variabilité multidimensionnelle ainsi qu'une modélisation relationnelle est requise dans le cadre de lignes de produits de systèmes complexes pour en améliorer la compréhension et en faciliter l'évolution (proposition d'un cadre générique de décomposition de la modélisation et d'un langage (DSML) nommé PLiMoS, dédié à l'expression relationnelle et intentionnelle dans les MBPLs), et que 2) les efforts de spécialisation lors de la dérivation d'un produit ainsi que l'évolution de la LdP doivent être guidé par une architecture conceptuelle (introduction de motifs architecturaux autour de PLiMoS et du patron ABCDE) et capitalisés dans un processus outillé semi-automatisé d'évolution incrémentale des lignes de produits par extension.

Les travaux présentés dans ce mémoire proposent une méthode originale de génération automatique de tests à partir de modèles SysML pour la validation de systèmes embarqués. Un sous-ensemble du langage SysML (appelé SysML4MBT) regroupant les éléments de modélisation pris en compte dans notre approche a été défini et une stratégie de génération de tests dédiée (intitulée ComCover) a été créée. Cette stratégie, basée sur les principes du critère de couverture de modèles bien connu Def-Use, s'intéresse à la couverture des communications (envois / réceptions) au sein du système et entre le système et son environnement.La mise en œuvre opérationnelle d'un prototype, basé sur un générateur de tests à partir de modèle UML, a nécessité la définition de règles de réécriture permettant la transformation du modèle SysML4MBT vers le format d'entrée natif du générateur de tests tout en conservant l'expressivité de SysML4MBT. Finalement, les étapes de concrétisation des tests en scripts exécutables et l'établissement automatique du verdict lors de l'exécution sur banc de test définis durant le projet VETESS permettent l'établissement d'une chaîne outillée opérationnelle de génération et d'exécution automatique de tests à partir de spécifications SysML. Cette chaîne outillée a été étrennée sur plusieurs cas d'étude automobile tels que l'éclairage avant, les essuie-glaces ou la colonne de direction de véhicule. Sur ce dernier exemple, nous avons eu l'opportunité d'exécuter les tests sur un banc de test physique. Ces cas d'étude ont permis de valider chacune des étapes de l'approche proposée.