La plupart des entreprises évoluent dans des marchés concurrentiels en adaptant rapidement leurs processus métiers. Leur performance dépend de leur capacité à utiliser des techniques d'amélioration continue de leur organisation par la mise au point de Systèmes Informatiques (SI) durables pour l'automatisation des processus. En ce sens, les architectures orientées services (Service Oriented Architectures) ont permis le développement de SI flexibles avec un style d'architecture prédominant de composition de services. Cependant, l'alignement de ces architectures aux impératifs de l'évolution des processus reste une préoccupation centrale. Dans cette thèse, nous étudions la cartographie et l'évolution des processus métiers depuis leur conception jusqu'à leur automatisation dans une architecture orientée services ainsi que son adaptation. Nous proposons une approche d'ingénierie dirigée par les modèles intégrée à un outil de modélisation de processus et de développement d'architectures orientées services. Celle-ci débute par la spécification d'un modèle BPMN (Business Process Modeling Notation) décrivant les interactions des processus métiers. Grâce à une chaîne de transformation automatisée, nous produisons un modèle SCA (Service Component Architecture) décrivant une solution de composition de services. Ceci garantit la traçabilité architecturale entre le niveau métier du SI et son niveau technique puisque les services générés décrivent une logique applicative qui met en oeuvre la logique métier du modèle BPMN. Ensuite, nous introduisons une méthode de propagation du changement de la logique métier vers la logique applicative qui est fondée sur la synchronisation incrémentale entre les modèles BPMN et SCA. Elle est intégrée à un outil d'analyse de l'impact du changement qui se base sur la réécriture de graphes pour éviter les inconsistances induites par les modifications. Enfin, elle permet de simuler l'impact des évolutions des processus, pour en estimer le coût selon les métriques que nous proposons, avant de procéder à la réingénierie de l'architecture orientée services pour assurer une meilleure gouvernance du changement / Most companies evolve in competitive markets by quickly adapting their business processes. Their performance depends on their capability to adopt continuous improvement techniques for their organization through the development of durable Information Systems (IS) for automating the processes. In this sense, Service-Oriented Architectures (SOA) enable the development of flexible IS with a predominant architectural paradigm of service compositions. However, aligning the SOA to the business processes evolutions remains an overriding concern. In this thesis, we study business process management and evolution from their design until their automation in SOA and their adaptation. We propose a model-driven engineering approach which is integrated to a tool for business process modeling and SOA development. It begins with the design of a model with Business Process Modeling Notation (BPMN) describing process interactions. With an automated transformation chain, we produce a model with Service-Component Architecture (SCA) describing service compositions solution based on a SOA. This ensures the architectural traceability between the business level of the IS and its technical level, since generated services describe an application logic that implements the BPMN model. Then, we introduce an incremental change propagation method between business process and SOA founded on BPMN and SCA models synchronization. It is integrated to a change impact simulation and analysis tool that is based on graph rewriting technique to avoid the inconsistencies caused by change propagation. Finally, we propose metrics for measuring the impact of business process evolutions on SOA maintenance and ensuring better change governance

