Cette thèse développe des outils permettant de prouver qu’un système dynamique est sûr. En supposant qu’une partie de l’espace d’état est dangereuse, un système dynamique est dit sûr lorsque son état n’atteint jamais cette partie dangereuse au cours du temps, quel que soit l’état initial appartenant à un ensemble d’états initiaux admissibles et quel que soit le niveau de perturbation restant dans un domaine admissible. Les outils proposés cherchent à établir des preuves de sûreté pour des systèmes décrits par des modèles dynamiques non-linéaires et des modèles dynamiques hybrides. Prouver qu’un système dynamique est sûr en calculant explicitement l’ensemble des trajectoires possibles du système lorsque le modèle dynamique est non-linéaire et perturbé reste une tâche très difficile. C’est pourquoi cette thèse aborde ce problème à l’aide de fonctions barrières paramétrées. Une barrière, lorsqu’elle existe, permet de partitionner l’espace d’état et d’isoler l’ensemble des trajectoires possibles de l’état du système de la partie dangereuse de l’espace d’état. La fonction paramétrique décrivant la barrière doit satisfaire un certain nombre de contraintes impliquant la dynamique du modèle, l’ensemble des états initiaux possibles, et l’ensemble dangereux. Ces contraintes ne sont pas convexes en général, ce qui complique la recherche de fonctions barrières satisfaisantes. Précédemment, seules des fonctions barrières polynomiales ont été considérées pour des modèles dynamiques polynomiaux. Cette thèse considère des systèmes dynamiques relativement généraux avec des barrières paramétriques quelconques. Les solutions présentées exploitent des outils de satisfaction de contraintes sur des domaines continus et des outils issus de l’analyse par intervalles. Dans un premier temps, cette thèse considère des systèmes dynamiques non-linéaires à temps continu. Le problème de conception d’une barrière paramétrique est formulé comme un problème de satisfaction des contraintes sur des domaines réels avec des variables quantifiées de manière existentielle et universelle. L’algorithme CSC-FPS a été adapté afin de résoudre le problème de synthèse de barrière. Cet algorithme combine une exploration de l’espace des paramètres de la barrière et une phase de vérification des propriétés de la barrière. A l’aide de contracteurs, il est possible de significativement accélérer la recherche de solutions. Dans un second temps, ces résultats sont étendus au cas de systèmes décrits par des modèles dynamiques hybrides. La propriété de sûreté doit être prouvée lors de l’évolution à temps continu du système dynamique, mais aussi pendant les transitions du système. Ceci nécessite l’introduction de contraintes supplémentaires qui lient les fonctions barrières associées à chaque mode à temps continu entre elles. Réaliser la synthèse de toutes les fonctions barrières pour les différents modes simultanément n’est envisageable que pour des systèmes de très petite dimension avec peu de modes. Une approche séquentielle a été proposée. Les contraintes liées aux transitions sont introduites progressivement entre les modes pour lesquels une barrière a déjà été obtenue. Lorsque certaines contraintes de transition ne sont pas satisfaites, une méthode de backtracking doit être mise en œuvre afin de synthétiser des barrières offrant une meilleure prise en compte des contraintes de transition non satisfaites. Ces approches ont été évaluées et comparées avec des techniques de l’état de l’art sur des systèmes décrits par des modèles à temps continu et des modèles hybrides. / This thesis addresses the problem of proving the safety of systems described by non-linear dynamical models and hybrid dynamical models. A system is said to be safe if all trajectories of its state do not reach an unsafe region. Proving the safety of systems by explicitly computing all its trajectories when its dynamic is non-linear or when its behavior is described by an hybrid model with non-linear dynamics remains a challenging task. This thesis considers the barrier function approach to prove the safety of a system. A barrier function, when it exists, partitions the state space and isolates the trajectories of the system starting from any possible initial values of the state and the unsafe part of the state space. The set of constraints, which have to be satisfied by a barrier function are usually non-convex, rendering the search of satisfying barrier functions hard. Previously, only polynomial barrier functions were taken in consideration and for systems with polynomial dynamics. This thesis considers relatively general dynamical systems with generic non-linear barrier functions. The solutions presented are based on template barrier functions, constraint satisfaction problems, and interval analysis. The first part of the thesis focuses on non-linear dynamical systems. The barrier function design problem is formulated as a constraint satisfaction problem that can be solved using tools from interval analysis. This formulation allows one to prove the safety of a non-linear dynamical system by finding the parameters of a template barrier function such that all constraints are satisfied using the FPS-CSC algorithm, which has been adapted and supplemented with contractors to improve its efficiency. The second part of the thesis is dedicated to the design of barrier functions for systems described by hybrid dynamical models. Safety properties have to be proven during the continuous-time evolution of the system, but also during transitions. This leads to additional constraints that have to be satisfied by candidate barrier functions. Solving all the constraints simultaneously to find all the barrier functions is usually computationally intractable. In the proposed approach, the algorithm explores all the locations sequentially. Transition constraints are introduced progressively between the already explored locations. Backtracking to previous location is considered when transition constraints are not satisfied. The efficiency of the proposed approaches has been compared with state-of-the-art solutions.

