Ce document concerne le développement d'un cadre mathématique spécifiant une technologie capable de prendre en charge quelques unes des problématiques relevant du domaine des grands flux de données. Nous proposons de combiner le point de vue ontologique de Newell et celui épistémologique de Floridi d'abstraction pour construire des outils de transformation de modéles au moyen d'un ensemble adéquats de foncteurs au sens de la théorie des catégories de Samuel Eilenberg et Saunders Mac Lane. La méthode de résolution de problème proposée est basée sur un raisonnement d'abstraction temps réel qui produit, en ligne, une réduction d'un grand nombre de données sémantiquement pauvres en une donnée unique équivalente mais sémantiquement plus riche. Le prix à payer pour un tel enrichissement sémantique de l'information est la perte d'information syntaxique (i.e. le phénoméne d'oubli). Nos contributions sont les suivantes: (i) la démonstration que le concept d'observateur unaire de la théorie des observations datées (TOT) de Le Goc joue le même rôle qu'un échantillonneur de Dirac, (ii) la construction de la catégorie $TOT(\mathbb{Z})$, adéquate à la formulation du processus d'abstraction proposé et (iii) la conception de la méthode de résolution de problème TOM4A (timed observations methodology for abstraction) dont une application concrète est présentée visant à découvrir et modéliser le problème complexe de la fraude interne dans le domaine bancaire / This document concerns the development of a theoretical mathematical framework to provide a technology able to manage some of the problematics of the big data flows domain. We propose to combine Newell's ontological and Floridi's epistemological point of views of abstraction to build tools that transform models by the mean of an adequate set of functors according to Samuel Eilenberg and Saunders Mac Lane's category theory. The proposed problem solving method relies on a real time abstraction reasoning process to resume, on line, a lot of semantically poor data into an equivalent but richer one. The price to pay for such an information semantic enrichment is the loss of syntactic data (i.e. the oversight phenomenon). Our contributions are (i) to prove that Le Goc's timed observations theory (TOT) concept of unary observer plays the same role as Dirac's sampler, (ii) the construction of the $TOT(\mathbb{Z})$ category that is adequate to formulate the proposed abstraction based PSM and (iii) the design of TOM4A (timed observations methodology for abstraction), a specific recursive abstraction-reification based PSM whose a concrete application has been provided for detecting and modeling the complex problem of internal frauds in the banking industry

La visualisation interactive est un outil essentiel pour l'exploration, la compréhension et l'analyse de données. L'exploration interactive efficace de jeux de données grands ou complexes présente cependant deux difficultés fondamentales. La première est visuelle et concerne les limitations de la perception et cognition humaine, ainsi que celles des écrans. La seconde est computationnelle et concerne les limitations de capacité mémoire ou de traitement des machines standards. Dans cette thèse, nous nous intéressons aux techniques de passage à l'échelle relativement à ces deux difficultés, pour plusieurs contextes d'application.Pour le passage à l'échelle visuelle, nous présentons une approche versatile de mise en évidence de sous-ensembles d'éléments par déformation spatiale appliquée aux vues multiples et une représentation abstraite et multi-/échelle de coordonnées parallèles. Sur les vues multiples, la déformation spatiale vise à remédier à la diminution de l'efficacité de la surbrillance lorsque les éléments graphiques sont de taille réduite. Sur les coordonnées parallèles, l'abstraction multi-échelle consiste à simplifier la représentation tout en permettant d'accéder interactivement au détail des données, en les pré-agrégeant à plusieurs niveaux de détail.Pour le passage à l'échelle computationnelle, nous étudions des approches de pré-calcul et de calcul à la volée sur des infrastructures distribuées permettant l'exploration de jeux de données de plus d'un milliard d'éléments en temps interactif. Nous présentons un système pour l'exploration de données multi-dimensionnelles dont les interactions et l'abstraction respectent un budget en nombre d'éléments graphiques qui, en retour, fournit une borne théorique sur les latences d'interactions dues au transfert réseau entre client et serveur. Avec le même objectif, nous comparons des stratégies de réduction de données géométrique pour la reconstruction de cartes de densité d'ensembles de points. / Interactive visualization is helpful for exploring, understanding, and analyzing data. However, increasingly large and complex data challenges the efficiency of visualization systems, both visually and computationally. The visual challenge stems from human perceptual and cognitive limitations as well as screen space limitations while the computational challenge stems from the processing and memory limitations of standard computers.In this thesis, we present techniques addressing the two scalability issues for several interactive visualization applications.To address visual scalability requirements, we present a versatile spatial-distortion approach for linked emphasis on multiple views and an abstract and multi-scale representation based on parallel coordinates. Spatial distortion aims at alleviating the weakened emphasis effect of highlighting when applied to small-sized visual elements. Multiscale abstraction simplifies the representation while providing detail on demand by pre-aggregating data at several levels of detail.To address computational scalability requirements and scale data processing to billions of items in interactive times, we use pre-computation and real-time computation on a remote distributed infrastructure. We present a system for multi-/dimensional data exploration in which the interactions and abstract representation comply with a visual item budget and in return provides a guarantee on network-related interaction latencies. With the same goal, we compared several geometric reduction strategies for the reconstruction of density maps of large-scale point sets.

