L’objectif de ce travail de thèse est d’explorer la conception de mécanismes de contrôle d’accès dans les environnements collaboratifs ubiquitaires. Les changements dynamiques et l’augmentation du nombre de ressources et d’utilisateurs dans ce type d’environnements rendent le contrôle d’accès plus complexe. Dans ce travail, nous proposons une approche d’adaptation qui permet de déployer et de reconfigurer dynamiquement les composants logiciels en cours d’exécution en fonction des fluctuations de la structure de collaboration et des changements des besoins de contrôle d’accès. En premier lieu, un modèle sémantique de contrôle d’accès est proposé afin de permettre l’expression des besoins de contrôle d’accès selon les situations de collaboration. Des règles d’adaptation qui assurent la décentralisation des mécanismes de contrôle d’accès ont été proposées dans le but d’assurer un passage à l’échelle. En second lieu, nous proposons un framework qui permet d’effectuer l’adaptation et d’exécuter les actions de déploiement des composants logiciels en fonction des besoins de contrôle d’accès à tout moment de la collaboration. Nous avons validé nos contributions à travers un scénario mettant en œuvre des services de collaboration et de partage de ressources dans un environnement de travail collaboratif. / The objective of this work is to explore the design of access control mechanisms in collaborative ubiquitous environments. The dynamic changes and the increasing number of resources and users in this type of environments make the access control more complex. In this work, we propose an adaptation approach that allows deploying and reconfiguring the software components at runtime according to the changes of the collaboration structure and access control requirements. Firstly, a semantic model of access control is proposed to allow the expression of access control requirements. Adaptation rules that ensure the decentralization of access control mechanisms are also proposed for scalability reasons. Secondly, we propose a framework that makes adaptation and implements deployment actions during the collaboration process. We validate our contributions through a scenario that implements collaboration services and resources sharing in a collaborative working environment.

This dissertation focuses on the works of two well-known African Francophone novelists, Ahmadou Kourouma from the Ivory Coast and Mongo Beti from Cameroon. The objective of this study is to look at the influences of African oral traditions and analyze the literary transposition of semantic structures from African languages and cultures into the French language. I utilize Chantal Zabus' explanations of how the process of indigenization leads to relexification, the process by which the authors seek to display their linguistic innovation by attempting to merge their local African languages with the French language. Chapter one introduces the language policies in the Ivory Coast and Cameroon during the colonization and in the post-colonial Africa. It establishes the relationship between the dominant European languages and the local African languages and examines the question of rehabilitation of the African languages. Chapter two examines the impact of the African oral traditions and the use of orality as a writing strategy. Chapter three aims to analyze the process whereby words of African local languages and cultures are semantically incorporated through Les Soleils des Indépendances (1968) and Allah n'est pas oblige (2000) by Ahmadou Kourouma, and Ville cruelle (1954) and Branle-bas en noir et blanc (2000) by Mongo Beti. Chapter four examines the use of stylistic features associated with local African languages by comparing the earlier works of the two authors with their later literary production in order to establish whether there is continuity or not in their writing style.