Afin d'assurer disponibilité et réactivité, de nombreux systèmes distribués reposent sur des bases de données répliquées qui maintiennent des copies (répliques) des données sur différents serveurs. la cohérence constitue un défi important dans la mise en oeuvre des bases de données répliquées. les concepteurs de bases de données repliquées doivent faire un choix difficile entre une cohérence forte, qui guarantit une large gamme d'invariants applicatifs, mais qui est lente et fragile, et une réplication asynchrone, qui assure un bon niveau de disponibilité et de réactivité, mais laisse le programmeur face à de possibles anomalies liées à la concurrence.pour résoudre ce dilemme, des bases de données commerciales et recherche fournissent une cohérence hybride qui permet au programmeur d'exiger une cohérence forte pour certaines opérations, et d'ainsi permettre une synchronisation.cette thèse étudie l'analyse et la mise en oeuvre d'une application et de la cohérence associée, de manière à assurer les invariants de cette application avec un minimum d'exigences de cohérence. les trois principales contributions de cette thèse sont: 1) nous proposons le premier outil d'analyse statique destiné à prouver la validité d'invariants d'applications de base de données à modèle de cohérence hybride. 2) nous présentons la mise en application de notre outil d'analyse dans le cadre de la conception d'un système de fichiers dont la sémantique permet un comportement similaire à posix et à un coût résonable. 3)nous proposons un ensemble de patterns utiles, susceptibles d'aider les développeurs d'application dans l'implémentation d'invariants les plus communs. / Distributed databases take advantage of replication to bring data close to the client, and to always be available. the primary challenge for such databases is to ensure consistency. recent research provide hybrid consistency models that allow the database supports asynchronous updates by default, but synchronisation is available upon request. to help programmers exploit the hybrid consistency model, we propose a set of useful patterns,proof rules, and tool for proving integrity invariants of applications. in the first part, we study a sound proof rule that enables programmers to check whether the operations of a given application semantics maintain the application invariants under a given amount of parallelism. we have developed a smt-based tool that automates this proof, and verified several example applications using the tool. in the second part, we apply the above methodology to the design of a replicated file system.the main invariant is that the directory structure forms a tree. we study three alternative semantics for the file system. each exposes a different amount of parallelism, and different anomalies. using our tool-assisted rules, we check whether a specific file system semantics maintains the tree invariant, and derive an appropriate consistency protocol. in the third part of this thesis, we present three classes of invariants: equivalence, partial order, and single-item generic. each places some constraints over the state. each of these classes maps to a different storage-layer consistency property: respectively, atomicity, causal ordering, or total ordering.