Cette thèse porte sur le développement d'approches compositionnelles et efficaces de synthèse de contrôleurs pour les systèmes cyber-physiques (CPS). En effet, alors que les techniques de conception des CPS basées sur des modèles ont fait l'objet de nombreuses études au cours de la dernière décennie, leur scalabilité reste problématique. Dans cette thèse, nous contribuons à rendre de telles approches plus évolutives.La première partie est axée sur les approches compositionnelles. Un cadre général pour le raisonnement compositionnel en utilisant des contrats d’hypothèse-garantie est proposé. Ce cadre est ensuite combiné avec des techniques de contrôle symbolique et appliqué à un problème de synthèse de contrôleur pour des systèmes échantillonnés, distribués et multipériodiques, où l'approche symbolique est utilisé pour synthétiser un contrôleur imposant un contrat donné. Ensuite, une nouvelle approche de calcul compositionnel des abstractions symboliques est proposée, basée sur la notion de composition approchée et permettant de traiter des abstractions hétérogènes.La deuxième partie de la thèse porte sur des techniques efficaces d'abstraction et de synthèse de contrôleurs. Deux nouvelles techniques de calcul d’abstractions sont proposées pour les systèmes à commutation incrémentalement stables. La première approche est basée sur l'échantillonnage multi-niveaux où nous avons établi l'existence d'un paramètre optimal d'échantillonnage qui aboutit à un modèle symbolique avec un nombre minimal de transitions. La deuxième approche est basée sur un échantillonnage événementiel, où la durée des transitions dans le modèle symbolique est déterminée par un mécanisme déclencheur, ce qui permet de réduire le conservatisme par rapport au cas périodique. La combinaison avec des techniques de synthèse de contrôleurs paresseux est proposée permettant la synthèse à un coût de calcul réduit. Enfin, une nouvelle approche de synthèse paresseuse a été développée pour les systèmes de transition monotones et les spécifications de sécurité dirigées. Plusieurs études de cas sont considérées dans cette thèse, telles que la régulation de la température dans les bâtiments, le contrôle des convertisseurs de puissance, le pilotage des véhicules et le contrôle de la tension dans les micro-réseaux DC. / This thesis focus on the development of compositional and efficient controller synthesis approaches for cyber-physical systems (CPS). Indeed, while model-based techniques for CPS design have been the subject of a large amount of research in the last decade, scalability of these techniques remains an issue. In his thesis, we contribute to make such approaches more scalable.The focus of the first part is on compositional approaches. A general framework for compositional reasoning using assume-guarantee contracts is proposed. This framework is then combined with symbolic control techniques and applied to a controller synthesis problem for multiperiodic distributed sampled-data systems, where symbolic approaches have been used to synthesize controllers enforcing a given assume-guarantee contract. Then, a new approach to the compositional computation of symbolic abstractions is proposed based on the notion of approximate composition, allowing to deal with heterogeneous abstractions and arbitrary interconnections.The second part is about efficient abstraction and controller synthesis techniques. Two new abstractions schemes have been developed for incrementally stable switched systems. The first approach is based on multirate sampling where we established the existence of an optimal multirate sampling parameter that results in a symbolic model with a minimal number of transitions. The second approach is based on event-based sampling, where the duration of transitions in the symbolic model is determined by some triggering mechanism, which makes it possible to reduce the conservatism with respect to the periodic case. Combination with lazy controller synthesis techniques has been proposed allowing the synthesis at a reduced computational cost. Finally, a new lazy approach has been develop for monotone transition systems and directed safety specifications. Several case studies have been considered in this thesis such as temperature regulation in buildings, control of power converters, vehicle platooning and voltage control in DC micro-grids.

