L'introduction du temps dans les bases de données classiques et spatiales apparaît de plus en plus, aujourd'hui, comme une nécessité pour une gestion optimale de l'historicité. En effet, les applications de bases de données spatio-temporelles sont présentes dans un grand nombre d'applications. Le besoin, par exemple, est de sauvegarder l'historique des géométries des parcelles dans le système d'information d'un plan cadastral, la prévention d'incendie dans le système de gestion forestière, le système de navigation des véhicules, etc. Cet historique des phénomènes permet de mieux comprendre ce qui s'est produit dans le passé, de manière à éventuellement anticiper certaines évolutions futures.<p><p>Etant donné ces nouveaux besoins, cette thèse se focalise sur la modélisation et l'implantation des aspects temporels dans bases de données. En effet, la conception d'une application de base de données se fait par un enchaînement de trois phases (conceptuelle, logique et physique). Au niveau conceptuel, plusieurs modèles conceptuels ont été proposés intégrant les caractéristiques temporelles et spatiales.<p><p>Malheureusement, au niveau logique, les modèles de données des SGBD actuels n'offrent pas les concepts nécessaires pour implanter le modèle conceptuel spatio-temporel. Nous proposons donc de nouvelles règles de traductions d'un schéma conceptuel, basé sur le modèle MADS (Modélisation des Applications à des données spatio-temporelles), en un schéma logique MADSLog pour les modèles cibles à savoir :relationnel et relationnel-objet. Chaque règle transforme un concept structurel, temporel et spatial du modèle MADS en un ou plusieurs concepts supportés par la cible. Par exemple, la propriété spatiale définissant la géométrie d'un type d'objet est traduite par la création d'un nouvel attribut de type spatial dans ce type d'objet. Un outil CASE(Computer-Aided Software Engineering) appelé Schema Translateur est développé dans cette thèse implémentant toutes les règles de traductions.<p><p>La traduction de schémas conceptuels en schémas logiques peut impliquer une perte sémantique en raison de la différence de la puissance d'expression entre le modèle conceptuel et le modèle de données des SGBD existants. D'où la nécessité de générer un ensemble de contraintes d'intégrité afin de préserver la sémantique définie dans le schéma conceptuel. Ces contraintes sont exprimées à ce niveau par des formules logiques.<p><p>Avec l'apparition de GML (Geographic Markup Language ) qui est conçu pour la modélisation, le transport et le stockage d'informations géographiques. Nous transformons également le schéma conceptuel MADS en GML. De nouveaux schémas GML temporel et spatial sont définis qui peuvent être employés par n'importe application de base de données spatio-temporelle.<p><p>Au niveau physique, nous proposons une méthode d'adaptation du schéma logique en schéma physique pour le modèle relationnel-objet.<p>Elle permet de définir les tables, les types abstraits, les types d'objets, les domaines, etc. Notre proposition permet aussi la génération des contraintes d'intégrité au niveau physique. En effet, chaque contrainte d'intégrité (structurelle, temporelle ou spatiale) qui est définie en calcul logique est exprimée soit directement par des contraintes déclaratives ou soit par des déclencheurs du SGBD choisi. Les déclencheurs spatiaux sont fondés sur les fonctionnalités prédéfinies dans Oracle, alors que les déclencheurs temporels sont basés sur les opérateurs et méthodes appliquées sur les types temporels.<p><p>Enfin, la traduction de requêtes est une deuxième clef de cette recherche. Le but de la traduction de requêtes, exprimées en algèbre, étant de reconstituer l'information au sens MADS à partir de la base de données stockées dans le SGDB cible. Elle permet de traduire les expressions algébriques MADS, qui sont définies sur le schéma conceptuel et non sur le schéma physique, en requêtes opérationnelles qui peuvent être exécutées sur une base de données spatiale et temporelle sous un SGBD ou un SIG.<p> / Doctorat en sciences appliquées / info:eu-repo/semantics/nonPublished

