Le respect de la vie privée par construction est de plus en plus mentionné comme une étape essentielle vers une meilleure protection de la vie privée. Les nouvelles technologies de l'information et de la communication donnent naissance à de nouveaux modèles d'affaires et de services. Ces services reposent souvent sur l'exploitation de données personnelles à des fins de personnalisation. Alors que les exigences de respect de la vie privée sont de plus en plus sous tension, il apparaît que les technologies elles-mêmes devraient être utilisées pour proposer des solutions davantage satisfaisantes. Les technologies améliorant le respect de la vie privée ont fait l'objet de recherches approfondies et diverses techniques ont été développées telles que des anonymiseurs ou des mécanismes de chiffrement évolués. Cependant, le respect de la vie privée par construction va plus loin que les technologies améliorant simplement son respect. En effet, les exigences en terme de protection des données à caractère personnel doivent être prises en compte au plus tôt lors du développement d’un système car elles peuvent avoir un impact important sur l'ensemble de l'architecture de la solution. Cette approche peut donc être résumée comme « prévenir plutôt que guérir ». Des principes généraux ont été proposés pour définir des critères réglementaires de respect de la vie privée. Ils impliquent des notions telles que la minimisation des données, le contrôle par le sujet des données personnelles, la transparence des traitements ou encore la redevabilité. Ces principes ne sont cependant pas suffisamment précis pour être directement traduits en fonctionnalités techniques. De plus, aucune méthode n’a été proposée jusqu’ici pour aider à la conception et à la vérification de systèmes respectueux de la vie privée. Cette thèse propose une démarche de spécification, de conception et de vérification au niveau architectural. Cette démarche aide les concepteurs à explorer l'espace de conception d'un système de manière systématique. Elle est complétée par un cadre formel prenant en compte les exigences de confidentialité et d’intégrité des données. Enfin, un outil d’aide à la conception permet aux concepteurs non-experts de vérifier formellement les architectures. Une étude de cas illustre l’ensemble de la démarche et montre comment ces différentes contributions se complètent pour être utilisées en pratique. / Privacy by Design (PbD) is increasingly praised as a key approach to improving privacy protection. New information and communication technologies give rise to new business models and services. These services often rely on the exploitation of personal data for the purpose of customization. While privacy is more and more at risk, the growing view is that technologies themselves should be used to propose more privacy-friendly solutions. Privacy Enhancing Technologies (PETs) have been extensively studied, and many techniques have been proposed such as anonymizers or encryption mechanisms. However, PbD goes beyond the use of PETs. Indeed, the privacy requirements of a system should be taken into account from the early stages of the design because they can have a large impact on the overall architecture of the solution. The PbD approach can be summed up as ``prevent rather than cure''. A number of principles related to the protection of personal data and privacy have been enshrined in law and soft regulations. They involve notions such as data minimization, control of personal data by the subject, transparency of the data processing, or accountability. However, it is not clear how to translate these principles into technical features, and no method exists so far to support the design and verification of privacy compliant systems. This thesis proposes a systematic process to specify, design, and verify system architectures. This process helps designers to explore the design space in a systematic way. It is complemented by a formal framework in which confidentiality and integrity requirements can be expressed. Finally, a computer-aided engineering tool enables non-expert designers to perform formal verifications of the architectures. A case study illustrates the whole approach showing how these contributions complement each other and can be used in practice.