Les preuves par récurrence sont parfaitement adaptées au raisonnement sur des structures de données non-bornées, comme par exemple les entiers et les listes, ou, de manière plus générale, sur des ensembles d’éléments non vides munis d’ordres noethériens. Leur domaine d’application est très vaste, une utilité particulière portant sur la validation des propriétés d’applications industrielles dans des domaines critiques tels que les télécommunications et les cartes à puces. Le principe de récurrence noethérienne est à la base d’un ensemble de techniques de preuve par récurrence modernes, dont celles basées sur la récurrence implicite. Dans cette thèse, nous nous intéresserons à l’intégration du raisonnement par récurrence implicite tel qu’il est implémenté dans le démonstrateur Spike en utilisant l’environnement de preuve certifié Coq. Basé sur la récurrence implicite, Spike est capable de raisonner automatiquement sur des théories conditionnelles de premier ordre. L’implémentation de Spike n’est pas encore certifiée, même si les fondements théoriques sous-jacents ont été approuvés à plusieurs reprises par la communauté scientifique. Une alternative convenable serait de certifier seulement les preuves générées par Spike. Dans ce cas, le processus de certification doit être automatique car les scripts de preuves de Spike sont souvent longs. Des travaux précédents ont montré la possibilité de certifier automatiquement des preuves par récurrence implicite générées par Spike à l’aide de l’environnement certifié de l’assistant de preuve Coq. Nous proposerons des nouvelles tactiques Coq qui seront capables de prouver automatiquement des théorèmes par récurrence implicite. Deux approches seront étudiées. La première approche consiste à utiliser Spike comme un outil externe. Elle est limitée au traitement des spécifications Coq qui peuvent être traduites dans des spécifications conditionnelles, ainsi qu’à des théorèmes convertibles dans des équations conditionnelles. Les traces de preuves générées par Spike sont ensuite traduites dans des scripts Coq qui sont finalement validés par son noyau. Une autre limitation est due à la traduction des applications d’un sous-ensemble de règles d’inférence de Spike. La deuxième approche est l’utilisation des stratégies à la Spike pour construire automatiquement des preuves par récurrence implicite dans Coq. Cette approche se base sur des tactiques Coq qui simulent des règles d’inférence de Spike pour générer de nouveaux sous-buts. Par rapport à la première approche, ces tactiques peuvent utiliser des techniques de raisonnement de Coq qui ne sont pas présentes dans Spike et ouvre la possibilité de mélanger des étapes de preuves automatiques et manuelles. Ces deux approches ont été mises en œuvre et testées sur différents exemples dont des lemmes utilisés dans la preuve de validité de l’algorithme de conformité du protocole de télécommunication ABR / Proofs by induction are perfectly adequate to reasoning on unbounded data structures, for example naturals, lists and more generally on non-empty sets of elements provided with noetherian orders. They are largely used on different fields, particularly for the validation of properties of industrial applications in critical areas such as telecommunications and smart cards. The principle of noetherian induction is the basis of a set of modern techniques of proof by induction, including those based on implicit induction. In this thesis, we will focus on the integration of implicit induction reasoning like it is implemented by spike using the certified proof environnement Coq. Spike is an automatic theorem prover based on implicit induction that is capable of reasoning on conditional first-order theories. The implementation of Spike is not yet certified, even if the underlying theoretical foundations have been approved repeatedly by the scientific community. A suitable alternative is to certify only the proofs produced by Spike. In this case, the certification process must be automatic because scripts of Spike’s proofs are often long. Previous work has shown the possibility of certifying automatically some proofs by implicit induction generated by Spike using the certified environment provided by the Coq proof-assistant. We will propose new Coq tactics that are able to prove automatically theorems by implicit induction. Two approaches will be studied. The first approach consists on using Spike as an external tool. It is limited to process Coq specifications which can be translated in conditional specifications, as well as theorems convertible in conditional equations. Proofs generated by Spike are then translated into Coq scripts finally validated by its kernel. Another limitation is due to the translation of the application of a subset of the Spike inference rules. The second approche is to use strategies à la Spike to automatically build implicit induction proofs in Coq. This approach consists on creating tactics that perform like Spike inference rules to generate new subgoals in Coq. Comparing to the first approach, these tactics permit the use of Coq reasoning techniques which are not present in Spike and opens the possibility of mixing automatic and manual proof steps. Both approaches have been implemented and tested on several examples including lemmas used in the proof of validity of the conformity algorithm for the ABR telecommunications protocol