La sémantique des jeux est une approche pour modéliser les langages de programmation dans laquelle les types sont interprétés par des jeux et les programmes par des stratégies. Ces modèles de jeux ont couvert des constructions fonctionnelles et impératives, des opérateurs de contrôle, etc. L'approche a récemment été étendue aux langages non-déterministes et concurrents, provoquant au passage un changement de perspective profond~: les parties sont maintenant organisées en une catégorie, sur laquelle les stratégies sont des préfaisceaux. La notion fondamentale d'innocence a aussi été caractérisée comme une condition de faisceau. Cette thèse s'attache à l'étude de quelques constructions apparaissant dans ces nouveaux modèles de jeux.D'abord, constatant que, dans plusieurs de ces modèles, l'étape cruciale consiste à définir une catégorie double de jeux et de parties, nous proposons une construction abstraite d'une telle catégorie double à partir de données de base, puis nous démontrons que, sous des hypothèses adéquates, le résultat obtenu permet en effet la construction des stratégies.Dans un second temps, nous établissons un lien entre deux techniques existantes pour définir les parties~: la technique standard, fondée sur les séquences justifiées, et une autre plus récente utilisant les diagrammes de cordes. Nous définissons un plongement (plein) de la première dans la seconde et prouvons qu'elles induisent essentiellement le même modèle.Enfin, nous proposons une axiomatisation des notions de jeu et de partie, de laquelle nous tirons une catégorie de jeux et stratégies. Nous raffinons ensuite les axiomes pour traiter l'innocence et nous démontrons que, sous des hypothèses adéquates, les stratégies innocentes sont stables par composition. / Game semantics is a class of models of programming languages in which types are interpreted as games and programs as strategies. Such game models have successfully covered diverse features, such as functional and imperative programming, or control operators. They have recently been extended to non-deterministic and concurrent languages, which generated an in-depth recasting of the standard approach: plays are now organised into a category, on which strategies are presheaves. The fundamental notion of innocence has also been recast as a sheaf condition. This thesis is a study of various constructions appearing in this new approach to game semantics.We first consider a pattern common to several game models of concurrent languages, in which games and plays are first organised into a double category, from which strategies are then derived. We provide an abstract construction of such a double category from more basic data, and prove that, under suitable hypotheses, the result allows the construction of strategies.Our second contribution is to relate two established techniques for defining plays: the standard one, based on justified sequences, and a more recent one, based on string diagrams. We (fully) embed the former into the latter and prove that they induce essentially the same model.Finally, we propose an axiomatisation of the notions of game and play, from which we formally derive a category of games and strategies. We also refine the axioms to deal with innocence, and prove that, under suitable hypotheses, innocent strategies are stable under composition.

Dans l'industrie l'approche de gestion du cycle de vie du produit (PLM) a été considérée comme une solution essentielle pour améliorer la compétitivité des produits. Elle vise à fournir une plate-forme commune qui rassemble les différents systèmes de l'entreprise à chaque étape du cycle de vie du produit dans ou à travers les entreprises. Bien que les principaux éditeurs de logiciels fassent des efforts pour créer des outils offrant un ensemble complet et intégré de systèmes, la plupart d' entre eux n'intègrent pas l'ensemble des systèmes. Enfin, ils ne fournissent pas une intégration cohérente de l'ensemble du système d'information. Il en résulte une sorte de « tour de Babel », où chaque application est considérée comme une île au milieu de l'océan de l'information, gérée par de nombreuses parties prenantes dans une entreprise, ou même dans un réseau d'entreprises. L'hétérogénéité des parties prenantes augmente le problème d'interopérabilité. L'objectif de cette thèse est de traiter la question de l'interopérabilité sémantique, en proposant une méthode d'annotation sémantique formelle pour favoriser la compréhension mutuelle de la sémantique de l'information partagée et échangée dans un environnement PLM / In manufacturing enterprises the Product Lifecycle Management (PLM) approach has been considered as an essential solution for improving the product competitive ability. It aims at providing a shared platform that brings together different enterprise systems at each stage of a product life cycle in or across enterprises. Although the main software companies are making efforts to create tools for offering a complete and integrated set of systems, most of them have not implemented all of the systems. Finally, they do not provide a coherent integration of the entire information system. This results in a kind of "tower of Babel", where each application is considered as an island in the middle of the ocean of information, managed by many stakeholders in an enterprise, or even in a network of enterprises. The different peculiarities of those stakeholders are then over increasing the issue of interoperability. The objective of this thesis is to deal with the issue of semantic interoperability, by proposing a formal semantic annotation method to support the mutual understanding of the semantics inside the shared and exchanged information in a PLM environment