La modélisation informatique et la simulation sont des activités de plus en plus répandues lors de la conception de systèmes complexes et critiques tels que ceux embarqués dans les avions. Une proposition pour la conception et réalisation d'abstractions compatibles avec les objectifs de simulation est présentée basés sur la théorie de l'informatique, le contrôle et le système des concepts d'ingénierie. Il adresse deux problèmes fondamentaux de fidélité dans la simulation, c'est-à-dire, pour une spécification du système et quelques propriétés d'intérêt, comment extraire des abstractions pour définir une architecture de produit de simulation et jusqu'où quel point le comportement du modèle de simulation représente la spécification du système. Une notion générale de cette fidélité de la simulation, tant architecturale et comportementale, est expliquée dans les notions du cadre expérimental et discuté dans le contexte des abstractions de modélisation et des relations d'inclusion. Une approche semi-formelle basée sur l'ontologie pour construire et définir l'architecture de produit de simulation est proposée et démontrée sur une étude d'échelle industrielle. Une approche formelle basée sur le jeu théorique et méthode formelle est proposée pour différentes classes de modèles des systèmes et des simulations avec un développement d'outils de prototype et cas des études. Les problèmes dans la recherche et implémentation de ce cadre de fidélité sont discutées particulièrement dans un contexte industriel. / In using Modeling and Simulation for the system Verification & Validation activities, often the difficulty is finding and implementing consistent abstractions to model the system being simulated with respect to the simulation requirements. A proposition for the unified design and implementation of modeling abstractions consistent with the simulation objectives based on the computer science, control and system engineering concepts is presented. It addresses two fundamental problems of fidelity in simulation, namely, for a given system specification and some properties of interest, how to extract modeling abstractions to define a simulation product architecture and how far does the behaviour of the simulation model represents the system specification. A general notion of this simulation fidelity, both architectural and behavioural, in system verification and validation is explained in the established notions of the experimental frame and discussed in the context of modeling abstractions and inclusion relations. A semi-formal ontology based domain model approach to build and define the simulation product architecture is proposed with a real industrial scale study. A formal approach based on game theoretic quantitative system refinement notions is proposed for different class of system and simulation models with a prototype tool development and case studies. Challenges in research and implementation of this formal and semi-formal fidelity framework especially in an industrial context are discussed.

Nous proposons de nouveaux algorithmes et de nouvelles structures de données pour la vérification formelle de systèmes réactifs finis sur architectures parallèles. Ces travaux se basent sur les techniques de vérification model checking. Notre approche cible des architectures multi-processeurs et multi-cœurs, avec mémoire partagée, qui correspondent aux générations de serveurs les plus performants disponibles actuellement.Dans ce contexte, notre objectif principal est de proposer des approches qui soient à la fois efficaces au niveau des performances, mais aussi compatibles avec les politiques de partage dynamique du travail utilisées par les algorithmes de génération d’espaces d'états en parallèle; ainsi, nous ne plaçons pas de contraintes sur la manière dont le travail ou les données sont partagés entre les processeurs.Parallèlement à la définition de nouveaux algorithmes de model checking pour machines multi-cœurs, nous nous intéressons également aux algorithmes de vérification probabiliste. Par probabiliste, nous entendons des algorithmes de model checking qui ont une forte probabilité de visiter tous les états durant la vérification d’un système. La vérification probabiliste permet des gains importants au niveau de la mémoire utilisée, en échange d’une faible probabilité de ne pas être exhaustif; il s’agit donc d’une stratégie permettant de répondre au problème de l’explosion combinatoire / In this thesis, we propose and study new algorithms and data structures for model checking finite-state, concurrent systems. We focus on techniques that target shared memory, multi-cores architectures, that are a current trend in computer architectures.In this context, we present new algorithms and data structures for exhaustive parallel model checking that are as efficient as possible, but also ``friendly'' with respect to the work-sharing policies that are used for the state space generation (e.g. a work-stealing strategy): at no point do we impose a restriction on the way work is shared among the processors. This includes both the construction of the state space as the detection of cycles in parallel, which is is one of the key points of performance for the evaluation of more complex formulas.Alongside the definition of enumerative, model checking algorithms for many-cores architectures, we also study probabilistic verification algorithms. By the term probabilistic, we mean that, during the exploration of a system, any given reachable state has a high probability of being checked by the algorithm. Probabilistic verification trades savings at the level of memory usage for the probability of missing some states. Consequently, it becomes possible to analyze part of the state space of a system when there is not enough memory available to represent the entire state space in an exact manner