Les logiciels modernes sont de plus en plus complexes. Ceci est dû en partie à l'hétérogénéité des solutions misent en oeuvre, au caractère distribué des architectures de déploiement et à la dynamicité requise pour de tels logiciels qui devraient être capable de s'adapter en fonction des variations de leur contexte d'évolution. D'un autre coté, l'importance grandissante des contraintes de productivité dans le but de réduire les coûts de maintenance et de production des systèmes informatiques a favorisé l'émergence de nouveaux paradigmes pour répondre à la complexité des logiciels modernes. L'informatique des systèmes autonomes (Autonomic computing) s'inscrit dans cette perspective. Elle se propose entre autres de réduire le coût de maintenance des systèmes informatiques en développant des logiciels dits autonomes, c'est à dire dotés de la capacité de s'auto-gérer moyennant une intervention limité d'un opérateur humain. Toutefois, le développement de logiciels autonomes soulèvent de nombreux défis scientifiques et technologiques. Par exemple, l'absence de visibilité de la couche de contrôle dans les applications autonomes rend difficile leur maintenabilité, l'absence d'outils de vérification pour les architectures autonomes est un frein pour l'implémentation d'applications fiables, enfin, la gestion transparente des propriétés non-fonctionnelles et la traçabilité entre le design et l'implémentation sont autant de défis que pose la construction de logiciels autonomes flexibles. La principale contribution de cette thèse est CORONA. CORONA est un canevas logiciel qui vise à faciliter le développement de logiciels autonomes flexibles. Dans cet objectif, CORONA s'appuie sur un langage de description architecturale qui réifie les éléments qui forment la couche de contrôle dans les systèmes autonomes. CORONA permet l'intégration transparente des propriétés non-fonctionnelles dans la description architecturale des systèmes autonomes. il fournit aussi dans sa chaîne de compilation un ensemble d'outils qui permet d'effectuer des vérifications sur l'architecture des systèmes autonomes. Enfin, la traçabilité entre le design et l'implémentation est assurée par un mécanisme de génération des skeletons d'implémentation à partir d'une description architecturale. Les différentes propriétés de CORONA sont illustrées par trois cas d'utilisation.

La thèse contribue à la compréhension de la nature, du rôle et des mécanismes de la polarisation dans les langages de programmation, en théorie de la preuve et dans les modèles catégoriels. La polarisation correspond à l'idée que la condition d'associativité de la composition peut être relâchée, comme on le montre à travers un résultat qui relie les duploïdes, notre modèle direct de la polarisation, aux adjonctions. En conséquence, la polarisation sous-tend de nombreux modèles du calcul, ce que l'on souligne encore en montrant comment les modèles par passage de continuation pour des opérateurs de contrôle délimité se décomposent en trois étapes fondamentales. Elle explique également des phénomènes de constructivité en théorie de la démonstration, ce que l'on illustre en donnant une interprétation selon le principe de la formule comme type à la polarisation en général et à une négation involutive en particulier. Notre approche est basée sur une représentation interactive des démonstrations et des programmes à base de termes (calcul L), qui met en évidence la structure des polarités. Celle-ci est basée sur la correspondance entre les machines abstraites et les calculs de séquents, et vise à synthétiser diverses directions : la modélisation du contrôle, de l'ordre d'évaluation et des effets dans les langages de programmation, la quête d'un lien entre la dualité catégorielle et les continuations, et l'approche interactive de la constructivité en théorie de la preuve. On introduit notre technique en supposant uniquement une connaissance élémentaire du λ-calcul simplement typé et de la réécriture.

Les travaux réalisés dans le cadre de cette thèse ont pour objectif de proposer un langage de description temporelle pour des systèmes temps-réel et d’établir les conditions de leur ordonnançabilité sous l’algorithme Earliest Deadline First (EDF). Les langages de description temporelle permettent de spécifier le comportement temporel d’une application indépendamment de son comportement fonctionnel. Le programmeur déclare dans ces langages à quels instants précis doivent être déclenchées et terminées les activités du système. Cette gestion du temps, précise et explicite, apporte au système son caractère déterministe. Le langage proposé, Extended Timing Definition Language (E-TDL), étend des langages dirigés par le temps existants, en particulier Giotto et TDL, en introduisant un nouveau modèle de tâche donné par quatre paramètres : phase, pire temps d’exécution, temps d’exécution logique TEL (intervalle de temps séparant le lancement de la tâche et sa terminaison) et période. L’introduction de ce nouveau modèle de tâche nécessite de revisiter en particulier le problème de l’ordonnançabilité des tâches pour EDF. Cette thèse propose et développe une analyse basée sur la fonction de demande pour des ensembles de tâches décrites en E-TDL et s’exécutant en contexte monoprocesseur. Une condition nécessaire et suffisante est obtenue au travers d’une analyse précise des intervalles séparant les activations de tâches au sein de différents modules s’exécutant indépendamment et pouvant changer de mode à des instants prédéfinis. Une borne de la longueur des intervalles sur lesquels doit s’opérer la vérification est déterminée. Un outil mettant en œuvre cette analyse a été développé. / The goal of this research is to define a time-triggered language for modeling real-time systems and to provide the conditions for their schedulability under Earliest Deadline First (EDF). Time-triggered languages separate the functional part of applications from their timing definition. These languages permit to model the real-time system temporal behavior by assigning system activities to particular time instants. We propose a new time-triggered framework, Extended Timing Definition Language (E-TDL), that enhances the basic task model used in Giotto and TDL while keeping compositional and modular structure brought by the latter. An E-TDL task is characterized by: an offset, a worst case execution time, a Logical Execution Time (a time interval between task release and its termination) and a period. The schedulability analysis of the system based on this new task model should be, in particular for EDF, investigated. We develop, on the concept of the processor demand criterion, conditions for the feasibility of an E-TDL system running on a single CPU under EDF. A necessary and sufficient condition is obtained by considering the global schedules that are made up of execution traces occurring at the same time in distinct modules that are able to switch their modes at predefined instants. We estimate a maximal length of the interval on which the schedulability condition must be checked. A tool suite performing the schedulability analysis of the E-TDL systems is developed.

