Nous étudions la stratification de Newton des variétés de Shimura de type PEL aux places de bonne réduction. Nous considérons la strate basique de certaines variétés de Shimura simples de type PEL modulo une place de bonne réduction. Sous des hypothèses simplificatrices nous prouvons une relation entre la cohomologie l-adique de ce strate basique et la cohomologie de la variété de Shimura complexe. En particulier, nous obtenons des formules explicites pour le nombre de points dans la strate basique sur des corps finis, en termes de représentations automorphes. Nous obtenons les résultats à l'aide de la formule des traces et de la troncature de la formule de Kottwitz pour le nombre de points sur une variété de Shimura sur un corps fini. Nous montrons, en utilisant la formule des traces, que n'importe quelle strate de Newton d'une variété de Shimura de type PEL de type (A) est non vide en une place de bonne réduction. Ce résultat a déjà été établi par Viehmann-Wedhorn; nous donnons une nouvelle preuve de ce théorème. Considérons la strate basique des variétés de Shimura associées à certains groupes unitaires dans les cas où cette strate est une variété finie. Alors, nous démontrons un résultat d' équidistribution pour les opérateurs de Hecke agissant sur cette strate. Nous relions le taux de convergence avec celui de la conjecture de Ramanujan. Dans nos formules ne figurent que des représentations automorphes cuspidales sur Gl_n pour lesquelles cette conjecture est connue, et nous obtenons donc des estimations très bonnes sur la vitesse de convergence. En collaboration avec Erez Lapid nous calculons le module de Jacquet d'une représentation en échelle pour tout sous-groupe parabolique standard du groupe général linéaire sur un corps local non-archimédien.

La thèse s'inscrit dans le domaine de la modélisation et de la validation des systèmes modernes complexes. Les systèmes actuels sont en fait d'une complexité sans cesse croissante et formés de plus en plus de composants de natures différentes. Ceci rend leur processus de conception et de validation coûteux et difficile. Il semble être la simple façon permettant de faire face à cette hétérogénéité et à cette complexité est l'approche orientée composant. Suivant cette approche, le système est une entité formée par un ensemble des composants interconnectés. Les composants définissent une interface qui permet d'abstraire leur modèle interne (boîte noire), ce qui favorise la modularité et la réutilisation des composants. L'interaction entre ces composants se fait conformément à un ensemble des règles pré-établies, permettant ainsi d'avoir une vision globale de comportement du système. La conception ainsi que la validation des systèmes modernes reste alors problématique à cause de la nécessité de prendre en compte l'hétérogénéité des différents composants. Dans ce cadre, dans un premier temps, nous définirons un cadre formel générique dans lequel une large famille de formalismes de description de systèmes à base d'états peut être naturellement capturée. Ainsi, nous allons définir un ensemble de règles de composition permettant de mettre en correspondance les différents composants et ainsi de constituer un modèle global du système à concevoir. Dans un second temps, nous proposerons une approche de test d'intégration qui permet de valider le comportement d'un système complexe sous l'hypothèse que chaque composant est testé et validé. Cette approche vise à générer automatiquement des cas de test en s'appuyant sur un modèle global décrit dans notre framework du système sous test.