The focus of current formal verification methods is mitigating the state explosion problem. One of these formal methods is predicate abstraction, which reduces concrete states of a system to bitvectors of true/false valuations of a set of predicates. Predicate abstraction comes in two flavors, over-approximation and under-approximation. A drawback of over-approximation is that it produces too many spurious errors for data-intensive applications. A more recent under-approximation technique which does not produce spurious errors, does abstract matching on concrete states (AMCS). AMCS adds behaviors to an abstract system by augmenting the set of initial predicates, making use of a theorem prover. The logic behind this approach is that if an error is found in the early coarse abstractions of the system, we save space and time. Our research improves AMCS by providing a refinement technique which guarantees termination. Our technique finds errors in less time and space by using an abstract state splitting algorithm based on intervals, which does not require a theorem prover.

Constraint programming (CP) is a technology in which a combinatorial problem is modeled declaratively as a conjunction of constraints, each of which captures some of the combinatorial substructure of the problem. Constraints are more than a modeling convenience: every constraint is partially implemented by an inference algorithm, called a propagator, that rules out some but not necessarily all infeasible candidate values of one or more unknowns in the scope of the constraint. Interleaving propagation with systematic search leads to a powerful and complete solution method, combining a high degree of re-usability with natural, high-level modeling. A propagator can be characterized as a sound approximation of a constraint on an abstraction of sets of candidate values; propagators that share an abstraction are similar in the strength of the inference they perform when identifying infeasible candidate values. In this thesis, we consider abstractions of sets of candidate values that may be described by an elegant mathematical formalism, the Galois connection. We develop a theoretical framework from the correspondence between Galois connections and propagators, unifying two disparate views of the abstraction-propagation connection, namely the oft-overlooked distinction between representational and computational over-approximations. Our framework yields compact definitions of propagator strength, even in complicated cases (i.e., involving several types, or unknowns with internal structure); it also yields a method for the principled derivation of propagators from constraint definitions. We apply this framework to the extension of an existing CP solver to constraints over strings, that is, words of finite length. We define, via a Galois connection, an over-approximation for bounded-length strings, and demonstrate two different methods for implementing this overapproximation in a CP solver. First we use the Galois connection to derive a bounded-length string representation as an aggregation of existing scalar types; propagators for this representation are obtained by manual derivation, or automated synthesis, or a combination. Then we implement a string variable type, motivating design choices with knowledge gained from the construction of the over-approximation. The resulting CP solver extension not only substantially eases modeling for combinatorial string problems, but also leads to substantial efficiency improvements over prior CP methods.