Malgré de nombreuses années de travail en robotique, il existe toujours un manque d’architecture logicielle et de middleware stables pour les systèmes multi-robot. Un intergiciel robotique devrait être conçu pour faire abstraction de l’architecture matérielle de bas niveau, faciliter la communication et l’intégration de nouveaux logiciels. Cette thèse se concentre sur le middleware pour systèmes multi-robot et sur la façon dont nous pouvons améliorer les frameworks existantes dans un contexte multi-robot en ajoutant des services de coordination multi-robot, des outils de développement et de déploiement massif. Nous nous attendons à ce que les robots soient de plus en plus utiles car ils peuvent tirer profit des données provenant d’autres périphériques externes dans leur prise de décision au lieu de simplement réagir à leur environnement local (capteurs, robots coopérant dans une flotte, etc.). Cette thèse évalue d’abord l’un des intergiciels les plus récents pour robot(s) mobile(s), Robot operating system (ROS), suivi par la suite d’un état de l’art sur les middlewares couramment utilisés en robotique. Basé sur les conclusions, nous proposons une contribution originale dans le contexte multi-robots, appelé SDfR (Service discovery for Robots), un mécanisme de découverte des services pour les robots. L’objectif principal est de proposer un mécanisme permettant aux robots de garder une trace des pairs accessibles à l’intérieur d’une flotte tout en utilisant une infrastructure ad-hoc. A cause de la mobilité des robots, les techniques classiques de configuration de réseau pair à pair ne conviennent pas. SDfR est un protocole hautement dynamique, adaptatif et évolutif adapté du protocole SSDP (Simple Service Discovery Protocol). Nous conduisons un ensemble d’expériences, en utilisant une flotte de robots Turtlebot, pour mesurer et montrer que le surdébit de SDfR est limité. La dernière partie de la thèse se concentre sur un modèle de programmation basé sur un automate temporisé. Ce type de programmation a l’avantage d’avoir un modèle qui peut être vérifié et simulé avant de déployer l’application sur de vrais robots. Afin d’enrichir et de faciliter le développement d’applications robotiques, un nouveau modèle de programmation basé sur des automates à états temporisés est proposé, appelé ROSMDB (Robot Operating system Model Driven Behaviour). Il fournit une vérification de modèle lors de la phase de développement et lors de l’exécution. Cette contribution est composée de plusieurs composants : une interface graphique pour créer des modèles basés sur un automate temporisé, un vérificateur de modèle intégré basé sur UPPAAL et un générateur de squelette de code. Enfin, nous avons effectué deux expériences : une avec une flotte de drones Parrot et l’autre avec des Turtlebots afin d’illustre le modèle proposé et sa capacité à vérifier les propriétés. / Despite many years of work in robotics, there is still a lack of established software architecture and middleware for multi-robot systems. A robotic middleware should be designed to abstract the low-level hardware architecture, facilitate communication and integration of new software. This PhD thesis is focusing on middleware for multi-robot system and how we can improve existing frameworks for fleet purposes by adding multi-robot coordination services, development and massive deployment tools. We expect robots to be increasingly useful as they can take advantage of data pushed from other external devices in their decision making instead of just reacting to their local environment (sensors, cooperating robots in a fleet, etc). This thesis first evaluates one of the most recent middleware for mobile robot(s), Robot operating system (ROS) and continues with a state of the art about the commonly used middlewares in robotics. Based on the conclusions, we propose an original contribution in the multi-robot context, called SDfR (Service discovery for Robots), a service discovery mechanism for Robots. The main goal is to propose a mechanism that allows highly mobile robots to keep track of the reachable peers inside a fleet while using an ad-hoc infrastructure. Another objective is to propose a network configuration negotiation protocol. Due to the mobility of robots, classical peer to peer network configuration techniques are not suitable. SDfR is a highly dynamic, adaptive and scalable protocol adapted from Simple Service Discovery Protocol (SSDP). We conduced a set of experiments, using a fleet of Turtlebot robots, to measure and show that the overhead of SDfR is limited. The last part of the thesis focuses on programming model based on timed automata. This type of programming has the benefits of having a model that can be verified and simulated before deploying the application on real robots. In order to enrich and facilitate the development of robotic applications, a new programming model based on timed automata state machines is proposed, called ROSMDB (Robot Operating system Model Driven Behaviour). It provides model checking at development phase and at runtime. This contribution is composed of several components: a graphical interface to create models based on timed automata, an integrated model checker based on UPPAAL and a code skeleton generator. Moreover, a ROS specific framework is proposed to verify the correctness of the execution of the models and to trigger alerts. Finally, we conduct two experiments: one with a fleet of Parrot drones and second with Turtlebots in order to illustrates the proposed model and its ability to check properties.