Computer forensic tools have been developed to enable forensic investigators to analyse software artefacts to help reconstruct possible scenarios for activity on a particular computer system. A number of these tools allow the examination and analysis of system generated artefacts such as the Windows registry. Examination and analysis of these artefacts is focussed on recovering the data extracting information relevant to a digital investigation. This information is currently underused in most digital investigations. With this in mind, this thesis considers system generated artefacts that contain information concerning the activities that occur on a Windows system and will often contain evidence relevant to a digital investigation. The objective of this research is to develop an architecture that simplifies and automates the collection of forensic evidence from system generated files where the data structures may be either known or in a structured but poorly understood (unknown) format. The hypothesis is that it should be feasible to develop an architecture that will be to integrate forensic data extracted from a range of system generated files and to implement a proof of concept prototype tool, capable of visualising the Event logs and Swap files. This thesis presents an architecture to enable the forensic investigator to analyse and visualise a range of system generated artefacts for which the internal arrangement of data is either well structured and understood or those for which the internal arrangement of the data is unclear or less publicised (known and not known data structures). The architecture reveals methods to access, view and analyse system generated artefacts. The architecture is intended to facilitate the extraction and analysis of operating system generated artefacts while being extensible, flexible and reusable. The architectural concepts are tested using a prototype implementation focussed the Windows Event Logs and the Swap Files. Event logs reveal evidence regarding logons, authentication, account and privilege use and can address questions relating to which user accounts were being used and which machines were accessed. Swap file contains fragments of data, remnants or entire documents, e-mail messages or results of internet browsing which reveal past user activities. Issues relating to understanding and visualising artefacts data structure are discussed and possible solutions are explored. The architecture is developed by examining the requirements and methods with respect to the needs of computer forensic investigations and forensic process models with the intention to develop a new multiplatform tool to visualise the content of Event logs and Swap files. This tool is aimed at displaying data contained in event logs and swap files in a graphical manner. This should enable the detection of information which may support the investigation. Visualisation techniques can also aid the forensic investigators in identifying suspicious events and files, making such techniques more feasible for consideration in a wider range of cases and, in turn, improve standard procedures. The tool is developed to fill a gap between capabilities of certain other open source tools which visualise the Event logs and Swap files data in a text based format only.

Les systèmes informatiques envahissent notre vie quotidienne et sont devenus des éléments essentiels de chacun de nos instants de vie. La technologie de l'information est un secteur d'activités offrant des opportunités considérables pour l'innovation et cet aspect paraît sans limite. Cependant, des systèmes à logiciel intégré ont donné des résultats décevants. Selon les constats, ils étaient non fiables, parfois dangereux et ne fournissaient pas les résultats attendus. La faiblesse des pratiques de développement constitue la principale raison des échecs de ces systèmes. Ceci est dû à la complexité des logiciels modernes et au manque de connaissances adéquates et propres. Le développement logiciel fournit un cadre contribuant à simplifier la conception de systèmes complexes, afin d'en obtenir une meilleure compréhension et d'assurer une très grande qualité à un coût moindre. Dans les domaines de l'automatique, de la surveillance médicale, de l'avionique..., les systèmes embarqués hautement critiques sont candidats aux erreurs pouvant conduire à des conséquences graves en cas d'échecs. La thèse vise à résoudre ce problème, en fournissant un ensemble de techniques, d'outils et un cadre pour développer des systèmes hautement critiques, en utilisant des techniques formelles à partir de l'analyse des exigences jusqu'à la production automatique de code source, en considérant plusieurs niveaux intermédiaires. Elle est structurée en deux parties: d'une part des techniques et des outils et d'autre part des études de cas. La partie concernant des techniques et des outils présente une structure intégrant un animateur de modèles en temps-réel, un cadre de correction de modèles et le concept de charte de raffinement, un cadre de modélisation en vue de la certification, un modèle du coeur pour la modélisation en boucle fermée et des outils de générations automatiques de code. Ces cadres et outils sont utilisés pour développer les systèmes critiques à partir de l'analyse des exigences jusqu'à la production du code, en vérifiant et en validant les étapes intermédiaires en vue de fournir un modèle formel correct satisfaisant les propriétés souhaitées attendues au niveau le plus concret. L'introduction de nouveaux outils concourt à améliorer la vérification des propriétés souhaitées qui ne sont pas apparentes aux étapes initiales du développement du système. Nous évaluons les propositions faites au travers de cas d'études du domaine médical et du domaine des transports. De plus, le travail de cette thèse a étudié la représentation formelle des protocoles médicaux, afin d'améliorer les protocoles existants. Nous avons complètement formalisé un protocole réel d'interprétation des ECG, en vue d'analyser si la formalisation était conforme à certaines propriétés relevant du protocole. Le processus de vérification formelle a mis en évidence des anomalies dans les protocoles existants. Nous avons aussi découvert une structure hiérarchique pour une interprétation efficace permettant de découvrir un ensemble de conditions qui peuvent être utiles pour diagnostiquer des maladies particulières à un stade précoce. L'objectif principal du formalisme développé est de tester la correction et la consistance du protocole médical / Software systems are pervasive in all walks of our life and have become an essential part of our daily life. Information technology is one major area, which provides powerful and adaptable opportunities for innovation, and it seems boundless. However, systems developed using computer-based logic have produced disappointing results. According to stakeholders, they are unreliable, at times dangerous, and fail to provide the desired outcomes. Most significant reasons of system failures are the poor development practices for system development. This is due to the complex nature of modern software and lack of adequate and proper understanding. Software development provides a framework for simplifying the complex system to get a better understanding and to develop the higher fidelity quality systems at lower cost. Highly embedded critical systems, in areas such as automation, medical surveillance, avionics, etc., are susceptible to errors, which can lead to grave consequences in case of failures. This thesis intends to contribute to further the use of formal techniques for the development computing systems with high integrity. Specifically, it addresses that formal methods are not well integrated into established critical systems development processes by defining a new development life-cycle, and a set of associated techniques and tools to develop highly critical systems using formal techniques from requirements analysis to automatic source code generation using several intermediate layers with rigorous safety assessment approach. The approach has been realised using the Event-B formalism. This thesis has mainly two parts: techniques and tools and case studies. The techniques and tools section consists of development life-cycle methodology, a framework for real-time animator, refinement chart, a set of automatic code generation tools and formal logic based heart model for close loop modeling. New development methodology, and a set of associated techniques and tools are used for developing the critical systems from requirements analysis to code implementation, where verification and validation tasks are used as intermediate layers for providing a correct formal model with desired system behavior at the concrete level. Introducing new tools help to verify desired properties, which are hidden at the early stage of the system development. We also critically evaluate the proposed development methodology and developed techniques and tools through case studies in the medical and automotive domains. In addition, the thesis work tries to address the formal representation of medical protocols, which is useful for improving the existing medical protocols. We have fully formalised a real-world medical protocol (ECG interpretation) to analyse whether the formalisation complies with certain medically relevant protocol properties. The formal verification process has discovered a number of anomalies in the existing protocols. We have also discovered a hierarchical structure for the ECG interpretation efficiently that helps to find a set of conditions that can be very helpful to diagnose particular disease at the early stage. The main objective of the developed formalism is to test correctness and consistency of the medical protocol