Le Web 2.0 a montré l'importance des systèmes collaboratifs. Il a permis de transformer des internautes en écrivains du Web. De nombreux outils sociaux tels que les wikis et les blogs sont utilisés par des larges communautés produisant une grande quantité d'informations. Afin d'améliorer la recherche, la navigation et l'interopérabilité, les outils sociaux évoluent en intégrant les technologies du Web sémantique. Les wikis suivent cette tendance et évoluent vers des wikis sémantiques. L'introduction des technologies du Web sémantique dans les outils sociaux pose un certain nombre de problèmes tels que le passage à l'échelle et le support des procédés d'édition collaborative pour garantir la qualité des contenus. Dans ce manuscrit, nous adressons ces problèmes par une instanciation du modèle de réplication optimiste. Dans le cadre des wikis sémantiques, nous répliquons un nouveau type de données composé de pages wikis et d'annotations sémantiques. Nous nous plaçons dans un contexte où le nombre de répliques n'est pas connu et varie à l'exécution à l'instar des réseaux P2P. En tant que système collaboratif, un système de réplication optimiste est correct s'il respecte le modèle de cohérence CCI. Nous proposons Swooki et DSMW, deux instanciations du modèle de réplication optimiste pour les wikis sémantiques assurant la cohérence CCI sur le nouveau type de données répliqué. Swooki est le premier wiki sémantique P2P, il adresse particulièrement les problèmes de passage à l'échelle et de tolérance aux pannes. Tandis que DSMW permet de construire un réseau ami-à-ami sémantique et s'intéresse plus aux problèmes de représentation des procédés / The Web 2.0 has shown the importance of collaborative systems. It has allowed to transform a community of strangers into a community of collaborators. Nowadays, many social tools such as wikis and blogs are used by large communities; they produce a large amount of information. The Semantic Web aims structuring this information in order to make it processable by machines. Many social tools evolve by integrating the Semantic Web technologies. Wikis as social tools follow this trend and evolve towards semantic wikis. The introduction of Semantic Web technologies in social tools raises a number of problems such as scalability and support for collaborative editing processes which is necessary to maintain the quality of the content. In this thesis, we address these problems through an instantiation of the optimistic replication model in the context of semantic wikis, an instantiation replicating a new data type composed of wiki pages and semantic annotations. Indeed, the optimistic replication model is based on the replication of shared objects on multiple sites and ensures their consistency. In our context, the number of sites is unknown and varies like in P2P networks. A collaborative editing system using the optimistic replication is correct if it ensures the consistency model CCI. We propose Swooki and DSMW, two instantiations of the optimistic replication model for semantic wikis that ensure the CCI consistency of the new replicated data type. Swooki is the first P2P semantic wiki. It addresses specifically the problems of scalability and fault tolerance. While DSMW allows to build a semantic friend-to-friend network and to support collaborative editing processes

Ce travail s'inscrit dans le domaine du traitement automatique du langage naturel et traite plus spéci?quement de l'application de ce dernier à la segmentation thématique de texte. L'originalité de cette thèse consiste à intégrer dans une méthode non-supervisée de segmentation thématique de texte de l'information syntaxique, sémantique et stylistique. Ce travail propose une approche linéaire de la segmentation thématique s'appuyant sur une représentation vectorielle issue de l'analyse morpho-syntaxique et sémantique de la phrase. Cette représentation est ensuite utilisée pour calculer des distances entre segments thématiques potentiels en intégrant de l'information stylistique. Ce travail a donné lieu au développement d'une application qui permet de tester les di?érents paramètre de notre modèle, mais qui propose également d'autres approches testées dans ce travail. Notre modèle a été évaluer de deux manières di?érentes, une évaluation automatique sur la base de textes annotés et une évaluation manuelle. Notre évaluation manuelle a donné lieu à la dé?nition d'un protocole d'évaluation s'appuyant sur des critères précis. Dans les deux cas, les résultats de notre évaluation ont été au niveau, voir même au dessus, des performances des algorithmes les plus populaires de la littérature.