Modern software is built by teams of developers that work in a collaborative environment. The goal of this kind of development is that multiple developers can work in parallel. They can alter a set of shared artifacts and inspect and integrate the source code changes of other developers. For example, bug fixes, enhancements, new features or adaptations due to changing environment might be integrated into the system release. At a technical level, a collaborative development process is supported by version control systems. Since these version control systems allow developers to work in their own branch, merging and integration have become an integral part of the development process. These systems use automatic and advanced merging techniques to help developers to merge their modifications in the development repositories. However, these techniques do not guarantee to have a functional system. While the use of branching in the development process offers numerous advantages, the activity of merging and integrating changes is hampered by the lack of comprehensive support to assist developers in these activities. For example, the integration of changes can have an unexpected impact on the design or behavior of the system, leading to the introduction of subtle bugs. Furthermore, developers are not supported when integrating changes across branches (cherry picking), when dealing with branches that have diverged, when finding the dependencies between changes, or when assessing the potential impact of changes. In this dissertation we present an approach that aims at alleviating these problems by providing developers and, more precisely, integrators with semi-automated support for assisted integration within a branch and across branches. We focus on helping integrators with their information needs when understanding and integrating changes by means of characterizations of changes and streams of changes (i.e., sequence of successive changes within a branch) together with their dependencies. These characterizations rely on the first-class representation of systems' histories and changes based on program entities and their relationships rather than on files and text. For this, we provide a family of meta-models (Ring, RingH, RingS and RingC) that offer us the representation of program entities, systems' histories, changes and their dependencies, along with analyses for version comparison, and change and dependency identification. Instances of these meta-models are then used by our proposed tool support to enable integrators to analyze the characterizations and changes. Torch, a visual tool, and JET, a set of tools, actually provide the information needs to assist integration within a branch and across branches by means of the characterization of changes and streams of changes respectively.

Face à l'augmentation de la taille et de la complexité des systèmes logiciels, il convient de les décrire à un plus haut niveau d'abstraction (\ie au-delà du code) avant de concrètement les implémenter. Toutefois, l'utilisation de ces descriptions de haut niveau dans les processus de construction et de vérification des systèmes reste très rudimentaire, ne permettant pas de véritablement guider et faciliter le développement logiciel. Cette thèse propose une nouvelle approche pour rendre plus simple et plus sûr le développement de systèmes logiciels. Cette approche repose sur l'utilisation de langages dédiés et sur un couplage fort entre une couche de spécification et d'architecture et une couche d'implémentation. Elle consiste tout d'abord à décrire à un haut niveau d'abstraction différents aspects, à la fois fonctionnels et non fonctionnels, d'un système dans la couche de spécification et d'architecture. Ces descriptions sont ensuite analysées et utilisées pour personnaliser la couche d'implémentation, afin de faciliter la construction et la vérification du système logiciel. Nous illustrons notre approche dans le domaine de l'informatique ubiquitaire. À la suite d'une analyse complète du domaine, nous avons conçu deux langages dédiés à l'orchestration d'objets communicants, Pantaxou et Pantagruel.