(Brief abstract written by the author in 2011 since I don't have the original to hand.) This thesis introduced much of the theory for Hoare's CSP, including the failures and failures-divergences model and methods of proving properties of processes based on metric, order and topological structures. The final chapter investigates the structures underlying operational semantics.

Thesis (M.S.)--State University of New York at Binghamton, Department of Computer Science, Thomas J. Watson School of Engineering and Applied Science, 2005. / "This dissertation is a compound document (contains both a paper copy and a CD as part of the dissertation)"--ProQuest abstract document view. Includes bibliographical references.

Les techniques d'analyse et de débogage d'applications sont de plus en plus mises à mal dans les systèmes modernes. En particulier dans les systèmes basés sur des composants embarqués multiprocesseurs (ou MPSoc) qui composent aujourd'hui la plupart de nos dispositifs quotidiens. Le recours à des traces d'exécution devient incontournable pour appliquer une analyse fine de tels systèmes et d'en identifier les comportements divergents. Même si la trace représente une source d'information riche mise à disposition du développeur pour travailler, les informations pertinentes à l'analyse se retrouvent noyées dans la masse et sont difficilement utilisables sans une expertise de haut niveau. Des outils dédiés à l'exploitation des traces deviennent nécessaires. Cependant les outils existants prennent rarement en compte les aspects métiers spécifiques à l'application afin d'optimiser le travail d'analyse. Dans cette thèse, nous proposons une approche qui permet au développeur de représenter, manipuler et interroger une trace d'exécution en se basant sur des concepts liés à ses propres connaissances métier. Notre approche consiste en l'utilisation d'une ontologie pour modéliser et interroger les concepts métier dans une trace, et l'utilisation d'un moteur d'inférence pour raisonner sur ces concepts métier. Concrètement, nous proposons VIDECOM l'ontologie du domaine de l'analyse des traces d'exécution des applications embarquées multimédia sur MPSoC. Nous nous intéressons ensuite au passage à l'échelle de l'exploitation de cette ontologie pour l'analyse des traces de grandes tailles. Ainsi, nous faisons une étude comparative des différents systèmes de gestion des ontologies pour déterminer l'architecture la plus adaptée aux traces de très grande taille au sein de notre ontologie VIDECOM. Nous proposons également un moteur d'inférence qui adresse les défis que pose le raisonnement sur les concepts métier, à savoir l'inférence de l'ordre temporel entre les concepts métier dans la trace et la terminaison du processus de génération de nouvelles connaissances métier. Enfin, nous illustrons la mise en pratique de l'utilisation de l'ontologie VIDECOM dans le cadre du projet SoC-Trace pour l'analyse des traces d'exécution réelles sur MPSoC. / Applications analysis and debugging techniques are increasingly challenging task in modern systems. Especially in systems based on embedded multiprocessor components (or MPSoC) that make up the majority of our daily devices today. The use of execution traces is unavoidable to apply a detailed analysis of such systems and identify unexpected behaviors. Even if the trace offers a rich corpus of information to the developer for her work, information relevant to the analysis are hidden in the trace and is unusable without a high level of expertise. Tools dedicated to trace analysis become necessary. However existing tools take little or no account of the specific business aspects to an application or the developer's business knowledge to optimize the analysis task. In this thesis, we propose an approach that allows the developer to represent, manipulate and query an execution trace based on concepts related to her own business knowledge. Our approach is the use of an ontology to model and query business concepts in a trace, and the use of an inference engine to reason about these business concepts. Specifically, we propose VIDECOM, the domain ontology for the analysis of execution traces of multimedia applications embedded on MPSoC. We then focus on scaling the operation of this ontology for the analysis of huge traces. Thus, we make a comparative study of different ontologies management systems (or triplestores) to determine the most appropriate architecture for very large traces in our VIDECOM ontology.We also propose an inference engine that addresses the challenges of reasoning about business concepts, namely the inference of the temporal order between business concepts in the trace and the termination of the process of generating new knowledge from business knowledge. Finally, we illustrate the practical use of VIDECOM in the SoC-Trace project for the analysis of real execution traces on MPSoC.

Un comportement distribué peut être décrit avec un multi-ensemble partiellement ordonné (pomset). Bien que compacts et très intuitifs, ces modèles sont difficiles à vérifier. La principale technique utilisée dans cette thèse est de ramener les problèmes de décision de la logique MSO sur les pomsets à des problèmes de décision sur les mots. Les problèmes considérés sont la satisfiabilité et la vérification. Le problème de la vérification pour une formule donnée et un pomset consiste à décider si une interprétation est vraie, et le problème de satisfiabilité consiste à décider si un pomset répondant à la formule existe. Le problème de satisfiabilité de MSO sur pomsets est indécidable. Une procédure de semi-décision peut apporter des solutions pour de nombreux cas, en dépit du fait qu'elle peut ne pas terminer. Nous proposons un nouveau modèle, que l'on appelle ⌈-Pomset, pouvant rendre l'exploration des pomsets possible. Par conséquent, si une formule est satisfiable alors notre approche mènera éventuellement à la détection d'une solution. De plus, en utilisant les ⌈-Pomsets comme modèles pour systèmes concurrents, le model-checking de formules ordre partiel sur systèmes concurrents est décidable. Certaines expérimentations ont été faites en utilisant l'outil MONA. Nous avons comparé aussi la puissance expressive de certains modèles classiques de la concurrence comme les traces de Mazurkiewicz avec les ⌈-Pomsets. / Multiset of partially ordered events (pomset) can describe distributed behavior. Although very intuitive and compact, these models are difficult to verify. The main technique used in this thesis is to bring back decision problems for MSO over pomsets to problems for MSO over words. The problems considered are satisfiability and verification. The verification problem for a formula and a given pomset consists in deciding whether such an interpretation exists, and the satisfiability problem consists in deciding whether a pomset satisfying the formula exists. The satisfiability problem of MSO over pomsets is undecidable. A semi-decision procedures can provide solutions for many cases despite the fact that they may not terminate. We propose a new model, so called ⌈-Pomset, making the exploration of pomsets space possible. Consequently, if a formula is satisfiable then our approach will eventually lead to the detection of a solution. Moreover, using ⌈-Pomsets as models for concurrent systems, the model checking of partial order formulas on concurrent systems is decidable. Some experiments have been made using MONA. We compare also the expressive power of some classical model of concurrency such as Mazurkiewicz traces with our ⌈-Pomsets.

A presente pesquisa foi elaborada a partir da minha produção prática em desenho realizada no período de 2009 a 2011. Trata-se de uma reflexão, que busca abarcar a formação dos trabalhos, transcorridos por referências, tais como os documentos de trabalho que englobam as coleções de desenhos e os registros diários. O objeto de pesquisa refere-se à elaboração de reservatórios gráficos formados por múltiplos desenhos que condensam vestígios/experiências e materiais. A pesquisa reuniu considerações sobre as diversas instaurações que envolvem as escolhas materiais, as camadas do fazer e a montagem. / This research was drawn from my practice production in drawing performed in the period from 2009 to 2011. This is a reflection that seeks to encompass the formation of the works, which pass by references such as the working papers including the collections of drawings and the daily entries. The research object concerns the development of graphical shells that are formed from multiple drawings that condense trace/experiences and materials. The survey gathered considerations on the various instaurations which involve the material choices, the making layers and the installation.

A presente pesquisa foi elaborada a partir da minha produção prática em desenho realizada no período de 2009 a 2011. Trata-se de uma reflexão, que busca abarcar a formação dos trabalhos, transcorridos por referências, tais como os documentos de trabalho que englobam as coleções de desenhos e os registros diários. O objeto de pesquisa refere-se à elaboração de reservatórios gráficos formados por múltiplos desenhos que condensam vestígios/experiências e materiais. A pesquisa reuniu considerações sobre as diversas instaurações que envolvem as escolhas materiais, as camadas do fazer e a montagem. / This research was drawn from my practice production in drawing performed in the period from 2009 to 2011. This is a reflection that seeks to encompass the formation of the works, which pass by references such as the working papers including the collections of drawings and the daily entries. The research object concerns the development of graphical shells that are formed from multiple drawings that condense trace/experiences and materials. The survey gathered considerations on the various instaurations which involve the material choices, the making layers and the installation.

The research shows an iconographic survey around some situations, which abandonment can be identified in art representations, firstly through paintings that represent homeless people images, beggars and wanderers, expanding itself later to other imagistic references and artistic languages. My own affective and poetry memory was highly significant for this research; both related to the childhood and beings. Abandonment poetry deals with body gestures, in its presences, absences and fragmentations, allowing us to think about the way the abandonment situations are presented into artistic production during all history, even among our contemporaneity, the context in which we must be aware about its invisibility processes and, above all, in the leftovers, the remains and traces that surround these characters existence. / Esta pesquisa apresenta um levantamento iconográfico em torno das situações em que o abandono pode ser identificado nas representações da arte, inicialmente através de pinturas que apresentam imagens de moradores de rua, pedintes, mendigos e andarilhos, ampliando-se posteriormente para outros referenciais imagéticos e linguagens artísticas. Para esta pesquisa foi significativa minha memória afetiva e poética pessoal, relacionadas desde a infância a essas situações e seres. As poéticas do abandono tratam da gestualidade do corpo, em suas presenças, ausências e fragmentações, permitindo-nos refletir sobre os modos pelos quais as situações de abandono são apresentadas na produção artística ao longo da história, inclusive na contemporaneidade, contexto ao qual devemos estar atentos em seus processos de invisibilidade e, sobretudo, nos restos, resíduos e vestígios que cercam a existência desses personagens. / Mestre em Artes

La thèse s’inscrit dans le domaine de la modélisation et de la validation des systèmes modernes complexes. Les systèmes actuels sont en fait d’une complexité sans cesse croissante et formés de plus en plus de composants de natures différentes. Ceci rend leur processus de conception et de validation coûteux et difficile. Il semble être la simple façon permettant de faire face à cette hétérogénéité et à cette complexité est l’approche orientée composant. Suivant cette approche, le système est une entité formée par un ensemble des composants interconnectés. Les composants définissent une interface qui permet d’abstraire leur modèle interne (boîte noire), ce qui favorise la modularité et la réutilisation des composants. L’interaction entre ces composants se fait conformément à un ensemble des règles pré-établies, permettant ainsi d’avoir une vision globale de comportement du système. La conception ainsi que la validation des systèmes modernes reste alors problématique à cause de la nécessité de prendre en compte l’hétérogénéité des différents composants. Dans ce cadre, dans un premier temps, nous définirons un cadre formel générique dans lequel une large famille de formalismes de description de systèmes à base d’états peut être naturellement capturée. Ainsi, nous allons définir un ensemble de règles de composition permettant de mettre en correspondance les différents composants et ainsi de constituer un modèle global du système à concevoir. Dans un second temps, nous proposerons une approche de test d’intégration qui permet de valider le comportement d’un système complexe sous l’hypothèse que chaque composant est testé et validé. Cette approche vise à générer automatiquement des cas de test en s’appuyant sur un modèle global décrit dans notre framework du système sous test. / In spite of several decades of research, assuring the quality of software systems still represents a major and serious problem nowadays for the industry with respect to both results and costs. This thesis comes within the scope of a proposal centered on a generic unified framework for both complex software systems modeling and testing. The contribution of this paper is then twofold: first, it defines a unified framework for modelling generic components, as well as a formalization of integration rules to combine their behaviour. This is based on a coalgebraic definition of components, which is a categorical representation allowing the unification of a large family of formalisms for specifying state-based systems. Second, it studies compositional conformance testing i.e. checking whether an implementation made from correct interacting components combined with integration operators conforms to its specification