De nombreuses études démontrent la ségrégation dont souffrent les habitants de certains quartiers. L'étude de la liste de ces derniers montre qu'une majeure partie d'entre eux sont des grands ensembles construits en France lors des Trente Glorieuses. Ces quartiers ont deux particularités : ils ont été bâtis à l'aide d'un modèle similaire et relèvent principalement du logement social. L'analyse du phénomène urbain, des politiques de la ville et de la situation de nombreux grands ensembles de copropriété montrent que le critère « logement social » ne suffit pas à comprendre l'ensemble des mécanismes de relégation observés. Les politiques de la ville, qui accordent un volet important à l'action sur le bâti, suggèrent aussi que la forme urbaine participe aux mécanismes d'exclusion. La question de l'impact de la matérialité de la forme urbaine dans la distribution sociale de l'espace urbain apparait alors. Cette thèse étudie les liens qui se tissent entre une société et ses espaces. Il s'agit de comprendre comment le social entre interaction avec le spatial. La réponse proposée se focalise sur le cas des grands ensembles français des Trente Glorieuses. En montrant comment la forme urbaine peut produire de la ségrégation, cette recherche met à jour les mécanismes cognitifs stimulés par la perception visuelle qui participent à la relégation des barres et des tours. Autrement dit, elle explique comment la vue procure un ressenti qui est, dans le cas de l'architecture domestique, une construction sociale et culturelle influant sur les perceptions du monde, les manières de faire, de voir et de penser, sur les comportements et les modes de vie des individus dans l'urbain. / Numerous studies, demonstrate the segregation from which the inhabitants of certain districts in difficulties suffer. Said studies show that most of these districts are old French "priority development area" zones (ZUP), that are complexes of tower and slab built in France between 1950s and 1970s. These neighbourhoods have two peculiarities: they were built with a similar model and most of them are social housing. Urban phenomenon, urban policies and the situation of numerous co-ownership show that the criteria «social housing» is not enough to understand the banishment process. Urban policies, which grant an important budget for the action on the built, also suggest that the urban form participates in the mechanisms of exclusion. Does the materiality of the urban form impact the social distribution of the urban space? Do slabs and towers participate in the banishment of their inhabitants?The asked question is about the links established between a society and its spaces. The aim is to understand how social can interact with space. The proposed answer focuses on the case of French global mass housing. Showing how urban form can produce segregation, this thesis reveals the cognitive mechanisms stimulated by the visual perception that are working to slabs and towers blocks relegation. In other words, it explains how the view provides a feeling that is, in the case of domestic architecture, a social and cultural construction affecting the perception of the world, ways of doing, seeing and thinking, of behaviours and lifestyles of people in the urban areas.

Cette thèse s'inscrit dans le domaine de la vérification formelle de programmes parallèles. L'enjeu de la vérification formelle est de s'assurer qu'un programme va bien fonctionner comme il le devrait, sans commettre d'erreur, se bloquer, ou se terminer anormalement. Cela est d'autant plus important dans le domaine du calcul parallèle, où le coût des calculs est parfois très élevé. Le modèle BSP (Bulk Synchronous Parallelism) est un modèle de parallélisme bien adapté à l'utilisation des méthodes formelles. Il garantit une forme de structure dans le programme parallèle, en l'organisant en super-étapes où chacune d'entre elle est composées d'une phase de calculs, puis d'une phase de communications entre les unités de calculs. Dans cette thèse, nous avons choisi d'étendre un outil actuel pour l'adapter à la preuve de programmes BSP. Nous nous sommes basés sur Why, un VCG (générateur de condition de vérification) qui a l'avantage de pouvoir s'interfacer avec plusieurs prouveurs automatiques et assistants de preuve pour décharger les obligations de preuves. Les contributions de cette thèse sont multiples. Dans un premier temps, nous présentons une comparaison des différentes librairies BSP disponibles, afin de mettre en évidence les primitives de programmation BSP les plus utilisées, donc les plus intéressantes à formaliser. Nous présentons ensuite BSP-Why, notre outil de preuve des programmes BSP. Cet outil se repose sur une génération d'un programme séquentiel qui simule le programme parallèle entré permettant ainsi d'utiliser Why et les nombreux prouveurs automatiques associés pour prouver les obligations de preuves. Nous montrons ensuite comment BSP-Why peut-être utilisé pour prouver la correction de quelques algorithmes BSP simples, mais aussi pour un exemple plus complexe qu'est la construction distribuée de l'espace d'états (model-checking) de systèmes et plus particulièrement dans les protocoles de sécurité. Enfin, afin de garantir la plus grande confiance dans l'outil BSP-Why, nous formalisons les sémantiques du langage, dans l'assistant de preuve Coq. Nous démontrons également la correction de la transformation utilisée pour passer d'un programme parallèle à un programme séquentiel / This thesis takes part in the formal verification of parallel programs. The aim of formal verification is to ensure that a program will run as it should, without making mistakes, blocking, or terminating abnormally. This is even more important in the parallel computation field, where the cost of calculations can be very high. The BSP model (Bulk Synchronous Parallelism) is a model of parallelism well suited for the use of formal methods. It guarantees a structure in the parallel program, by organising it into super-steps, each of them consisting of a phase of computations, then communications between the processes. In this thesis, we chose to extend an existing tool to adapt it for the proof of BSP programs. We based ourselves on Why, a VCG (verification condition generator) that has the advantage of being able to interface with several automatic provers and proof assistants to discharge the proof obligations. There are multiple contributions in this thesis. In a first part, we present a comparison of the existing BSP libraries, in order to show the most used BSP primitives, which are the most interesting to formalise. We then present BSP-Why, our tool for the proof of BSP programs. This tools uses a generation of a sequential program to simulate the parallel program in input, thus allowing the use of Why and the numerous associated provers to prove the proof obligations. We then show how BSP-Why can be used to prove the correctness of some basic BSP algorithms, and also on a more complex example, the generation of the state-space (model-checking) of systems, especially for security protocols. Finally, in order to ensure the greatest confidence in the BSP-Why tool, we give a formalisation of the language semantics, in the Coq proof assistant. We also prove the correctness of the transformation used to go from a parallel program to a sequential program