Knowing ‘what’ to build is an integral part of an Information System Development, and it is generally understood that this, which is known as Requirements, is achievable through a process of understanding, communication and management. It is currently maintained by the Requirements theorists that successful system design clarifies the interrelations between information and its representations. However, this belief can be shown to be based on flawed assumptions, as there are persistent reports of failures, indicating that there is a gap between the theory and the practice, and that this gap needs to be bridged. A year long in-depth case study of a project group, starting with their strategy announcement and ending with the commissioning system hand-over meeting, followed the group in their ‘doing’ of the Requirements. These mundane meetings were recorded and transcribed, forming a detailed data set of ‘what-is-done’ and ‘how-it-is-done’. The developed research approach adhesively maintained the practical situation, aiming to investigate and make sense of the here-and-now actions of the scoping and defining processes that were at work. The results of the investigation led the researcher to question previous beliefs and assumptions in Requirements, because of ambiguities that were uncovered, also because there was no sufficiently distinct process found that could assuredly be labelled as Requirements. This phenomenon evoked further questioning of “how strange?”, which triggered the testing of the validity of the Requirements theory. The second stage adapted an analysis framework on decision-making in order to reveal a causal connection between the actions found in the ‘doing’ and in the stocks of knowledge that form the Requirements theory. This phase analysed the operationalization of the theory to examine its commensurate, incommensurate and defective activities. The analysis revealed the existence of other dominant processes that affect the Requirements theory, leaving it underdetermined, with no true causal connections that can be established. This led to the inevitable conclusion that the current Information Systems thinking on Requirements is on the horns of a dilemma without any prospective resolution, because of the elliptical misalignment between the theoretical and the empirical worlds.