The present thesis is an exploration of normalization processes and the problem of appropriation in labor conflict. More specifically, it analyses the way contemporary labor conflicts in nursing relate to, and thereby help to illuminate, changes in modes of gender normalization under neoliberalism, and how nurse labor conflict thereby sheds light on wider patterns of labor strife. Analysis shows how a “virtue script” bound up with long-lasting patterns of gender normalization in nursing becomes tangled with forms of abstract labor related to “new public management” reform. Although the restructuring of work threatens public professionals’ autonomy, at the same time, it provides opportunities for resistance through collective action. What is more, this restructuring process facilitates the appropriation by nurses and, by implication, other public workers, of the discourses and ideals that belonged to the ethos of the Keynesian welfare state. However, this is a contradictory process, since the discourses and ideals thus appropriated inhere in modes of labor exploitation and normalization. Analysis indicates that although appropriation risks to reinforce gendered and exploitative ideas about work, the strategy can be a lever of collective mobilization, and one of its possible outcomes is the radical transformation of the entities it takes possession of. This interview study is mainly based on four journal articles, attending to different aspects of an act of collective resignation taken by registered nurses at a Swedish hospital ward. This is an emerging form of collective action and the thesis provides one of the first analyses of this new grassroots and workplace-based phenomenon, which may be considered its particular empirical contribution. On the other hand, the chapters of the cover essay unfold a sustained argument on normalization and appropriation, thereby elaborating theoretical themes broached in the articles. The focal point of this discussion is a certain concept of form, deployed in Marxist and feminist theory, a concept pointing to the identity of thought-forms and practically enacted forms. Further, these forms migrate: they are evoked in practices wherein “the mind is not active as sentient” (Hegel), later to be projected by the mind onto different entities. The results of the discussion thus question common approaches to normalization. In particular, it is untenable to oppose a tacit and internal mode of control where individuals are induced to comply by attaching to identifications (by becoming/being made into subjects) to an overt and external mode reliant on sheer coercion. This matter–form dichotomy should be dissolved, and modes of coercion should be understood to leave subjective imprints—not at the level of identity but at the level of thought’s infrastructure, that is, form. / Föreliggande avhandling utforskar normaliseringsprocesser och problem rörande appropriering i samband med arbetskonflikter. Avhandlingen analyserar hur sam-tida arbetskonflikter i sjuksköterskeprofessionen relaterar till och sålunda belyser förändrad genusnormalisering i en nyliberal tid, samt hur dessa konflikter belyser övergripande konfliktmönster i arbetslivet. Analysen påvisar hur en ”dygdighets-norm” kopplad till långlivade modaliteter av genusnormalisering sammanvävs med en form av abstrakt arbete relaterad till sentida NPM-reformer. Men medan denna omstruktureringsprocess urholkar den autonomi som professioner i offentlig sektor länge innehaft medför den också möjligheter till kollektiva motståndshandlingar. Vidare möjliggör denna nyliberala omstrukturering sjuksköterskors—liksom andra offentliga professioners—appropriering av diskurser och ideal som var centrala i den tidigare, keynesianska, välfärdsstaten; men detta är en motsägelsefull process då dessa diskurser och ideal är sprungna ur, och präglade av, historier av utsugning och normalisering. Analysen visar att medan appropriering visserligen riskerar att reproducera former av normalisering underlättar denna strategi mobilisering och kan i förlängningen omvandla övertagna diskurser och ideal. Denna intervjustudie är huvudsakligen baserad på fyra artiklar: de analyserar olika aspekter av en kollektiv uppsägningsaktion bland sjuksköterskor vid en sjukhus-avdelning. Detta är en framväxande typ av aktion i Sverige och avhandlingen är en av de första studierna av denna gräsrots- och arbetsplatsbaserade kampform, vilket kan ses som dess empiriska forskningsbidrag. I kappan förs, å andra sidan, en kon-tinuerlig teoretisk diskussion kring normalisering och appropriering som utvecklar teman som lyfts i de enskilda artiklarna. Diskussionen kretsar kring ett visst form-begrepp, som härrör ur marxistisk och feministisk teori och som påvisar en identitet mellan tankeform och praktiskt artikulerad form. Dessa former migrerar; de uttrycks omedvetet i praktiker där individens fokus är annorstädes och projiceras sedan på andra praktiker. I diskussionen ifrågasätts sålunda vedertagna förståelser av norma-lisering: det är teoretiskt ofruktbart att ställa omedvetna, interna, former av kontroll där lydnad eller konformitet uppnås via internaliseringen av påbjudna identiteter mot medvetna, externa, eller tvingande, former av kontroll. En häri latent dikotomi om materia respektive form bör upplösas i syfte att synliggöra hur ett slags kontroll över arbete lämnar subjektiverande avtryck, inte genom att påbjuda identifikationer utan genom att forma vad som kan beskrivas som tänkandets minsta beståndsdelar. / <p>Vid tidpunkten för disputationen var följande delarbeten opublicerade: delarbete 2 och 4 inskickat.</p><p>At the time of the doctoral defence the following papers were unpublished: paper 2 and 4 submitted.</p>