L'objectif de cette recherche est de bâtir un répertoire descriptif généralisé des structures interrogatives directes du français. Le travail est pluridisciplinaire : linguistique, informatique, documentation. La partie linguistique consiste à dresser un répertoire descriptif formel dans lequel toutes les propriétés pertinentes concernent l'interrogation. Ces propriétés doivent être suffisamment abstraites pour que n'importe quel formalisme puisse les incorporer au besoin. L'implémentation sous forme d'un répertoire vise ensuite l'incorporation des contraintes apportées par la description linguistique. Enfin, nous proposons une consultation de bases de données à visée linguistique, qui est reliée par interface à l'analyse informatique.

C++ est un des langages de programmation les plus utilisés en pratique, y compris pour le logiciel embarqué critique. C'est pourquoi la vérication de programmes écrits en C++ devient intéressante, en particulier via l'utilisation de méthodes formelles. Pour cela, il est nécessaire de se fonder sur une sémantique formelle de C++. De plus, une telle sémantique formelle peut être validée en la prenant comme base pour la spécication et la preuve d'un compilateur C++ réaliste, afin d'établir la confiance dans les techniques usuelles des compilateurs C++. Dans cette thèse, nous nous focalisons sur le modèle objet de C++. Nous proposons une sémantique formelle de l'héritage multiple en C++ comprenant les structures imbriquées à la C, sur laquelle s'appuie notre étude de la représentation concrète des objets avec optimisations des bases vides, à travers des conditions suffisantes que nous prouvons correctes vis-à-vis des accès aux champs et des opérations polymorphes. Puis nous spécifions un algorithme de représentation en mémoire fondé sur l'ABI pour Itanium, et une extension de cet algorithme avec optimisations des champs vides, et nous prouvons qu'ils satisfont nos conditions. Nous obtenons alors un compilateur vérifié et réaliste d'un sous-ensemble de C++ vers un langage à trois adresses et accès mémoire de bas niveau. Rajoutant à notre sémantique la construction et la destruction d'objets, nous étudions leurs interactions avec l'héritage multiple. Cela nous permet de formaliser la gestion de ressources, notamment le principe RAII (resource acquisition is initialization) via l'ordre de construction et destruction des sous-objets. Nous étudions aussi les effets sur les opérations polymorphes telles que la sélection de fonction virtuelle pendant la construction et la destruction, en généralisant la notion de type dynamique. Nous obtenons alors un compilateur vérifié pour notre sémantique étendue, notamment en prouvant la correction de l'implémentation des changements de types dynamiques. Toutes nos spécifications et preuves sont formalisées en Coq.

Cette thèse propose une nouvelle approche du parallélisme et de la concurrence, posant les bases d'un langage de programmation à la fois sûr et "secure" (garantissant la sécurité des données), fondé sur une sémantique formelle claire et simple, tout en étant adapté aux architectures multi-cores. Nous avons adopté le paradigme synchrone, dans sa variante réactive, qui fournit une alternative simple à la programmation concurrente standard en limitant l'impact des erreurs dépendant du temps ("data-races"). Dans un premier temps, nous avons considéré un langage réactif d'orchestration, DSL, dans lequel on fait abstraction de la mémoire (Partie 1). Dans le but de pouvoir traiter la mémoire et la sécurité, nous avons ensuite étudié (Partie 2) un noyau réactif, CRL, qui utilise un opérateur de parallélisme déterministe. Nous avons prouvé la réactivité bornée des programmes de CRL. Nous avons ensuite équipé CRL de mécanismes pour contrôler le flux d'information (Partie 3). Pour cela, nous avons d'abord étendu CRL avec des niveaux de sécurité pour les variables et les évènement, puis nous avons défini dans le langage étendu, SSL, un système de types permettant d'éviter les fuites d'information. Parallèlement (Partie 4), nous avons ajouté la mémoire à CRL, en proposant le modèle DSLM. En utilisant une notion d'agent, nous avons structuré la mémoire de telle sorte qu'il ne puisse y avoir de "data-races". Nous avons également étudié l'implémentation de DSLM sur les architectures multi-cores, fondée sur la notion de site et de migration d'un agent entre les sites. L'unification de SSL et de DSLM est une piste pour un travail futur.