Στην παρούσα διπλωματική αναπτύσσεται ένα ενσωματωμένο σύστημα αποτελούμενο από υλικό και λογισμικό, για τον χαρακτηρισμό τηλεπικοινωνιακών διατάξεων. Ειδικότερα μελετάται ο έλεγχος εξειδικευμένης ενσωματωμένης τηλεπικοινωνιακής διάταξης, η αυτοματοποίηση της συλλογής δεδομένων ενδιαφέροντος κατά τη λειτουργία της τηλεπικοινωνιακής διάταξης, καθώς και ο τρόπος επικοινωνίας με το χρήστη αναπτυξιακών συστημάτων που βασίζονται σε FPGA και χρησιμοποιούνται για την κατασκευή προτύπων τηλεπικοινωνιακών διατάξεων. Συγκεκριμένα μελετώνται διαφορετικές τεχνικές εισαγωγής και εξαγωγής δεδομένων από τα FPGAs και αποθήκευσής τους σε σύστημα host. O τρόπος εισαγωγής δεδομένων και παραμέτρων στα υπάρχοντα συστήματα παρουσιάζει συγκεκριμένους περιορισμούς. Εδώ μελετάται ο τρόπος που μπορούν τα δεδομένα και παράμετροι να εισάγονται δυναμικά μέσω ενός φιλικού προς τον χρήστη περιβάλλοντος. Επίσης μελετάται ο τρόπος αυτόματης συλλογής όγκου δεδομένων ενδιαφέροντος και εξαγωγής δεδομένων με ασφαλή και αυτοματοποιημένο τρόπο. Για να επιτευχθεί αυτό αναπτύσσεται ένα ενσωματωμένο σύστημα που η διεπαφή χρήστη γίνεται μέσω web server. Η ανάπτυξη περιλαμβάνει τη χρήση ενσωματωμένου επεξεργαστή διαθέσιμου ως IP block σε FPGA, τη δόμηση ενός συστήματος βασισμένου σε κανάλια επικοινωνίας με χρήση εικονικής διευθυνσιοδότησης, καθώς και τον έλεγχο και σύνδεση της μονάδας προτυποποίησης τηλεπικοινωνιακών διατάξεων με το κανάλι επικοινωνίας του επεξεργαστή. Το σύστημα που προκύπτει είναι ένα ενσωματωμένο σύστημα στο οποίο το λειτουργικό σύστημα βασίζεται σε διακοπές ενώ η διεπαφή χρήστη γίνεται με την ανάπτυξη ενσωματωμένου web server. Με αυτόν τον τρόπο παρέχεται ένα διαδραστικό περιβάλλον που είναι ευρέως διαδεδομένο και με το οποίο ο χρήστης μπορεί να έχει άμεση επαφή με το hardware, ενώ ταυτόχρονα αυτοματοποιεί τη διαδικασία εξαγωγής δεδομένων προσφέροντας αξιοπιστία και υψηλές ταχύτητες. / This thesis presents the development of an embedded system composed of both hardware and software components, for the characterization of a telecommunication prototype. Specifically, we study the control of an advanced telecommunication IP, the automation of collecting interesting data during the operation of the telecommunication device, and ways in available for the engineer to interact with FPGA-based system prototypes. Different techniques of importing and exporting data from the FPGA and storing them to a host system are investigated. The way of importing data and parameters in existing systems presents certain restrictions. In this thesis we study techniques of dynamically importing the data and parameters through a user-friendly environment. We automated the process of collecting data of interest and data retrieval in a secure and reliable manner. To achieve this, an embedded system interface is implemented developing an embedded, on-board web server. The development process includes the use of an embedded processor available as IP block on an FPGA, building a system based on bus channels using virtual addressing, and the connection and the control of telecommunication IP blocks through the bus channel to the processor. The developed system is an embedded system utilizes an interrupt-based operating system offering a user interface based a developed embedded web server. This system provides an interactive environment which is widely used, where the developer can directly access the hardware, and at the same time automates data retrieval and offers reliability and high speed.

