L'interopérabilité des applications est devenue le leitmotiv des développeurs et concepteurs en ingénierie système. La plupart des approches pour l'interopérabilité existant dans l'entreprise ont pour objectif principal l'ajustement et l'adaptation des types et structures de données nécessaire à la mise en œuvre de collaboration entre entreprises. Dans le domaine des entreprises manufacturières, le produit est une composante centrale. Des travaux scientifiques proposent des solutions pour la prise en compte des systèmes d'information issus des produits, tout au long de leur cycle de vie. Mais ces informations sont souvent non corrélées. La gestion des données de produit (PDM) est couramment mise en œuvre pour gérer toute l'information relative aux produits durant tout leur cycle de vie. Cependant, ces modèles sont généralement des "îlots" indépendants ne tenant pas compte de la problématique d'interopérabilité des applications supportant ces modèles. L'objectif de cette thèse est d'étudier cette problématique d'interopérabilité appliquée aux applications utilisées dans l'entreprise manufacturière et de définir un modèle ontologique de la connaissance des entreprises relatives aux produits qu'elles fabriquent, sur la base de leurs données techniques. Le résultat de ce travail de recherche concerne la formalisation d'une méthodologie d'identification des informations de gestion techniques des produits, sous la forme d'une ontologie, pour l'interopérabilité des applications d'entreprises manufacturières, sur la base des standards existants tels que l'ISO 10303 et l'IEC 62264. / In recent years, the enterprise applications interoperability has become the leitmotiv of developers and designers in systems engineering. Most approaches to interoperability in the company have the primary objective of adjustment and adaptation of types and data structures necessary for the implementation of collaboration between companies. In the field of manufacturing, the product is a central component. Scientific works propose solutions taking into account information systems derived from products technical data throughout their life cycle. But this information is often uncorrelated. The management of product data (PDM) is commonly implemented to manage all information concerning products throughout their life cycle. The modelling of management and manufacturing processes is widely applied to both physical products and services. However, these models are generally independent “islands” ignoring the problem of interoperability between applications that support these models. The objective of this thesis is to study the problem of interoperability applied to applications used in the manufacturing environment and to define a model of the ontological knowledge of enterprises related to the products they manufacture, based on technical data, ensuring the interoperability of enterprise systems. The outcome of this research concerns the formalization of a methodology for identifying a product-centric information system in the form of an ontology, for the interoperability of applications in manufacturing companies, based on existing standard such as ISO 10303 and IEC 62264.

Pour des systèmes mécaniques fortement sollicités et lubrifiés (en roulement avec ou sans glissement), les performances des lubrifiants se caractérisent par l’évolution de l’usure des surfaces. Celle-ci peut se manifester par un micro-écaillage qui conduit à une dégradation des fonctionnalités des surfaces. Pour quantifier la durabilité du mécanisme, il est donc important de pouvoir caractériser l’usure du contact : quantifiable à l’échelle du composant par la mesure de la perte de masse par exemple. Notre approche tentera de caractériser l’usure des surfaces dans ses premières heures de fonctionnement (phase de rodage) se manifestant par des modifications locales de la rugosité et non par la perte de masse qui est peu significative. Notre étude a pour objectif d’établir une relation entre l’évolution des paramètres surfaciques durant cette phase de rodage et la résistance à l’usure des surfaces. Des paramètres tridimensionnels sont ainsi identifiés, permettant de connaître assez tôt, les performances des lubrifiants la fin de longs essais d’endurance. / For lubricated mechanical systems and working with heavy loading (rolling with or without sliding), the lubricants performances are characterized by the evolution of the wear on surfaces. This wear can take the form of micro-pitting which leads to a functional surface degradation. To quantify the durability of the mechanism, it is thus important to be able to characterize the wear of the contact: quantifiable on the scale of the component by the measure of the loss of mass for example. Our approach stands to characterize the wear of surfaces during the first hours of functioning (running-on phase), showing itself by local modifications of the roughness and not by the loss of mass which insignificant. Our study has for objective to establish a relation between the evolution of the surface parameters during the running-in phase and the wear of the surfaces. Tridimentional parameters are so identified, to know early enough the performances of lubricants, without waiting the end of long endurance tests.