ITC/USA 2007 Conference Proceedings / The Forty-Third Annual International Telemetering Conference and Technical Exhibition / October 22-25, 2007 / Riviera Hotel & Convention Center, Las Vegas, Nevada / The Instrumentation Hardware Abstraction Language (IHAL) has been developed to be a neutral language that is focused on the description and control of instrumentation systems and networks. This paper describes the various instrumentation configuration management tools we have designed that make use of IHAL’s neutral specification of instrumentation networks. We discuss the features currently present in prototypes as well as future enhancements.

International Telemetering Conference Proceedings / October 23-26, 2000 / Town & Country Hotel and Conference Center, San Diego, California / With wireless communications becoming the rule rather than the exception, satellite operators need tools to effectively monitor increasingly large and complex satellite constellations. Visual data monitoring increases the monitoring capacity of satellite operators by several orders of magnitude, enabling them to track hundreds of thousands of parameters in real-time on a single screen. With this powerful new tool, operators can proactively address potential problems before they become customer complaints.

The thesis explores human embodiment in 3D Virtual environments as a means of enhancing interaction. I aim to provide a better understanding of embodied interaction in digital environments in general. 3D interactive virtual environments challenge users to question aspects of their embodiment by providing new modes for interacting with space. Designers are facing new challenges that require novel means of interacting with virtual environments that do not simply mirror the way we interact within physical environments. Much of the research in the field aims to show how such environments can be made more familiar and "realistic" to users. This thesis attempts to probe the unfamiliar aspects of the medium. In this thesis I explore the concept, image and object of intimate space. How can an understanding of intimate space inform embodied interaction with virtual environments? I also investigate the role of familiarity by analysing and testing it in two contrasting interactive virtual environments. My contribution is to provide an account of familiarity as the driver behind embodied interaction in virtual environments based on human experience (from a phenomenological standpoint). In order to enhance the process of design for human embodied interaction in 3D virtual environments or in physical environments, I will identify tangible and intangible elements that affect human embodiment in 3D virtual environments and space, such as ethics and scale. Both examples are explored in interactive 3D virtual environments corresponding to real physical environments by subjects who are the daily users of the real physical environments. The thesis presents scale as a tangible element and ethics as an intangible element of human embodied interaction in space in order to highlight the different aspects that affect human engagement with space, and therefore human perception of their space and their embodiment. The Subjects’ accounts contribute toward informing the design of interactive 3D virtual environments within the context of embodied interaction.

I present a simple Simultaneous Abstraction Calculus, where the familiar lambda-abstraction over single variables is replaced by abstraction over whole sets of them. Terms are applied to partial assignments of objects to variables. Variants of the system are investigated and compared, with respect to their semantic and proof theoretic properties. The system overcomes the strict ordering requirements of the standard lambda-calculus,and is shown to provide the kind of "non-selective" binding needed for Dynamic Montague Grammar and Discourse Representation Theory. It is closely related to a more complex system, due to Peter Aczel and Rachel Lunon, and can be used for Situation Theory in a similar way. I present versions of these theories within an axiomatic, property-theoretic framework, based on Aczels Frege Structures. The aim of this work is to provide the means for integrating various semantic theories within a formal framework,so that they can share what is common between them, and adopt from each other what is compatible with them.