Aujourd'hui, l'exploitation des grands réseaux électriques est de plus en plus complexe du fait de l'augmentation de leur taille. de la présence de lignes d'interconnexion de grande longueur, de l'adoption de nouvelles techniques, de contraintes économiques, politiques et écologiques. Ces facteurs obligent les opérateurs à exploiter ces réseaux près de la limite de stabilité et de sécurité. Les situations de pays à forte croissance de consommation accroissent encore les risques d'apparition du phénomène d'instabilité. Pour éviter ce phénomène, l'étude de stabilité (de tension et des angles) est proposée dans cette thèse. Cette étude est un outil très important pour déterminer la possibilité de transfert de puissance dans le contexte de dérégulation future. Le travail de cette thèse est mené grâce à l'utilisation des techniques d'analyse statique et de simulation dynamique avec les logiciels Matlab et Eurostag. Ces techniques sont appliquées principalement au cas du grand réseau (220 et 500 kV) du Vietnam, du réseau test 500 kV BPA aux Etats Unis et à celui du Massif Central français. Dans ce travail, plusieurs techniques d'analyse statique sont présentées de façon à estimer la marge de stabilité et à identifier les lieux critiques pour la stabilité de tension. Les résultats obtenus sont conformes à l'exploitation réelle du réseau du Vietnam. Puis, la simulation dynamique permet d'étudier tous les comportements du réseau de manière plus détaillée pour n'importe quel régime de fonctionnement. Grâce à ces simulations, la réponse de chaque variable des éléments du réseau est observée; les résultats entre les mesures et les simulations sont comparés ; les composants les plus sensibles à la stabilité de tension sont identifiés ainsi que les origines de l'instabilité (de tension ou des angles). Enfin, la combinaison entre l'analyse statique et la simulation dynamique est réalisée pour tirer avantage des deux analyses. Dans certaines conditions critiques, le réseau électrique peut connaître un phénomène d'instabilité. Ce phénomène peut être évité grâce à l'application de mesures préventives et correctrices. Dans cette thèse, trois méthodes de mesures préventives sont présentées : deux méthodes classiques et une nouvelle méthode. Elles servent à diminuer les risques d'instabilité de tension en régime permanent avant ou après une perturbation en utilisant les techniques de l'optimisation du calcul de répartition de puissance. Une nouvelle méthode de mesure correctrice est également présentée dans cette thèse, elle sert à éviter l'instabilité de tension en utilisant la sensibilité des puissances active et réactive avec la tension. Les nœuds critiques, où la charge doit être délestée, sont déterminés par les analyses statiques. Enfin, les solutions, pour améliorer la stabilité (de tension et des angles) et pour éviter l'instabilité, sont données en utilisant des dispositifs de réglage modernes (FACÎS, compensateur de charge, PSS)