Les travaux de cette thèse s'inscrivent dans le cadre du projet Petasky. Notre objectif est de proposer des outils permettant de gérer des dizaines de Peta-octets de données issues d'observations astronomiques. Nos travaux se focalisent essentiellement sur la conception des nouveaux systèmes permettant de garantir le passage à l'échelle. Dans cette thèse, nos contributions concernent trois aspects : Benchmarking des systèmes existants, conception d'un nouveau système et optimisation du système. Nous avons commencé par analyser la capacité des systèmes fondés sur le modèle MapReduce et supportant SQL à gérer les données LSST et leurs capacités d'optimisation de certains types de requêtes. Nous avons pu constater qu'il n'y a pas de technique « magique » pour partitionner, stocker et indexer les données mais l'efficacité des techniques dédiées dépend essentiellement du type de requête et de la typologie des données considérées. Suite à notre travail de Benchmarking, nous avons retenu quelques techniques qui doivent être intégrées dans un système de gestion de données à large échelle. Nous avons conçu un nouveau système de façon à garantir la capacité dudit système à supporter plusieurs mécanismes de partitionnement et plusieurs opérateurs d'évaluation. Nous avons utilisé BSP (Bulk Synchronous Parallel) comme modèle de calcul. Les données sont représentées logiquement par des graphes. L'évaluation des requêtes est donc faite en explorant le graphe de données en utilisant les arcs entrants et les arcs sortants. Les premières expérimentations ont montré que notre approche permet une amélioration significative des performances par rapport aux systèmes Map/Reduce / This work is carried out in framework of the PetaSky project. The objective of this project is to provide a set of tools allowing to manage Peta-bytes of data from astronomical observations. Our work is concerned with the design of a scalable approach. We first started by analyzing the ability of MapReduce based systems and supporting SQL to manage the LSST data and ensure optimization capabilities for certain types of queries. We analyzed the impact of data partitioning, indexing and compression on query performance. From our experiments, it follows that there is no “magic” technique to partition, store and index data but the efficiency of dedicated techniques depends mainly on the type of queries and the typology of data that are considered. Based on our work on benchmarking, we identified some techniques to be integrated to large-scale data management systems. We designed a new system allowing to support multiple partitioning mechanisms and several evaluation operators. We used the BSP (Bulk Synchronous Parallel) model as a parallel computation paradigm. Unlike MapeReduce model, we send intermediate results to workers that can continue their processing. Data is logically represented as a graph. The evaluation of queries is performed by exploring the data graph using forward and backward edges. We also offer a semi-automatic partitioning approach, i.e., we provide the system administrator with a set of tools allowing her/him to choose the manner of partitioning data using the schema of the database and domain knowledge. The first experiments show that our approach provides a significant performance improvement with respect to Map/Reduce systems

Dans le cadre de l’informatique décisionnelle, la programmation physico-financière doit permettre à des acteurs d’une collectivité provenant de divers domaines de faire converger leurs problématiques vers un objectif commun. L’une des principales difficultés de la modélisation d’une programmation physico-financière est que chaque acteur exprime ses problématiques dans des échelles de temps différentes. Dans cette thèse CIFRE, un métamodèle de calcul en temps continu appliqué à la programmation physico-financière est proposé afin de permettre aux acteurs de regrouper leurs visions dans un modèle unique, tout en se plaçant sur des échelles de temps différentes. La modélisation continue développée est confrontée à la modélisation discrète (représentative de l’état de l’art) au travers d’un cas d’étude, montrant les avancées de la première vis-à-vis de la seconde. Ce métamodèle innovant a été implémenté au sein de la société MGDIS, dans le cadre d’une convention CIFRE, à l’aide d’une architecture orientée service. Cette architecture se base sur un style innovant conçu dans cette thèse afin de maximiser la capacité à paralléliser l’évaluation des modèles. La solution développée dans cette thèse a été conçue pour permettre la programmation physico-financière de gros volumes de données à l’échelle réelle. Elle a été validée sur un cas d’étude et répond aux exigences exprimées par les experts de la modélisation de programmation physico-financière de MGDIS qui ont émis un avis positif quant à l’applicabilité de la solution proposée. / In the scope of Business Intelligence, planning aims to support multiple actors in their process of converging different views and problematics from different domains to get a shared business planning model. A major difficulty in business planning is that each actor states her/his views and problematics with a different time scale. Integrating them into a unique model that represents a common state of reality becomes very costly and awkward to manage when basing the construction of these models on discrete modeling techniques used by current tools of business planning. This doctorate thesis proposes a novel solution, beyond the state-of-the-art, for addressing these issues: it conceives a novel metamodel based on a continuous time calculus. Through the developed approach, it allows multiple actors to integrate the different business logics of their planning domain in a shared model as well as to observe it from different time scales. The advantages of our solution based on continuous time against solutions based on discrete time are presented through a case study. The conceived metamodel was implemented within a real industrial set in MGDIS (a company specialized in business planning for local governments) following an innovative service oriented architecture: this architecture segregates the modeling from the evaluation to allow the parallelization of model evaluation for big volumes of data. The overall solution conceived and implemented in this thesis was designed to be a real scale prototype to be applied to real scale problems. Besides the case study, it was validated by MGDIS experts on business planning against real requirements.