Comme les syst`emes mat´eriels et logiciels grandissent de fa¸con continue en ´echelle et fonctionnalit´es, la probabilit´e d’erreurs subtiles de- vient toujours plus grande. Les techniques d’abstraction, souvent bas´ees sur l’interpr´etation abstraite de Cousot, fournissent une m´ethode pour ex´ecuter symboliquement les syst`emes en utilisant le domaine abstrait `a la place du domaine concret. Dans cette th`ese, on introduit des techniques d’abstraction pour les logiques sous des interpr´etations multi-valu´ees. Beaucoup d’applications des logiques multi-valu´ees ont ´et´e trouv´ees dans la v´erification du mat´eriel et du logiciel. Pour la v´erification du mat´eriel, des outils de simulation et des r´ealisations des circuits multi-valu´es v´eritables ont ´et´e propos´es, les risques dynamiques ont ´et´e model´es en introduisant des ´etats faux pour trouver des r´egions chevauchantes des signaux en concurrence, etc. Pour la v´erification du logiciel on a besoin d’incertitude parce qu’on ne peut savoir si certains comportements devraient ˆetre possibles et on a besoin du d´esaccord parce que l’on peut avoir des acteurs diff´erents qui sont en d´esaccord pour la mani`ere dont les syst`emes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d’´equivalence et apr`es, les symboles pr´edicatifs de la logique sont red´efinis `a s’appliquer cor- rectement aux classes d’´equivalence `a l’aide des politiques d’interpr´etation. On fournit des r´esultats de pr´eservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multi-valu´ees pour la logique temporelle, nous pr´esentons une ´etude de cas pour utiliser l’abstraction dans le contexte des mod`eles du contrˆole d’acc`es. Nous fournirons aussi une technique d’abstraction pour les types de do- nn´ees. Cette technique d’abstraction peut ˆetre ´elargie pour les types abstraits de donn´ees. Ici, les abstractions sont appliqu´ees aux sp´ecifications initiales au moyen des ´equations et ils sont appel´es des abstractions ´equationnelles. De plus, la technique d’abstraction pr´esent´ee g´en´eralise et clarifie la nature de beaucoup de techniques d’abstraction trouv´ees dans la litt´erature, telles: la technique de dupliquer les symboles pr´edicatifs, shape analysis, l’abstraction par pr´edicats, l’approche de McMillan, etc. Pour raisonner au sujet des syst`emes dynamiques, on introduit les types de donn´ees dynamiques et on ´etend la m´ethode d’abstraction ant´erieure `a ce cas. Le probl`eme principal qui survient quand on utilise les abstractions est de trouver l’abstraction convenable ou de raffiner une abstraction d´ej`a existante pour en obtenir une meilleure. On prouve que les techniques d’abstraction que nous avons introduites pour les types de donn´ees sous l’interpr´etation 3- valu´ee Kleene, peuvent ˆetre utilis´ees dans une proc´edure de raffinement. De plus, on montre que la proc´edure de raffinement guid´e par contre-exemple est plus efficace quand on l’utilise sous les abstractions ´equationnelles / As the hardware and software systems are growing continuously in scale and functionality, the likelihood of subtle errors becomes greater. Abstraction techniques, often based on abstract interpretation, provide a method for symbolically executing systems using the abstract instead of the concrete domain. In this thesis, we are concerned with abstractions for logics under multi-valued interpretations. Many applications of multi-valued logics have been found in hardware and software verification. For hardware verification, simulation tools and imple- mentations of genuinely multi-valued circuits have been proposed, dynamic hazards have been modeled by introducing pseudo states to find overlapping regions of competing signals, implementation of gates have been verified on the basis of switch level models, etc. For software verification, we need uncer- tainty because we may not know whether some behaviors should be possible, we need disagreement because we may have different stakeholders that dis- agree about how the systems should behave and we need to represent relative importance because some behaviors are essential and others may or may not be implemented. The abstractions are obtained by applying equivalence relations and then, the predicate symbols of the logic are re-defined to work properly on equiva- lence classes by using interpretation policies. We provide preservation results for first-order logic, temporal logic, and temporal logic of knowledge. As a case study, we show how abstraction can be used to solve the safety problem for protection systems which model access control policies. The use of abstraction in the context of data types, is also investigated. This technique scales well from data types to abstract data types. Here, abstractions are applied to initial specifications by means of equations and they are called equationally specified abstractions. Moreover, the abstraction technique we propose generalizes and clarifies the nature of many abstraction techniques found in the literature, such as the technique of duplicating pred- icate symbols, shape analysis, predicate abstraction, McMillan’s approach, etc. To reason about dynamic systems, we introduce dynamic data types and extend the previous abstraction technique to this case. The main problem that arises when using abstraction techniques is to find the suitable abstraction or to refine an already existing abstraction in order to obtain a better one. In this thesis, we prove that the abstraction techniques for data types, under Kleene’s three-valued interpretation, can be used in a refinement procedure. Moreover, we show that the counterexample guided abstraction refinement procedure (CEGAR) works better when used with equationally specified abstractions

Dans cette thèse, nous nous intéressons au calcul d'ordonnanceurs pour les systèmes hybrides. En fait, nous considérons deux sous-classes des systèmes hybrides, les systèmes temps-réels où des tâches doivent se partager l'accès à une ressource commune, et les systèmes à commutations où un choix doit être fait sur les dynamiques à choisir en fonction d'objectifs à atteindre. Dans la première partie de cette thèse, nous nous intéressons aux problèmes d'ordonnancement et prenons comme étude de cas l'ordonnancement de tâches périodiques sur des architectures multiprocesseurs. Nous nous intéressons plus particulièrement à déterminer si l'on peut modifier certaines valeur des paramètres du système tout en respectant les contraintes temporelles sans changer d'ordonnanceur. La méthode inverse permet de prouver de manière formelle la robustesse des systèmes temporisés paramétriques. Nous introduisons une méthode de réduction du nombre d'états nécessaire à la vérification. Cette réduction nous permet de traîter des études de cas intéressantes telle que celle proposée par Astrium EADS pour le lanceur Ariane 6. Nous montrons également comment la Cartographie Comportementale, une extension de la méthode inverse, permet de trouver la zone de l'espace des paramètres où l'on a l'existence d'un ordonnancement satisfaisant les contraintes temporelles. Nous comparons cette approche avec une méthode analytique pour montrer l'intérêt de notre approche. Dans la seconde partie de cette thèse, nous nous intéressons au contrôle de systèmes affines à commutation. Ces systèmes sont gouvernés par une famille d'équations différentielles linéaires et le contrôleur peut choisir laquelle va gouverner le système pendant le prochain pas de temps. Dans ce cadre, le contrôle peut être vu comme l'ordonnancement des dynamiques que le système va prendre. Le choix de la dynamique peut se faire pour des objectifs de stabilité ou d'accessibilité. Nous proposons une nouvelle méthode qui calcule un contrôleur dont la stratégie est la même pour des ensembles denses de points. Notre méthode utilise le calcul en avant, souvent préférable au calcul à rebours pour les systèmes contractants. Nous montrons que, sous certaines conditions, le système contrôlé évolue vers un comportement limite. Nous appliquons notre méthode sur plusieurs études de cas issues de la littérature ainsi qu'un exemple réel, un prototype de convertisseur de tension multiniveaux. Enfin, nous montrons que notre méthode s'étend aux systèmes comportant des perturbations ainsi qu'aux systèmes non linéaires. / In this thesis, we are interested in designing schedulers for hybrid systems. We consider two specific subclasses of hybrid systems, real-time systems where tasks are competing for the access to common resources, and sampled switched systems where a choice has to be made on dynamics of the system to reach goals. Scheduling consists in defining the order in which the tasks will be run on the processors in order to complete all the tasks before a given deadline. In the first part of this thesis, we are interested in the scheduling of periodic tasks on multiprocessor architectures. We are especially interested in the robustness of schedulers, i.e., to prove that some values of the system parameters can be modified, and until what value they can be extended while preserving the scheduling order and meeting the deadlines. The Inverse Method can be used to prove the robustness of parametric timed systems. In this thesis, we introduce a state space reduction technique which allows us to treat challenging case studies such as one provided by Astrium EADS for the launcher Ariane 6. We also present how an extension of the Inverse Method, the Behavioral Cartography, can solve the problem of schedulability, i.e., finding the area in the parametric space in which there exists a scheduler that satisfies all the deadlines. We compare this approach to an analytic method to illustrate the interest of our approach In the second part of this thesis, we are interested in the control of affine switched systems. These systems are governed by a finite family of affine differential equations. At each time step, a controller can choose which dynamics will govern the system for the next time step. Controlling in this sense can be seen as a scheduling on the order of dynamics the system will have to use. The objective for the controller can be to make the system stay in a given area of the state space (stability) or to reach a given region of the state space (reachability). In this thesis, we propose a novel approach that computes a scheduler where the strategy is uniform for dense subsets of the state space. Moreover, our approach only uses forward computation, which is better suited than backward computation for contractive systems. We show that our designed controllers, systems evolve to a limit cyclic behavior. We apply our method to several case studies from the literature and on a real-life prototype of a multilevel voltage converter. Moreover, we show that our approach can be extended to systems with perturbations and non-linear dynamics.

Les nouveaux algorithmes présentés dans cette thèse contribuent à la thématique générale de la simplification des modèles biologiques : le calcul de bases creuses de lois de conservation, la simplification des systèmes d'équations différentielles paramétriques, fréquents en modélisation, et le reverse engineering des modèles. Les algorithmes de cette thèse sont basés sur de l'algèbre linéaire exacte. Le chapitre 2 présente un algorithme glouton exact et garanti permettant de calculer une base la plus creuse parmi toutes les bases d'un espace vectoriel. On l'applique au calcul de lois de conservation de modèles biologiques. Dans le chapitre 3, une variante de cet algorithme utilise la résolution de plusieurs programmes linéaires (avec l'algorithme du simplexe) en variables réelles. Cette variante permet de calculer des bases creuses sans garantir qu'elles soient complètes ou les plus creuses. Le chapitre 4 présente un algorithme permettant de calculer une base la plus creuse modulo un espace vectoriel. Il permet de simplifier des fractions rationnelles en effectuant des changements de variables. Enfin, le chapitre 5 présente un algorithme qui, dans le cas où l'ensemble des lois de conservation d'un modèle biologique n'admet pas de base complète de lois à coefficients positifs, suggère des modèles enrichis d'une ou plusieurs espèces. / The new algorithms introduced in this thesis contribute to the general theme of simplification of biological model : the computation of sparse bases of conservation laws, the simplification of parametric systems of differential equations, frequent in modelling, and the reverse engineering of models. The algorithms of this thesis are based on exact linear algebra. The chapter 2 introduces a greedy, exact and guaranteed algorithm which allows to compute a sparsest basis among all the bases of a vector space. We apply it to the computation of conservation laws of biological models. In the chapter 3, a variant of this algorithm uses the resolution of several linear programs (with the simplex algorithm) in real variables. This variant allows to compute sparse bases without guarantee they are complete or sparsest. The chapter 4 introduces an algorithm which allows to compute a sparsest basis modulo a vector space. It was developed with the aim to simplify rational fractions using changes of variables. The chapter 5 introduces an algorithm which suggests models enriched of one or several species, in the case where the set of conservation laws does not admit a complete basis of laws with nonnegative coefficients.

Le développement croissant de l’urbanisme et des activités anthropiques fait peser une pression de plus en plus importante sur les zones côtières, touchant particulièrement les régions méditerranéennes. Les processus liés au changement climatique et aux activités humaines impactent en profondeur les écosystèmes marins et tout particulièrement les systèmes planctoniques qui présentent une sensibilité accrue aux perturbations du milieu. Toutefois, les effets de ces processus agissant de concert à long terme sur la structure et le fonctionnement des écosystèmes côtiers sont encore mal compris. Ainsi, les séries temporelles planctoniques représentent des outils précieux pour la compréhension des processus impactant le milieu marin. Les séries temporelles du laboratoire EBMA-PROTEE de Toulon font partie des séries les plus anciennes de Méditerranée et présentent l’intérêt de combiner l’impact des processus naturels et anthropiques sur les communautés phyto- et zooplanctoniques. C’est dans ce contexte que ce travail a pour objectif de préciser le rôle de ces facteurs sur la dynamique et la composition phyto- et zooplanctonique en Méditerranée nord-occidentale (Toulon, France). Une première partie a ainsi consisté à évaluer le rôle des mélanges verticaux se produisant au sein du bassin Ligure, comme moteur de la dynamique printanière du plancton au sein de la Rade de Toulon. Cette étude a permis d’identifier des variations significatives du régime des précipitations associées à des modifications de la salinité au sein du site de la Grande Rade de Toulon (« LaB ») sur la période 2005-2013. Variations retrouvées également sur 2 autres sites côtiers du bassin Ligure (« SOFCOM » and « Point B »). Conformément à l’hypothèse énoncée, les années conditionnées par un automne et un hiver secs ont présenté en moyenne une production phytoplanctonique printanière supérieure au sein des 3 sites, comparées aux années les plus humides. Toutefois, la présence de différences entre les sites a souligné l’impact important de mécanismes locaux sur le conditionnement de la dynamique phytoplanctonique. L’impact des changements de régime des précipitations sur la composition micro-phytoplanctonique et méso-zooplanctonique a été étudié au cours d’une seconde partie. Les résultats ont suggéré un changement profond des communautés phytoplanctoniques lié à l’augmentation des précipitations, impactant également la structure des communautés zooplanctoniques. Ainsi, ces résultats semblent indiquer que les précipitations interviennent au sein de deux processus, impactant différemment les communautés planctoniques : d’une part, une absence de précipitations participerait à la mise en place de mélanges hivernaux et à la fertilisation des eaux de surfaces au sein de bassin Ligure profitant à la rade de Toulon; d’autre part, les changements dans la composition phytoplanctonique ont évoqué la mise en place d’un processus d’eutrophisation durant les périodes pluvieuses, alimenté par les apports des rivières locales. En parallèle de cet aspect temporel, le suivi de la Petite et Grande Rade de Toulon caractérisés par un degré différent de la pression anthropique a permis, au cours d’une troisième partie, de tester le potentiel des compartiments phyto- et zooplanctoniques en tant qu’indicateur de l’augmentation de la pression anthropique. Cette étude a identifié une sensibilité accrue de la composition du zooplancton par rapport au phytoplancton. Enfin, des indicateurs de pression anthropique des zones côtières, basés sur les familles de copépodes, ont été proposés. / The growing development of urbanism and anthropogenic activities is source of increasing environmental pressure on marine coastal area and especially the Mediterranean Sea. Both human activities and climate change deeply impact marine ecosystems and particularly planktonic systems, which were sensitive to environmental change. However, the combined effect of these two processes on coastal systems functioning and structure over time remains poorly understood. Therefore, planktonic time series provide powerful tools for investigating the impacts of these perturbations. The PROTEE-EBMA laboratory planktonic time series from Toulon (France) are among the oldest from the Mediterranean Sea and provide records of effects for both natural and anthropogenic pressures on planktonic communities. In the context of global change, the present work aim to determine the role of these factors on dynamic and composition of phyto- and zooplankton in NW Mediterranean (Toulon, France). The first part focused on the role of vertical mixing in the Ligurian Sea as inter annual variation driver of the spring plankton bloom in Toulon Bay. The results revealed significant shifts in precipitation regime associated with salinity change into the Large Bay (Toulon) over the period 2005-2013. Same changes were observed into 2 Ligurian basin sites (”SOFCOM” and “Point B”). According to previous hypothesis, spring blooms of phytoplankton conditioned by dry autumns and winters were on average more intense than those from wet conditions. However, differences among sites highlighted importance of local drivers affecting phytoplanktonic dynamics. The second part aimed to investigate impact of precipitation and salinity changes on plankton composition. Results showed a dramatic change in phytoplankton community composition triggering by increasing precipitations and consequently lower salinity and subsequently leading to zooplankton community shifts. In addition, these results suggested that precipitation involved in two specific processes, affecting in a different manner the plankton communities: firstly, low precipitation could contribute on the triggering of winter mixing and thus in surface water fertilization of the Ligurian Basin impacting the Toulon Bays. On the other hand, phytoplankton community shifts also suggested a developing eutrophication processes in Toulon Bay during important precipitation periods driven by increasing local river inputs. In the third part, impact of anthropogenic pressure on both phyto- and zooplankton communities was investigated based on monitoring of two neighboring coastal systems characterized by distinct levels of human activities. Zooplankton communities showed higher sensibility to anthropogenic activities than phytoplankton communities. Finally, indicators of anthropogenic pressure based on copepod families were proposed.

Détection et quantification d’acides nucléiques par l’intercalation de sondes électro-actives appliquée à l’intégration d’approches d’amplifications isothermes in vitro. Détecter et quantifier la présence d’agents pathogènes à travers leur ADN représente un enjeu majeur dans de nombreux secteurs comme l’analyse biomédicale, l’agroalimentaire ou l’environnement. La technique de PCR optique en temps réel, couplant la réaction d’amplification génique in vitro dite PCR à une détection par fluorescence constitue la méthode standard pour réaliser ces analyses. Cependant, elle nécessite l’utilisation d’un thermocycleur et l’intégration d’une instrumentation optique rendant l’équipement onéreux et encombrant. De plus, les échantillons troubles ou colorés ne peuvent pas être traités. Pour remédier aux problèmes posés par l’optique, une méthode de suivi électrochimique de la PCR au moyen de sondes électroactives interagissant préférentiellement avec l’ADN double-brin a été développée au LEM. Un démonstrateur préindustriel réalisé en partenariat avec la start-up Easy Life Science permet la parallélisation des mesures de PCR électrochimique en temps réel dans les 48 cellules d’un consommable. Dans ce travail, la problématique de la régulation thermique est adressée en remplaçant la PCR par deux méthodes d’amplifications isothermes de l’ADN. La première d’entre elles, la LAMP (Loop Mediated Isothermal Amplification), particulièrement efficace et spécifique, est combinée à une détection électrochimique via l’utilisation d’un panel de sondes redox afin d’obtenir des performances analytiques rivalisant avec les méthodes optiques standards. Une seconde approche d’amplification isotherme présentant un schéma réactionnel plus simple que la LAMP, basée sur le recyclage des produits d’une HCR (Hybridization Chain Reaction), est également proposée. Enfin, un nouveau consommable miniaturisé intégrant, à ce jour, cent cellules électrochimiques de faible volume (≤ μL) ainsi que le potentiostat dédié sont présentés. L’originalité de ce consommable repose sur son processus de fabrication à très bas coût n’utilisant que des empilements de supports sérigraphiés. Fonctionnel à température ambiante, l’objectif à terme sera de l’utiliser pour des réactions d’amplifications isothermes dites « digitalisées » / Nucleic acids detection and quantification via electro-active probes intercalation applied to the integration of in-vitro isothermal amplification reactions. Detection and quantification of pathogenic agents through their DNA has become increasingly important in applications such as molecular diagnostics and food safety control to environmental monitoring. Routinely, these analyses are performed using optical quantitative PCR method by coupling the in vitro DNA amplification reaction PCR with fluorescent detection. However, it requires the use of a thermocycler as well as the integration of optical instrumentation leading to a bulky and expensive apparatus, unable to process turbid or colored samples. In order to circumvent these limitations, an alternative electrochemical monitoring method for PCR, based on the use of electro-active probes preferentially binding to double stranded DNA, has been proposed and developed at the LEM. A pre-industrial demonstrator developed in partnership with the start-up Easy Life Science allows the parallelization of real time electrochemical PCR measurements in a custom-made 48 wells plate. This work deals with the thermic regulation problem by replacing PCR by two alternatives isothermal DNA amplification methods. First, the LAMP (Loop Mediated Isothermal Amplification), known to be highly efficient and specific, is combined to an electrochemical detection through the use of a panel of redox probes in order to obtain analytical performances competing with the standard optical techniques. Secondly an isothermal amplification method with a simpler mechanism than LAMP, based on the recycling of the products of an HCR (Hybridization Chain Reaction), is also proposed. Finally, a new miniaturized plate integrating, to date, one hundred low volume (≤ μL) electrochemical cells as well as the corresponding potentiostat are presented. The novelty of this plate relies on its very low cost fabrication process based on the simple assembly of screen-printed films. Although the results presented were at room temperature, in the long term, it is envisioned to monitor isothermal amplification reactions in a “digital” manner

Cette thèse se situe dans la problématique de la conduite en convoi de véhicules autonomes : des ensembles de véhicules qui se déplacent en conservant une configuration spatiale, sans aucune accroche matérielle. Ses objectifs sont d'abord, la définition d'une approche de prise de décision pour les systèmes de convois de véhicules, puis, la définition d'une approche de vérification, adaptée à la preuve de propriétés relatives aux convois de véhicules, avec une attention particulière envers les propriétés de sûreté.L'approche pour la prise de décision est décentralisée et auto organisée : chaque véhicule détermine son comportement de façon locale, à partir de ses propres capacités de perception, sans avoir recours à une communication explicite, de telle sorte que l'organisation du convoi, son maintien et son évolution soient le résultat émergeant du comportement de chaque véhicule. L'approche proposée s'applique a des convois suivant plusieurs types de configuration, et permet des changements dynamiques de configuration.L'approche proposée pour la vérification de propriétés de sûreté des convois de véhicules, adopte le model-checking comme technique de preuve. Pour contourner le problème de l'explosion combinatoire, rencontré dans la vérification des systèmes complexes, nous avons proposé une méthode compositionnelle de vérification, qui consiste a décomposer le système en sous systèmes et à associer une propriété auxiliaire à chacun des sous systèmes. La propriété globale sera ensuite déduite de l'ensemble des propriétés auxiliaires, par l'application d'une règle de déduction compositionnelle. La complexité calculatoire est mieux maîtrisée car le model-checking s'applique aux sous-systèmes. Nous proposons une règle de déduction adaptée aux systèmes de conduite en convoi, en particulier ceux qui sont basés sur des approches décentralisées. La règle considère chaque véhicule comme un composant. Elle est consistante sous la condition que l'ajout d'un nouveau composant au système n'a pas d'influence sur le comportement du reste du système. L'approche décentralisée proposée pour la conduite en convoi satisfait cette condition. Deux propriétés de sûreté ont été vérifiées : absence de collision et évolution confortable pour les passagers / This thesis places in the framework of Platoons, sets of autonomous vehicles that move together while keeping a spatial configuration, without any material coupling. Goals of the thesis are: first, the definition of a decision making approach for platoon systems. Second, the definition of a method for the verification of safety properties associated to the platoon system.The proposed decision making approach is decentralized and self-organized. Platoon vehicles are autonomous, they act based only on their perception capabilities. The configuration emerges as a result of the individual behavior of each of the platoon vehicle. The proposed approach can be applied to platoon with different configurations, and allows for dynamic change of configuration.The proposed verification method uses the model-checking technique. Model checking of complex system can lead to the combinatory explosion problem. To deal with this problem, we choose to use a compositional verification method. Compositional methods decompose system models into different components and associate to each component an auxiliary property. The global property can then be deduced from the set of all the auxiliary properties, by applying a compositional deduction rule. We define a deduction rule suitable for decentralised platoon systems. The deduction rule considers each vehicle as a component. It is applicable under the assumption that adding a new component to an instance of the system does not modify behavior of the instance. Two safety properties have been verified : collision avoidance.

De nombreux systèmes physiques peuvent être décrits par des modèles unidimensionnels (1D). C'est le cas de certains gaz d'atomes ultrafroids: dans les bonnes conditions leur dynamique a lieu suivant une seule dimension spatiale.<br />Je me suis intéressée à l'étude de quelques aspects des systèmes intégrables à 1D. D'abord je présente une étude de l'état fondamental d'un système de fermions 1D à 2 composants en interactions de contact répulsives. J'utilise l'ansatz de Bethe pour calculer le diagramme de phase du système homogène. Je prends ensuite en compte un piège harmonique et je montre que les atomes s'organisent en deux couches: une phase partiellement polarisée se trouve au centre du piège et une phase totalement polarisée aux bords.<br />Ensuite j'étudie des corrections dues aux effets de taille finie au gap du spectre d'excitations du modèle d'Hubbard 1D. J'obtiens deux termes correctifs aux résultats de la limite thermodynamique: un en loi de puissances inverses en la taille du système L, et un second exponentiel en L. Dans le régime de faible interaction ce deuxième terme peut être important.<br />Finalement j'étudie la réponse d'un système excité à la modulation temporelle de l'interaction entre atomes. Je considère le modèle de Lieb-Liniger et le modèle non-intégrable d'un gaz de fermions avec une impureté mobile. Je montre que le système non-intégrable est sensible à des excitations de fréquences de l'ordre de l'espacement moyen entre niveaux d'énergie, tandis que le système intégrable n'est excité que par des fréquences beaucoup plus grandes. Cet effet peut être utilisé comme test d'intégrabilité dans des systèmes mésoscopiques 1D et pourrait être observé expérimentalement.

Le but de ce travail est de montrer qu'il est possible de concilier sécurité et flexibilité dans un noyau de système d'exploitation. Nous démontrons qu'il est possible de garantir à la fois la flexibilité et la sécurité d'un système, en séparant la gestion de la politique de sécurité des outils servant à sa mise en oeuvre. Notre travail se découpe en deux partie. Dans la première nous proposons des outils élémentaires de protection ayant pour rôle de protéger le système contre certains types d'attaques choisis tout en restant totalement indépendants de la politique de sécurité mise en oeuvre dans le système. Dans la deuxième partie nous présentons le canevas logiciel sécurisé que nous avons implanté, et notamment le composant chargé de la gestion des politiques de sécurité que nous appelons gestionnaire de sécurité. Nos résultats sont validés sur des exemples mettant en évidence la flexibilité de la protection dans le système.