Cette thèse porte sur l'étude théorique et expérimentale des structures en béton armé sous sollicitations statique puis dynamique de type séismique. Une importante recherche bibliographique a été effectuée en vue d'analyser au mieux le comportement dynamique des matériaux ainsi que celui des éléments structuraux. Cette recherche est complétée par l'étude des structures essayées sur table séismique. Les enseignements qui ont été tirés de cette étude préalable, notamment ceux concernant la modification de la rigidité des structures Béton Armé sous chargement alterné et séismique, ont permis d'établir une méthode de calcul (dite ''statique équivalente") pour l'analyse de la tenue aux séismes des structures en Béton Armé. Cette méthode tient compte, en particulier de la non-linéarité du comportement des matériaux. Les réponses au séisme qui ont été obtenues par cette méthode sur des portiques essayés sur table vibrante, concordent de façon très satisfaisante avec les valeurs d'essais.

La détermination des propriétés physiques de l'eau pure, notamment la pression de vapeur saturante en fonction de la température, est un enjeu majeur en humidité et identifié comme tel par le Comité Consultatif de Thermométrie (CCT-WG6) sous-groupe Humidité du Comité Technique de Température (TC-T) afin d'améliorer les incertitudes des références nationales en humidité. A cette fin, le LNE-CETIAT et le LNE-Cnam ont développé conjointement un dispositif expérimental permettant d'accéder au couple température / pression de vapeur saturante de l'eau pure. Le principe est basé sur une mesure statique de la pression et de la température dans une cellule d'équilibre associée à un calorimètre quasi-adiabatique. La gamme de température d'équilibre couverte s'étend de 193,15 K à 373,15 K, correspondant à une pression de vapeur saturante allant de 0,06 Pa à 105 Pa.Ce travail présente la description, la réalisation et la caractérisation métrologique de ce nouveau dispositif expérimentale. Les résultats des mesures expérimentales sont comparés avec les travaux théoriques et expérimentaux les plus récents. Le budget d'incertitude finale prend en compte la contribution de la mesure de pression, de la mesure de température et des effets parasites telles que la transpiration thermique et la pression aérostatique. Grace aux différentes solutions mises en œuvre, la contribution des mesures de température dans le bilan d'incertitude globale est réduite. La part prépondérante reste essentiellement associée à la mesure de pression.

La détermination des propriétés physiques de l’eau pure, notamment la pression de vapeur saturante en fonction de la température, est un enjeu majeur en humidité et identifié comme tel par le Comité Consultatif de Thermométrie (CCT-WG6) sous-groupe Humidité du Comité Technique de Température (TC-T) afin d’améliorer les incertitudes des références nationales en humidité. A cette fin, le LNE-CETIAT et le LNE-Cnam ont développé conjointement un dispositif expérimental permettant d’accéder au couple température / pression de vapeur saturante de l’eau pure. Le principe est basé sur une mesure statique de la pression et de la température dans une cellule d’équilibre associée à un calorimètre quasi-adiabatique. La gamme de température d’équilibre couverte s’étend de 193,15 K à 373,15 K, correspondant à une pression de vapeur saturante allant de 0,06 Pa à 105 Pa.Ce travail présente la description, la réalisation et la caractérisation métrologique de ce nouveau dispositif expérimentale. Les résultats des mesures expérimentales sont comparés avec les travaux théoriques et expérimentaux les plus récents. Le budget d'incertitude finale prend en compte la contribution de la mesure de pression, de la mesure de température et des effets parasites telles que la transpiration thermique et la pression aérostatique. Grace aux différentes solutions mises en œuvre, la contribution des mesures de température dans le bilan d’incertitude globale est réduite. La part prépondérante reste essentiellement associée à la mesure de pression. / The determination of the physical properties of pure water, especially the vapor-pressure curve, is one of the major issues identified by the Consultative Committee for Thermometry (CCT) of the technical committee in thermometry sub-field hygrometry to improve the accuracy of the national references in humidity.In order to achieve this objective, the LNE-CETIAT and the LNE-Cnam have jointly built a facility dedicated to the measurement of the saturation vapor pressure and temperature of pure water. The principle is based on a static measurement of the pressure and the temperature of pure water in a closed, temperature-controlled thermostat, conceived like a quasi-adiabatic calorimeter. The explored temperature range lies between 193,15 K and 373,15 K, and the pressure range between 0,06 Pa and 105 Pa.This work presents a full description of this facility and the preliminary results obtained for its characterization. The obtained results have been compared with available literature data. The final uncertainty budget took into account several components: pressure measurements, temperature measurements and environmental error sources such as thermal transpiration and hydrostatic pressure correction. Thanks to the employment of several technical solutions, the thermal contribution to the overall uncertainty budget is reduced, and the remaining major part is mainly due to pressure measurements.

Il existe plusieurs modèles mathématiques pour décrire le comportement dynamique et acoustique des matériaux poreux. Ces modèles se basent sur l'introduction de plusieurs paramètres géométriques décrivant la structure du matériau poreux. La porosité, la résistivité statique, la tortuosité, les longueurs caractéristiques visqueuse et thermique et la perméabilité thermique sont les paramètres géométriques utilisés par exemple dans le modèle de Johnson-Lafarge. La détermination de ces six paramètres est un problème délicat, mais pourtant nécessaire pour la modélisation des matériaux poreux.Il existe des méthodes directes pour mesurer ces paramètres qui peuvent être plus ou moins couteuses et efficaces. Une alternative efficace et accessible aux méthodes directes est la méthode inverse qui est le sujet de ce mémoire. Cette méthode consiste à utiliser les données recueillies par un tube d'impédance, comme l'impédance de surface, pour remonter aux paramètres géométriques par inversion du modèle de Johnson-Lafarge.

Entre 1950 et 1970, le Québec a connu une période d’effervescence dans le domaine de la construction de bâtiments. De ce nombre se retrouvent plusieurs écoles construites avec de la maçonnerie non armée. En effet, ce matériau a servi dans la construction de murs structuraux ou non structuraux servants à faire la division des pièces dans ces bâtiments ainsi que pour isoler. Par contre, au niveau international, les murs constitués de blocs en béton ont fait mauvaise figure en subissant d’importants dommages principalement dus à un dimensionnement inadéquat. Ce programme de recherche a comme objectif principal de montrer que ce matériau pourvu d’armatures et complètement rempli de coulis permet d’atteindre les niveaux de performance escomptés. Pour y arriver, des essais sous charges cycliques à l’aide de vérins et d’un mur de réaction ont été effectués sur des murs en maçonnerie armée. Puisque les murs sont bien instrumentés, les résultats des essais ont permis d’idéaliser adéquatement le comportement des murs de maçonnerie ainsi que d’identifier les états d’endommagement pour chaque niveau de performance. À l’aide de ce modèle et de la variabilité des paramètres, la performance sismique d’une école typique de 2 étages située à Montréal a été évaluée à l’aide de courbes de fragilité selon l’analyse à bandes multiples. Afin de générer les accélérogrammes, ces derniers sont normalisés au spectre conditionné à la période fondamentale du bâtiment.

L'objectif de ce travail a été d'acquérir une meilleure connaissance de la motricité humaine tant au niveau clinique que fondamentale à travers deux études bien précises. La première portait sur une étude clinique à savoir, l'influence d'injection ciblée de toxine botulique au niveau du couple musculaire rectus fémoris – semitendinosus sur la vélocité mise en jeu au cours de la marche globale d'enfants infirmes moteurs cérébraux (IMC). La deuxième portait quant à elle sur une question plus fondamentale, à savoir, la modélisation biomécanique avancée du système musculo-squelettique au cours de la phase d'appui de la marche. En ce qui concerne l'étude clinique, le but a donc été à la fois biomécanique et clinique. D'un point de vue expérimental, plusieurs étapes ont été nécessaires avant la mise en place du protocole final utilisé à l'heure actuelle. De plus, un long travail d'analyse a été réalisé avec le clinicien responsable de ce projet, le docteur Dohin, afin d'établir et de sélectionner les critères cinématiques et cinétiques qui nous ont semblés pertinents. Ainsi, cette étude a été l'occasion de valider les critères discriminatifs d'évaluation en analyse quantifiée de la marche (AQM) pour des résultats visant à améliorer ou à restaurer la marche chez les enfants infirmes moteurs cérébraux. Au niveau fondamental, le but de notre étude a été la mise en place d'un protocole expérimental et des méthodes de calculs permettant d'évaluer quantitativement le fonctionnement du système ostéo-articulaire et musculaire non pathologique. Pour cela, une modélisation avancée a été développée afin d'appréhender le rôle des différentes structures : géométrie articulaires, ligaments, muscles, dans le fonctionnement des articulations humaines à travers des mouvements tel que la marche. D'un point de vue expérimental, l'acquisition de via points directement sur le sujet, permettant ainsi la personnalisation des bras de levier selon la morphologie de notre sujet, a été une étape importante et originale de notre travail. Afin de vérifier la pertinence de nos bras de levier « personnalisés », nous avons dans un premier temps, utilisé une technique d'optimisation statique « classique » visant à minimiser le critère : sommes des contraintes musculaires au carré. Les résultats obtenus sont tout à fait cohérents avec ceux présentés dans la littérature et avec le mouvement étudié. D'un point de vue modélisation, nous avons décidé d'affiner la représentation numérique du comportement du muscle pour rendre le modèle plus proche de la réalité. Ainsi, le comportement mécanique du complexe musculo-tendineux c'est-à-dire les relations forces longueurs, forces vitesses d'élongations et forces activations ont été prises en compte grâce au modèle rhéologique de Hill. Pour cela une étude bibliographique poussée a été nécessaire afin de cerner les nombreuses contraintes liées aux comportements mécaniques du complexe musculo-tendineux. Suite à cette étude bibliographique, nous avons sélectionné la modélisation mathématique la mieux adaptée à nos besoins. Les équations mathématiques mises en place dans notre travail contiennent donc de nombreux paramètres physiques tel que : la force isométrique maximale, la section physiologique, la longueur optimale de la fibre musculaire, l'angle de pennation, la longueur du tendon à partir de laquelle une force est développé... Une fois les forces musculaires calculées à partir du modèle rhéologiques de type Hill, ces dernières ont été implémentées dans la fonction d'optimisation classique. Plusieurs critères ont été alors testés. Le but étant d'essayer de comprendre l'influence du critère sur nos résultats et lequel serait à utiliser afin de prédire au mieux les forces musculaires mises en jeu au de la phase d'appui de la marche. Puis pour finaliser notre étude, les réactions articulaires au niveau de la cheville et du genou ont été calculées à partir des différentes configurations. Dans un premier temps, à partir des forces musculaires prédites par l'optimisation statique classique puis à partir de l'optimisation statique avec le critère modifié. Ceci nous a permis de voir au niveau de la réaction articulaire l'influence de la prise en compte des paramètres physiologiques des muscles. Cette donnée est très importante dans le domaine de la rééducation fonctionnelle et pour les concepteurs de prothèse.

Ce travail s'inscrit dans le cadre des recherches menées autour de la compilation des langages de classes, notamment Eiffel, et plus généralement des langages à objets à typage statique. Très brièvement, on peut dire que le but de cette thèse revient à tenter de répondre à une question fondamentale: comment mieux compiler les langages à objets, c'est à dire comment avoir des programmes plus rapides et plus sûrs ? Ce travail de recherche est basé en grande partie sur l'analyse statique, abordée via deux axes principaux. Le premier consiste à pouvoir effectuer des contrôles de validité et de cohérence du programme, et ce non seulement sur les programmes finis, mais bien dès le début du développement, de façon à pouvoir assister au maximum les développeurs durant la phase de conception et d'implantation. Le second axe, qui est la substance même de cette thèse, considère l'utilisation des informations apportées par l'analyse statique du système pour améliorer la qualité du code généré. En effet, ces informations offrent des possibilités importantes en terme d'optimisation du code généré, aussi bien par des optimisations liées aux algorithmes que par des optimisations sur les structures de données. Nous proposons et expérimentons une approche basée sur la duplication et la spécialisation du code par analyse globale du système, afin d'implanter de façon efficace les structures de données et le code du programme compilé, notamment en ce qui concerne la liaison dynamique. Nous introduisons ainsi une nouvelle méthode de liaison dynamique, basée sur des arbres de branchement directs, dont les performances sont supérieures ou égales à celles des systèmes actuels classiques à base de tables d'indirection. Cette approche est également étendue à la génération par le compilateur d'un ramasse-miettes automatiquement adapté à l'application compilée. Nous menons aussi certaines études pour évaluer les optimisations permises par l'utilisation massive de l'aliasing dans un compilateur écrit dans un langage de classes, ainsi que des moyens de mieux maîtriser cette technique. Ces travaux sont validés entre autres par le développement d'un compilateur Eiffel nommé SmallEiffel et de ses bibliothèques, qui, très largement diffusés et utilisés, sont devenus The GNU Eiffel Compiler.