Cette thèse porte sur l'intégration de données brutes provenant de sources hétérogènes sur le Web. L'objectif global est de fournir une architecture générique et modulable capable de combiner, de façon sémantique et intelligente, ces données hétérogènes dans le but de les rendre réutilisables. Ce travail est motivé par un scenario réel de l'entreprise Audience Labs permettant une mise à l'échelle de cette architecture. Dans ce rapport, nous proposons de nouveaux modèles et techniques permettant d'adapter le processus de combinaison et d'intégration à la diversité des sources de données impliquées. Les problématiques sont une gestion transparente et dynamique des sources de données, passage à l'échelle et responsivité par rapport au nombre de sources, adaptabilité au caractéristiques de sources, et finalement, consistance des données produites(données cohérentes, sans erreurs ni doublons). Pour répondre à ces problématiques, nous proposons un méta-modèle pour représenter ces sources selon leurs caractéristiques, liées à l'accès (URI) ou à l'extraction (format) des données, mais aussi au capacités physiques des sources (latence, volume). En s'appuyant sur cette formalisation, nous proposent différentes stratégies d'accès aux données, afin d'adapter les traitements aux spécificités des sources. En se basant sur ces modèles et stratégies, nous proposons une architecture orientée ressource, ou tout les composants sont accessibles par HTTP via leurs URI. En se basant sur les caractéristiques des sources, sont générés des workflows d'exécution spécifiques et adapté, permettant d'orchestrer les différentes taches du processus d'intégration de façon optimale, en donnant différentes priorités à chacune des tâches. Ainsi, les temps de traitements sont diminuées, ainsi que les volumes des données échangées. Afin d'améliorer la qualité des données produites par notre approches, l'accent est mis sur l'incertitude qui peut apparaître dans les données sur le Web. Nous proposons un modèle, permettant de représenter cette incertitude, au travers du concept de ressource Web incertaines, basé sur un modèle probabiliste ou chaque ressource peut avoir plusieurs représentation possibles, avec une certaine probabilité. Cette approche sera à l'origine d'une nouvelle optimisation de l'architecture pour permettre de prendre en compte l'incertitude pendant la combinaison des données / In this thesis, we focus on data integration of raw data coming from heterogeneous and multi-origin data sources on the Web. The global objective is to provide a generic and adaptive architecture able to analyze and combine this heterogeneous, informal, and sometimes meaningless data into a coherent smart data set. We define smart data as significant, semantically explicit data, ready to be used to fulfill the stakeholders' objective. This work is motivated by a live scenario from the French {\em Audience Labs} company. In this report, we propose new models and techniques to adapt the combination and integration process to the diversity of data sources. We focus on transparency and dynamicity in data source management, scalability and responsivity according to the number of data sources, adaptability to data source characteristics, and finally consistency of produced data (coherent data, without errors and duplicates). In order to address these challenges, we first propose a meta-models in order to represent the variety of data source characteristics, related to access (URI, authentication) extraction (request format), or physical characteristics (volume, latency). By relying on this coherent formalization of data sources, we define different data access strategies in order to adapt access and processing to data source capabilities. With help form these models and strategies, we propose a distributed resource oriented software architecture, where each component is freely accessible through REST via its URI. The orchestration of the different tasks of the integration process can be done in an optimized way, regarding data source and data characteristics. This data allows us to generate an adapted workflow, where tasks are prioritized amongst other in order to fasten the process, and by limiting the quantity of data transfered. In order to improve the data quality of our approach, we then focus on the data uncertainty that could appear in a Web context, and propose a model to represent uncertainty in a Web context. We introduce the concept of Web resource, based on a probabilistic model where each resource can have different possible representations, each with a probability. This approach will be the basis of a new architecture optimization allowing to take uncertainty into account during our combination process