Les lexiques sémantiques sont des ressources indispensables pour permettre à de nombreuses applications de traitement automatique des langues (résumé automatique, recherche d'information, traduction automatique, etc.) d'accéder au sens d'un texte. La question de la pertinence des informations présentes dans de tels lexiques est cruciale : le sens d'un mot comme navet, par exemple, varie considérablement selon que le texte étudié est consacré à la gastronomie ou à la cinématographie. Un moyen économique et linguistiquement motivé de disposer de descriptions de sens de mots réellement pertinentes est d'« apprendre » celles-ci à partir de l'utilisation effective des mots dans un corpus, collection de textes représentative d'un domaine d'expression. Nous proposons pour tenter de répondre à ce défi une méthodologie d'acquisition automatique sur corpus d'informations lexicales sémantiques en trois étapes, fondée sur les principes linguistiques de la Sémantique interprétative de F. Rastier. Par analyse statistique et comparaison des modes d'emploi des mots, en utilisant des méthodes classiques ou originales, nous parvenons tout d'abord à rapprocher des mots appartenant à un même domaine (par exemple donnée, transfert, réseau pour les NTIC), puis des mots de sens similaires (donnée et information). Enfin, nous proposons une première méthode permettant la mise au jour de nuances fines marquant des distinctions de sens entre mots proches (donnée est plus « concret » que information), ce qui constitue un résultat encore inédit en acquisition automatique d'informations lexicales sémantiques.

La modélisation et la spécification de systèmes distribués nécessitent une adaptation des modèles logiques utilisés pour leur représentation. Les notions<br />d'emplacements et de ressources jouent notamment un rôle centrale dans la représentation de ces systèmes.<br /><br />On propose tout d'abord à la proposition d'une première logique, la logique linéaire distribuée et mobile (DMLL) qui intègre les notions de distribution et de mobilité. On propose également une sémantique à la Kripke et un calcul des séquents supportant l'élimination des coupures pour cette logique.<br /><br />Cette première étude a mis en avant le rôle centrale de la sémantique pour la modélisation de systèmes distribués. On propose alors la structure des arbres de ressources, des arbres dont les noeuds possèdent des labels et contiennent des ressources appartenant à<br />monoïde partiel de ressources et BI-Loc, une logique pour raisonner sur ces arbres, un langage permettant de modifier les arbres et son axiomatisation correcte et complète sous forme de triplets de Hoare. Concernant BI-Loc, on détermine des conditions suffisantes pour décider de la satisfaction et de la validité par model-checking et on développe une méthode de preuves fondée sur les tableaux sémantiques correcte et complète.<br /><br />On montre comment on peut raisonner sur les tas de pointeurs grâce aux arbres de ressources. Enfin, on détermine comment le modèle des arbres partiel peut être utilisé pour représenter et spécifier les données<br />semi-structurées et raisonner sur la transformation de ce type de données.