Cette thèse vise à définir des techniques pour mieux exploiter les connaissances du domaine dans l’objectif de rendre compte de la réalité de systèmes qualifiés de complexes et critiques. La modélisation est une étape indispensable pour effectuer des vérifications et exprimer des propriétés qu’un système doit satisfaire. La modélisation est une représentation simplificatrice, mais réductionniste de la réalité d’un système. Or, un système complexe ne peut se réduire à un modèle. Un modèle doit s’intégrer dans sa théorie observationnelle pour rendre compte des anomalies qu’il peut y contenir. Notre étude montre clairement que le contexte est la première problématique à traiter car principale source de conflits dans le processus de conception d’un système. L’approche retenue dans cette thèse est celle d’intégrer des connaissances du domaine en associant le système à concevoir à des formalismes déclaratifs qualifiés de descriptifs appelés ontologies. Notre attention est portée au formalisme Event-B dont l’approche correct-par-construction appelée raffinement est le principal mécanisme dans ce formalisme qui permet de faire des preuves sur des représentations abstraites de systèmes pour exprimer/vérifier des propriétés de sûreté et d’invariance. Le premier problème traité concerne la représentation et la modélisation des connaissances du contexte en V&V de modèles. Suite à l’étude des sources de conflits, nous avons établi de nouvelles règles pour une extraction de connaissances liées au contexte par raffinement pour la V&V. Une étude des formalismes de représentation et d’interprétation logiques du contexte a permis de définir un nouveau mécanisme pour mieux structurer les modèles Event-B. Une deuxième étude concerne l’apport des connaissances du domaine pour la V&V. Nous définissons une logique pour le formalisme Event-B avec contraintes du domaine fondées sur les logiques de description, établissons des règles à exploiter pour l’intégration de ces connaissances à des fins de V&V. L’évaluation des propositions faites portent sur des études de cas très complexes telles que les systèmes de vote dont des patrons de conception sont aussi développés dans cette thèse. Nous soulevons des problématiques fondamentales sur la complémentarité que peut avoir l’intégration par raffinement des connaissances du domaine à des modèles en exploitant les raisonnements ontologiques, proposons de définir de nouvelles structures pour une extraction partiellement automatisée / This thesis aims at defining techniques to better exploit the knowledge provided from the domain in order to account for the reality of systems described as complex and critical. Modeling is an essential step in performing verifications and expressing properties that a system must satisfy according to the needs and requirements established in the specifications. Modeling is a representation that simplifies the reality of a system. However, a complex system can not be reduced to a model. A model that represents a system must always fit into its observational theory to account for any anomalies that it may contain. Our study clearly shows that the context is the first issue to deal with as the main source of conflict in the design process of a system. The approach adopted in this thesis is that of integrating knowledge of the domain by associating the system to design with declarative formalisms qualified of descriptive ones that we call ontologies. We pay a particular attention to the Event-B formalism, whose correct-by-construction approach called refinement is the main mechanism at the heart of this formalism, which makes it possible to make proofs on abstract representations of systems for expressing and verifying properties of safety and invariance. The first problem treated is the representation and modeling of contextual knowledge in V&V of models. Following to the study looked at the different sources of conflict, we established new definitions and rules for a refinement context knowledge extraction for Event-B V&V. A study of logical formalisms that represent and interpret the context allowed us to define a new mechanism for better structuring Event-B models. A second study concerns the contribution that domain knowledge can make to the V&V of models. We define a logic for the Event-B formalism with domain constraints based on the description logic, and we define rules to integrate domain knowledge for model V&V. The evaluation of the proposals made deal with very complex case studies such as voting systems whose design patterns are also developed in this thesis. We raise fundamental issues about the complementarity that the integration of domain knowledge can bring to Event-B models by refinement using ontological reasoning, and we propose to define a new structures for a partially automated extraction on both levels, namely the V&V