Dissertations / Theses on the topic 'Conformité de Modèles'

Dans le cadre de notre thèse, nous nous sommes intéressés à la modélisation du contrôle de conformité dans le domaine de la construction. Notre objectif principal a été de développer un modèle du contrôle de conformité d’un projet de construction relativement à un cadre réglementaire ou normatif traduit sous forme des contraintes de conformité. Nous proposons une formalisation des projets et des contraintes de conformité et des mécanismes de raisonnement permettant d’automatiser le processus de contrôle de conformité, en identifiant les causes éventuelles de non-conformité, et nous développons un modèle global du processus de contrôle intégrant des connaissances expertes. Partant du constat du manque de modèle de contrôle structuré et explicite qui prendrait en compte toute la complexité des connaissances liées au processus du contrôle et permettrait de réaliser un contrôle efficace, nous avons développé un modèle global du contrôle de conformité qui se base sur trois contributions principales : (i) une approche ontologique pour la représentation formelle des connaissances concernant le contrôle de conformité à savoir : ontologie du contrôle de conformité, requêtes de conformité, projet de construction orienté contrôle ; (ii) une méthode d’annotation sémantique et d’organisation des requêtes de conformité intégrant des connaissances sur le domaine pour un raisonnement efficace ; (iii) une modélisation de la démarche experte de contrôle basée sur l'appariement des annotations de projet et des requêtes de conformité et l'ordonnancement des requêtes de conformité pour un contrôle optimisé. Les résultats de ce travail ont été validés par le développement d'une application web qui utilise le moteur sémantique CORESE et l’environnement SeWeSe/Tomcat de développement d'applications Web sémantique. Les connaissances sont formalisées dans les langages RDF, OWL-Lite et SPARQL. Nous avons mené des expérimentations sur une base de projets de constructions et un ensemble de textes réglementaires relatifs à l'accessibilité des bâtiments, fournis par le Centre Scientifique et Technique du Bâtiment (CSTB)
In this work we are interested in modelling the conformity-checking process in the construction domain. The main objective of this research work was to model the process of checking whether a construction project (e. G. Public building) is compliant or not to a set of conformity requirements defined in construction regulations (i. E. A set of conformity constraints extracted from construction-related legal texts). We propose the formalisation of construction projects and conformity constraints, elaborate reasoning mechanisms automating the conformity-checking process by identifying eventual reasons of non-conformity, as well as developing a global conformity-checking model that integrates expert knowledge. By identifying the absence of a structured and explicit model that integrates the whole complexity of the knowledge taking part in the checking process and increases its effectiveness, we have developed a general conformity-checking model that has three main contributions : an ontological approach for the formal representation of knowledge concerning conformity-checking: conformity-checking ontology, conformity requirements, construction project oriented to conformity checking; a method for semantic annotation and organisation of conformity queries that integrates domain knowledge; modelling of the process of the conformity-checking adopted by checking engineers, which is based on matchings of project annotations and conformity queries and on scheduling of conformity queries for effective checking. The results of our research have been validated by the development of the web application that uses the semantic engine CORESE and the environment SeWeSe/Tomcat for the development of Semantic Web applications. The knowledge is formalised in the languages RDF, OWL-Lite and SPARQL. We have fulfilled the experimentations on the basis of construction projects and a set of regulation texts relating to the accessibility of public buildings that were by the Centre Scientifique et Technique du Bâtiment (CSTB)

La géométrie d'un assemblage est définie au travers de la géométrie de ses composants décrite dans la configuration nominale du produit, c'est à dire que les composants sont sans défauts et leurs positions relatives exactes. Dans la réalité, les géométries effectives des composants présentent des défauts géométriques, et leurs situations relatives ne sont pas exactes. Le travail doctoral consiste à prédire la conformité géométrique d'un assemblage aéronautique à partir des géométries de ses composants. A partir de la connaissance de la géométrie des composants avec défauts, une seconde étape vise à réaliser la simulation de l’assemblage de ces composants (propagation des défauts géométriques et couplage éléments finis) afin d’évaluer la conformité géométrique de l’assemblage, et en déduire les opérations à mener pour atteindre cette conformité. L’ensemble de la démarche sera appliqué à des nacelles aéronautiques
The assembly geometry is define through its components geometry described in their nominal configuration, in other words without geometrical deviations and with accurate relative positions. In fact, the real components geometries has geometrical deviations and their positions are not accurate. The doctoral work consists of predict the geometrical conformity of an aeronautical assembly from the geometries of its components. From knowledge of components geometry, a second step objective is to realise the simulation of assembly of this components (geometrical deviations propagation and finite elements coupling) in order to evaluate the geometrical conformity of the assembly, and to determinate the required operations in order to reach this conformity. The entire process will be applied on aeronautical nacelles

L'analyse des séries chronologiques et l'identification des systèmes nécessitent la détermination d'un modèle paramétrique d'inférence. Ce choix est donc d'une importance cruciale. Une structure de modèles inappropriée (ou sur paramétrisée) peut conduire a une complexité de calcul non nécessaire pour l'estimation de ses paramètres. A l'opposé, une structure de modèles sous-paramètrisée peut produire des résultats non significatifs. Le but principal de notre travail, est d'élaborer une méthodologie statistique générale qui puisse être utilisée pour la validation de structures de modèles les plus appropriées possibles (selon un certain sens statistique). La classe de tests développés, repose sur la construction de statistiques du minimum de Chideux, tenant compte des déviations entre les moyennes ergodiques de certaines transformations non linéaires du processus et de leur moyennes d'ensemble. Les distributions asymptotiques exactes de ces tests sont calculées sous l'hypothèse de base ho (modèle valide) et sous des hypothèses alternatives locales et globales. Pour illustrer la flexibilité de ces procédures générales, des versions explicites de ces tests sont construites, calibrées et appliquées sur des données réelles afin d'y détecter d'éventuels changements brusques de modèle. Finalement, nous présentons des résultats de simulation pour mettre en avant les performances des procédures de test ici développées

Dans cette thèse, nous nous intéressons au test de conformité qui vise à vérifier que l'implémentation d'un système satisfait à sa spécification selon une relation de conformité entre le modèle de la spécification et celui de l'implémentation. Nous avons défini le modèle RIOLTS signifiant Restrictive Input/Output Labeled Transition System et la relation de conformité rioco pour Restrictive Input/Output COnformance dont la spécificité est de permettre la description de systèmes dont certaines entrées sont interdites dans certains états. Dans la seconde partie de cette thèse nous nous intéressons à la génération de tests à partir de modèles infinis manipulant des types de données complexes, encore appelés modèles symboliques. La présence de types de données complexes rend plus difficile le problème de la sélection des tests: en effet, à la potentielle infinité des comportements d'un système s'ajoute celle des valeurs que peuvent prendre les symboles apparaissant dans les actions symboliques. De plus, des gardes peuvent conditionner les transitions ce qui nous confronte au fait que certaines traces symboliques ne sont pas faisables. Nous proposons ici une stratégie de sélection applicable sur tout modèle basé sur les systèmes de transitions symboliques. Nous utilisons un solveur de contraintes pour déterminer les chemins de l'automate de la spécification qui sont faisables. Les difficultés rencontrées pour obtenir de tels chemins de manière rapide nous ont conduit à optimiser l'utilisation du solveur. Ainsi plusieurs méthodes ont été proposées et expérimentées afin d'améliorer les temps de résolution et d'en assurer la terminaison
In this thesis, we get interested in conformance testing whose goal is to check that the implementation of a system conforms to its specification w. R. T. A conformance relation between the model of the specification and the one of the implementation. We have defined the RIOLTS model standing for Restrictive Input/Output Labeled Transition System and the conformance relation rioco standing for Restrictive Input/Output COnformance. The particularity of this model is that it makes it possible to describe systems in which some inputs are forbidden in some states. In the second part of this thesis, we have worked on test generation and selection from infinite models using complex data types. These models are called symbolic models. Complex data types makes it harder the test selection problem: we must not only deal with the possible unlimited number of behaviors of systems but also with the unlimited number of values possible for the symbols appearing in symbolic actions. Moreover as guards may condition transitions, some symbolic traces are unfeasible. We propose a selection strategy that can be applied on any model based on symbolic transition systems. We use a constraint solver to determine feasible paths of the specification automata. Such paths are difficult to calculate, and to get them faster, we have had to optimize the use of the solver. Though, we have proposed and carried out experiments on many methods to reduce solving time and ensure the termination of calculations

L'une des façons les plus efficace de s'assurer du bon fonctionnement d'un système informatique est de les représenter par des modèles mathématiques. De nombreux travaux ont été réalisés en utilisant des automates finis comme modèles, nous essayons ici d'étendre ces travaux à des modèles infinis. Dans cette thèse, nous nous intéressons à quelques problèmes dans lesquels un système est observé de façon incomplète. Dans ce cas, il est impossible d'accéder à certaines informations internes. La diagnosticabilité d'une propriété donnée consiste à vérifier qu'à l'exécution du système, un observateur sera en mesure de déterminer avec certitude que la propriété est vérifiée par le système. L'opacité consiste, réciproquement, à déterminer qu'un doute existera toujours. Une autre application concerne la génération de cas de test. Une fois encore, on considère qu'un observateur n'accède qu'à une partie des événements se produisant dans le système (en général les entrées et les sorties). À partir d'une spécification, on produit automatiquement des cas de test, qui ont pour but de détecter des non-conformités (elles même formalisées de façon précise). Ces trois problèmes ont été étudiés pour des modèles finis. Dans cette thèse, nous étendons leur étude aux modèles récursifs, pour cela nous avons introduit notre propre modèle, les RTS, qui sont une généralisation des automates à pile, et d'autres modèles de la récursivité. Nous adaptons ensuite les techniques utilisées sur des modèles finis, qui servent à résoudre les problèmes qui nous intéressent.

Les travaux présentés dans ce mémoire de thèse s'intéressent à la validation fonctionnelle de contrôleurs logiques par des techniques de test de conformité et de validation en boucle fermée. Le modèle de spécification est décrit dans le langage industriel Grafcet et le contrôleur logique est supposé être un automate programmable industriel (API) mono-tâche. Afin de contribuer à ces techniques de validation fonctionnelle, ces travaux présentent : - Une extension d'une méthode de formalisation du Grafcet par traduction sous la forme d'une machine de Mealy. Cette extension permet de produire un modèle formel de la spécification lorsque le Grafcet est implanté selon un mode d'interprétation sans recherche de stabilité, qui n'est pas préconisé dans la norme IEC 60848 mais largement utilisé dans les applications industrielles. - Une contribution au test de conformité par la définition d'un ensemble de relations de conformité basées sur l'observation de plusieurs cycles d'exécution pour chaque pas de test. - Une contribution à la validation en boucle fermée par la définition d'un critère de fin d'observation et par une technique d'identification en boite grise pour la construction et l'analyse du système en boucle fermée
The results presented in this PhD thesis deal with functional validation of logic controllers using conformance test and closed-loop validation techniques. The specification model is written in the Grafcet language and the logic controller is assumed to be a Programmable Logic Controller (PLC). In order to contribute to these validation techniques, this thesis presents: - An axtension to a fomalization methods for Grafcet languages by translation to a Mealy machine. This extension generates a formal model of a Grafcet specification that is interpreted without search of stability. This mode of interpretation is not recommended by the standard IEC 60848 but is widely used in industrial applications. - A contribution to conformance test by a definition of a set of conformance relation based on the observation of several execution cycles for each test step. - A contribution to closed-loop validation by the definition of a termination criterion and by a new gray-box identification technique that is used for construction and analysis of the closed-loop system

L'internet des objets (IoT) est aujourd'hui un moyen d'innovation et de transformation pour de nombreuses entreprises. Les applications s'étendent à un grand nombre de domaines, tels que les villes intelligentes, les maisons intelligentes, la santé, etc. Le Groupe Gartner estime à 21 milliards le nombre d'objets connectés d'ici 2020. Le grand nombre d'objets connectés introduit des problèmes, tels que la conformité et l'interopérabilité en raison de l'hétérogénéité des protocoles de communication et de l'absence d'une norme mondialement acceptée. Le grand nombre d'utilisations introduit des problèmes de déploiement sécurisé et d'évolution du réseau des IoT pour former des infrastructures de grande taille. Cette thèse aborde la problématique de la validation de l'internet des objets pour répondre aux défis des systèmes IoT. Pour cela, nous proposons une approche utilisant la génération de tests à partir de modèles (MBT). Nous avons confronté cette approche à travers de multiples expérimentations utilisant des systèmes réels grâce à notre participation à des projets internationaux. L'effort important qui doit être fait sur les aspects du test rappelle à tout développeur de système IoT que: ne rien faire est plus cher que de faire au fur et à mesure
The Internet of Things (IoT) is nowadays globally a mean of innovation and transformation for many companies. Applications extend to a large number of domains, such as smart cities, smart homes, healthcare, etc. The Gartner Group estimates an increase up to 21 billion connected things by 2020. The large span of "things" introduces problematic aspects, such as conformance and interoperability due to the heterogeneity of communication protocols and the lack of a globally-accepted standard. The large span of usages introduces problems regarding secure deployments and scalability of the network over large-scale infrastructures. This thesis deals with the problem of the validation of the Internet of Things to meet the challenges of IoT systems. For that, we propose an approach using the generation of tests from models (MBT). We have confronted this approach through multiple experiments using real systems thanks to our participation in international projects. The important effort which is needed to be placed on the testing aspects reminds every IoT system developer that doing nothing is more expensive later on than doing it on the go

Les données d'événements devenant une source d'information omniprésente, les techniques d'analyse de données représentent une opportunité sans précédent pour étudier et réagir aux processus qui génèrent ces données. Le Process Mining est un domaine émergent qui comble le fossé entre les techniques d'analyse de données, comme le Data Mining, et les techniques de management des entreprises, à savoir, le Business Process Management. L'une des bases fondamentales du Process Mining est la découverte de modèles de processus formels tels que les réseaux de Petri ou les modèles BPMN qui tentent de donner un sens aux événements enregistrés dans les journaux. En raison de la complexité des données d'événements, les algorithmes de découverte de processus ont tendance à créer des modèles de processus denses, qui sont difficiles à interpréter par les humains. Heureusement, la Vérification de Conformité, un sous-domaine du Process Mining, permet d'établir des liens entre le comportement observé et le comportement modélisé, facilitant ainsi la compréhension des correspondance entre ces deux éléments d'information sur les processus. La Vérification de Conformité est possible grâce aux artefacts d'alignement, qui associent les modèles de processus et les journaux d'événements. Il existe différents types d'artefacts d'alignement, à savoir les alignements, les multi-alignements et les anti-alignements. Actuellement, seuls les alignements sont traités en profondeur dans la littérature scientifique. Un alignement permet de relier le modèle de processus à une instance de processus donnée. Cependant, étant donné que de nombreux comportements existent dans les logs, l'identification d'un alignement par instance de processus nuit à la lisibilité des relations log-modèle.La présente thèse propose d'exploiter les artefacts de conformité pour regrouper les exécutions de processus enregistrées dans les journaux d'événements, et ainsi extraire un nombre restrictif de représentations modélisées. Le regroupement de données, communément appelé partitionnement, est une méthode courante pour extraire l'information de données denses et complexes. En regroupant les objets par similarité dans des clusters, le partitionnement permet d'extraire des ensembles de données plus simples qui englobent les similarités et les différences contenues dans les données. L'utilisation des artefacts de conformité dans une approche de partitionnement permet de considérer un modèle de processus fiable comme une base de référence pour le regroupement des instances de processus. Ainsi, les clusters découverts sont associés à des artefacts modélisés, que nous appelons variantes modélisées des traces, ce qui fournit des explications opportunes sur les relations entre le journal et le modèle.Avec cette motivation, nous avons élaboré un ensemble de méthodes pour calculer les artefacts de conformité. La première contribution est le calcul d'un comportement modélisé unique qui représente un ensemble d'instances de processus, à savoir le multi-alignement. Ensuite, nous proposons plusieurs approches de partitionnement basées sur l'alignement qui fournissent des clusters d'instances de processus associés à un artefact modélisé. Enfin, nous soulignons l'intérêt de l'anti-alignement pour extraire les déviations des modèles de processus par rapport au journal. Ce dernier artefact permet d'estimer la précision du modèle. Nous montrons son impact sur nos approches de partitionnement basées sur des modèles. Nous fournissons un encodage SAT pour toutes les techniques proposées. Des heuristiques sont ensuite ajoutées pour tenir compte de la capacité de calcul des ordinateurs actuels, au prix d'une perte d'optimalité
As event data becomes an ubiquitous source of information, data science techniques represent an unprecedented opportunity to analyze and react to the processes that generate this data. Process Mining is an emerging field that bridges the gap between traditional data analysis techniques, like Data Mining, and Business Process Management. One core value of Process Mining is the discovery of formal process models like Petri nets or BPMN models which attempt to make sense of the events recorded in logs. Due to the complexity of event data, automated process discovery algorithms tend to create dense process models which are hard to interpret by humans. Fortunately, Conformance Checking, a sub-field of Process Mining, enables relating observed and modeled behavior, so that humans can map these two pieces of process information. Conformance checking is possible through alignment artefacts, which associate process models and event logs. Different types of alignment artefacts exist, namely alignments, multi-alignments and anti-alignments. Currently, only alignment artefacts are deeply addressed in the literature. It allows to relate the process model to a given process instance. However, because many behaviors exist in logs, identifying an alignment per process instance hinders the readability of the log-to-model relationships.The present thesis proposes to exploit the conformance checking artefacts for clustering the process executions recorded in event logs, thereby extracting a restrictive number of modeled representatives. Data clustering is a common method for extracting information from dense and complex data. By grouping objects by similarities into clusters, data clustering enables to mine simpler datasets which embrace the similarities and the differences contained in data. Using the conformance checking artefacts in a clustering approach allows to consider a reliable process model as a baseline for grouping the process instances. Hence, the discovered clusters are associated with modeled artefacts, that we call model-based trace variants, which provides opportune log-to-model explanations.From this motivation, we have elaborated a set of methods for computing conformance checking artefacts. The first contribution is the computation of a unique modeled behavior that represents of a set of process instances, namely multi-alignment. Then, we propose several alignment-based clustering approaches which provide clusters of process instances associated to a modeled artefact. Finally, we highlight the interest of anti-alignment for extracting deviations of process models with respect to the log. This latter artefact enables to estimate model precision, and we show its impact in model-based clustering. We provide SAT encoding for all the proposed techniques. Heuristic algorithms are then added to deal with computing capacity of today’s computers, at the expense of loosing optimality

Cette thèse porte sur l'aide à la construction de machines d'états UML de systèmes réactifs. Elle vise à définir un cadre théorique et pragmatique pour mettre en oeuvre une approche incrémentale caractérisée par une succession de phases de construction, évaluation et correction de modèles. Ce cadre offre des moyens de vérifier si un nouveau modèle est conforme à ceux définis durant les étapes précédentes sans avoir à demander une description explicite des propriétés à vérifier. Afin de pouvoir analyser les machines d'états, nous leur associons une sémantique LTS ce qui nous a conduit à définir une procédure de transformation automatique de machines d'états en LTS. Dans un premier temps, nous avons défini et implanté des techniques de vérification de relations de conformité de LTS (red, ext, conf, et confrestr). Dans un second temps, nous nous sommes intéressés à la définition d'un cadre de construction incrémentale dans lequel plusieurs stratégies de développement peuvent être mises en \oe uvre en s'assurant que le modèle final élaboré sera une implantation conforme à la spécification initiale. Ces stratégies reposent sur des combinaisons de raffinements qui peuvent être de deux types : le raffinement vertical pour éliminer l'indéterminisme et ajouter des détails ; le raffinement horizontal pour ajouter de nouvelles fonctionnalités sans ajouter d'indéterminisme. Enfin, nous transposons la problématique de construction incrémentale d'une machine d'états à la construction d'architectures dont les composants sont des machines d'états. Des conditions sont définies pour assurer la conformité entre des architectures dans le cas de la substitution de composants.

Ce manuscrit de thèse porte sur le problème du test basé modèle de systèmes de production existants, tels ceux de notre partenaire industriel Michelin, l’un des trois plus grands fabricants de pneumatiques au monde. Un système de production est composé d’un ensemble de machines de production contrôlées par un ou plusieurs logiciels au sein d’un atelier dans une usine. Malgré les nombreux travaux dans le domaine du test basé modèle, l’écriture de modèles permettant de décrire un système sous test ou sa spécification reste un problème récurrent, en partie à cause de la complexité d’une telle tâche. De plus, un modèle est utile lorsqu’il est à jour par rapport à ce qu’il décrit, ce qui implique de le maintenir dans le temps. Pour autant, conserver une documentation à jour reste compliqué puisqu’il faut souvent le faire manuellement. Dans notre contexte, il est important de souligner le fait qu’un système de production fonctionne en continu et ne doit être ni arrêté ni perturbé, ce qui limite l’usage des techniques de test classiques. Pour pallier le problème de l’écriture de modèles, nous proposons une approche pour construire automatiquement des modèles depuis des séquences d’événements observés (traces) dans un environnement de production. Pour se faire, nous utilisons les informations fournies par les données échangées entre les éléments qui composent un système de production. Nous adoptons une approche boîte noire et combinons les notions de système expert, inférence de modèles et machine learning, afin de créer des modèles comportementaux. Ces modèles inférés décrivent des comportements complets, enregistrés sur un système analysé. Ces modèles sont partiels, mais également très grands (en terme de taille), ce qui les rend difficilement utilisable par la suite. Nous proposons une technique de réduction spécifique à notre contexte qui conserve l’équivalence de traces entre les modèles de base et les modèles fortement réduits. Grâce à cela, ces modèles inférés deviennent intéressant pour la génération de documentation, la fouille de données, mais également le test. Nous proposons une méthode passive de test basé modèle pour répondre au problème du test de systèmes de production sans interférer sur leur bon fonctionnement. Cette technique permet d’identifier des différences entre deux systèmes de production et réutilise l’inférence de modèles décrite précédemment. Nous introduisons deux relations d’implantation : une relation basée sur l’inclusion de traces, et une seconde relation plus faible proposée, pour remédier au fait que les modèles inférés soient partiels. Enfin, ce manuscrit de thèse présente Autofunk, un framework modulaire pour l’inférence de modèles et le test de systèmes de production qui aggrège les notions mentionnées précédemment. Son implémentation en Java a été appliquée sur différentes applications et systèmes de production chez Michelin dont les résultats sont donnés dans ce manuscrit. Le prototype développé lors de la thèse a pour vocation de devenir un outil standard chez Michelin
This thesis tackles the problem of testing (legacy) production systems such as those of our industrial partner Michelin, one of the three largest tire manufacturers in the world, by means of Model-based Testing. A production system is defined as a set of production machines controlled by a software, in a factory. Despite the large body of work within the field of Model-based Testing, a common issue remains the writing of models describing either the system under test or its specification. It is a tedious task that should be performed regularly in order to keep the models up to date (which is often also true for any documentation in the Industry). A second point to take into account is that production systems often run continuously and should not be disrupted, which limits the use of most of the existing classical testing techniques. We present an approach to infer exact models from traces, i.e. sequences of events observed in a production environment, to address the first issue. We leverage the data exchanged among the devices and software in a black-box perspective to construct behavioral models using different techniques such as expert systems, model inference, and machine learning. It results in large, yet partial, models gathering the behaviors recorded from a system under analysis. We introduce a context-specific algorithm to reduce such models in order to make them more usable while preserving trace equivalence between the original inferred models and the reduced ones. These models can serve different purposes, e.g., generating documentation, data mining, but also testing. To address the problem of testing production systems without disturbing them, this thesis introduces an offline passive Model-based Testing technique, allowing to detect differences between two production systems. This technique leverages the inferred models, and relies on two implementation relations: a slightly modified version of the existing trace preorder relation, and a weaker implementation proposed to overcome the partialness of the inferred models.Overall, the thesis presents Autofunk, a modular framework for model inference and testing of production systems, gathering the previous notions. Its Java implementation has been applied to different applications and production systems at Michelin, and this thesis gives results from different case studies. The prototype developed during this thesis should become a standard tool at Michelin

Est-il possible de tester automatiquement le comportement temporisé des systèmes interactifs temps réel ? Ces travaux proposent une solution en fournissant un ensemble d’outils de test basé sur modèles pour Systèmes Musicaux Interactifs (SMI). Les SMIs doivent calculer et réagir pendant une performance musicale et ainsi accompagner les musiciens. Certains de ces SMIs peuvent être basés sur partition et doivent, dans ce cas, suivre à tout prix les contraintes temporelles imposées par le document haut-niveau appelé partition. En somme, pendant une performance, le système doit réagir en temps réel aux signaux audio venant des musiciens en suivant cette partition. Ceci demande au système une forte fiabilité temporelle et une robustesse face aux erreurs pouvant arriver en entrée du système. Hors, la vérification formelle de propriétés, comme la fiabilité temporelle avant l’exécution du système lors d’une performance, est insuffisamment traitée par la communauté de l’informatique musicale. Nous présentons dans cette thèse, la réalisation d’un ensemble d’outils de test basé sur modèles appliqué à un SMI. Il est à noter que ces outils de test ont été définis formellement dans le but de tester plus généralement le comportement temporelle des systèmes interactifs temps réel prenant en compte des évènements discrets et des durées définissables sur des échelles multiples. Pour ce résumé nous présentons rapidement l’état de l’art de nos travaux avant d’introduire la définition de notre modèle créé pour spécifier les aspects évènementiel («event-triggerred») et temporel («timed-driven») des SMIs. Ce modèle a la particularité d’être automatiquement construit depuis les conditions temporelles définies dans un document haut-niveau et peut être traduit vers un réseau d’Automates Temporisés (TA). Dans le cadre de la performance musique mixte électronique/instrumentale nous avons introduit une notion de durée multi-temps gérée par notre modèle et une génération de trace d’entrée musicalement pertinente par notre ensemble d’outils de test. Pour tester un SMI selon les différentes attentes de l’utilisateur, notre ensemble d’outils a été implémenté avec plusieurs options possibles. Parmi ces options, la possibilité de tester automatiquement, selon une approche différée ou temps réel, la conformité temporelle du SMI est proposée. En effet, l’approche différée utilise des outils de la gamme du logiciel Uppaal [44] pour générer une suite de traces d’entrées exhaustive et garantir la conformité temporelle du système testé. Il est également possible de tester une trace d’entrée particulière ou une version altérée («fuzzed») de la trace idéale définie par la partition. L’approche temps réel interprète quand-à elle directement le modèle comme des instructions de byte-code grâce à une machine virtuelle. Finalement, des expériences ont été conduites via une étude de cas sur le suiveur de partition Antescofo. Ces expériences ont permis de tester ce système et d’évaluer notre ensemble d’outils et ses différentes options. Ce cas d’étude applique nos outils de test sur Antescofo avec succès et a permit d’identifier des bogues parfois non triviaux dans ce SMI
Can real-time interactive systems be automatically timed tested ? This work proposes an answer to this question by providing a formal model based testing framework for Interactive Music Systems (IMS). IMSs should musically perform computations during live performances, accompanying and acting like real musicians. They can be score-based, and in this case must follow at all cost the timed high-level requirement given beforehand, called score. During performance, the system must react in real-time to audio signals from musicians according to this score. Such goals imply strong needs of temporal reliability and robustness to unforeseen errors in input. Be able to formally check this robustness before execution is a problem insufficiently addressed by the computer music community. We present, in this document, the concrete application of a Model-Based Testing (MBT) framework to a state-of-the-art IMS. The framework was defined on purpose of testing real-time interactive systems in general. We formally define the model in which our method is based. This model is automatically constructed from the high-level requirements and can be translated into a network of time automata. The mixed music environment implies the management of a multi-timed context and the generation of musically relevant input data through the testing framework. Therefore, this framework is both time-based, permitting durations related to different time units, and event-driven, following the musician events given in input. In order to test the IMS against the user’s requirements, multiple options are provided by our framework. Among these options, two approaches, offline and online, are possible to assess the system timed conformance fully automatically, from the requirement to the verdict. The offline approach, using the model-checker Uppaal, can generate a covering input suite and guarantee the system time reliability, or only check its behavior for a specific or fuzzed input sequence. The online approach, directly interprets the model as byte-code instructions thanks to a virtual machine. Finally, we perform experiments on a real-case study: the score follower Antescofo. These experiments test the system with a benchmark of scores and a real mixed-score given as input requirements in our framework. The results permit to compare the different options and scenarios in order to evaluate the framework. The application of our fully automatic framework to real mixed scores used in concerts have permitted to identify bugs in the target IMS

L’adoption obligatoire des normes IFRS en Europe vise à améliorer la fiabilité et la comparabilité de l’information financière des sociétés cotées. Cependant, un tel objectif ne peut pas être atteint seulement en exigeant des sociétés d’adopter un référentiel comptable commun de qualité, mais aussi en surveillant l’application de celui-ci. S’il existe un certain nombre de travaux sur la surveillance des normes comptables en général et des IFRS en particulier, à notre connaissance, peu de recherches ont été menées sur les aspects techniques de vérification de la conformité à celles-ci. L’objectif de cette recherche est d’élaborer un modèle technique de vérification de la conformité aux IFRS à utiliser par la deuxième ligne de contrôle externe constituée par les autorités de surveillance. La méthodologie suivie est qualitative, s’est appuyée sur une étude exploratoire et l’observation empirique du système de contrôle de l’information financière de l’AMF, complétées par des entretiens avec les contrôleurs de l’AMF et des questionnaires réalisés auprès d’analystes financiers et de commissaires aux comptes de sociétés cotées en France. Le modèle a été élaboré selon l’approche par les risques qui consiste à évaluer le risque de non-conformité aux IFRS à travers trois composantes (risque inhérent, risque du contrôle interne et risque lié à l’audit), dans le but d’orienter la vérification vers les zones importantes comportant un risque de non-conformité. Le modèle a été ensuite testé sur des cas réels par des contrôleurs impliqués dans la vérification des états financiers d’émetteurs à l’AMF. Les résultats des tests montrent que si certains éléments se sont avérés difficilement appréhendables dans le cadre du contrôle externe secondaire, le modèle constitue un outil efficace pour relever les zones importantes de risque de non-conformité aux IFRS. En outre, l’utilisation du modèle pourrait aider à sensibiliser les contrôleurs à l’analyse des risques
The mandatory adoption of IFRS in Europe is aimed at improving the quality and the comparability of financial information of listed companies. Nevertheless, such goal cannot be achieved solely by making a requirement for EU companies to use the IFRS, but it would be also necessary to assure the compliance with those standards. While there is recent research that addresses the issues on enforcement of accounting standards in general and of IFRS in particular, there is still a lack of studies which discuss the technical aspects of monitoring compliance with accounting standards. The objective of this research is to elaborate a technical model of enforcement of IFRS to be used by the regulatory oversight bodies. The methodology adopted is qualitative, based on an exploratory study and empirical observation of the financial information oversight system of the AMF in France, completed by the interviews with the controllers at the AMF and by the surveys carried out with financial analysts and auditors of listed companies. Our model has been developed following the risk-based approach which consist of assessing the risk of non-compliance with IFRS by the analysis of three risk components (inherent risk, control risk and audit risk), in order to focus the review efforts on those important areas which are more likely to contain a risk of non-compliance. The model was then tested in practical cases (issuers’ financial statements) by the controllers of the AMF. The tests results indicate that if some factors had been proved difficult to be assessed at the regulatory oversight level, the model constitute a relevant methodological tool for risk detection which helps to identify important areas of risk of non-compliance with the IFRS. In addition, the use of the model can help to make the controllers sensitive to risk analysis

Nous sommes interesses par le test de systemes temps-reels a base de modele. Plus precisement, nous etudions deux classes de problemes, a savoir: (1) les problemes d'identification d'etat (II) le test de conformite en boite noire. Pour les problemes d'identification d'etat, nous disposons du modele de la machine dont nous ignorons l'etat initial et nous cherchons une experience a appliquer sur cette machine afin d'identifier l'etat initial inconnu ou l'etat final vers lequel la machine a evolue suite a cette experience. Pour le test de conformite, nous disposons du modele de la machine et nous voulons tester si la machine est conforme a son modele ou pas. Notre approche est basee principalement sur le modele d'automate temporise non-deterministe et partiellement observable. L'observabilite partielle et le non-determinisme sont des elements essentiels pour simplifier la modelisation ainsi que pour augmenter l'expressivite et l'implementabilite des systemes. Ce cadre permet'a l'utilisateur de definir, par une modelisation appropriee, des hypotheses sur l'environnement du systeme sous test (SST) ainsi que sur l'interface entre le testeur et le SST. Avant de resoudre les problemes d'identification d'etat pour le cas des automates temporises, nous etudions ces problemes pour le cas des transducteurs a etats finis(TEF). TEF est une extension du modele de la machine de Mealy. Nous montrons que ces problemes sont indecidables pour les TEF en general. Nous considerons une sous-classe de TEF, nommee, transducteurs avec attente de synchronisation (TEF-AS) pour laquelle ces problemes sont decidables. La premiere etape pour resoudre les problemes d'identification pour le cas des automates temporises consiste a calculer le "time-abstracting bisimulation (TAB) quotient graph" de l'automate temporise en question. La deuxieme etape consiste a transformer ce graphe en une machine de Mealy pour laquelle les problemes d'identification peuvent se resoudre en utilisant des techniques deja existantes. Pour le test de conformite en boite-noire, nous considerons deux types de tests: tests a horloge analogique et tests a horloge numerique. Notre algorithme pour la generation de tests a horloge analogique est base sur la determinisation a-la-volee de l'automate specification, durant l'execution du test, qui repose a son tour sur des calculs d'atteignabilite. Ces derniers peuvent etre parfois couteux, et par consequent problematiques, puisque le testeur doit reagir rapidement aux actions du systeme sous test. Pour cela, nous proposons des techniques permettant de representer les testeurs a horloge analogique sous forme d'automates temporises deterministes, reduisant ainsi le temps de reaction a un simple saut d'etat. Nous proposons des algorithmes de generation statique ou a-la-volee de tests a horloge numerique. Ces tests mesurent le temps avec des horloges numeriques a precision finie, qui est une condition essentielle d'implementabilite. Nous proposons une technique pour la couverture des noeuds, des arcs ou des etats, en reduisant le probleme a une couverture d'un graphe d'atteignabilite symbolique. Ceci permet d'eviter de generer un grand nombre de tests. Nous proposons egalement des techniques de generation de test a horloge numerique basees sur les techniques de raffinement pour reduire la taille des Tests generes. Nous decrivons notre outil prototype TTG ainsi que quatre etudes de cas: un systeme d'eclairage, le Bounded Retransmission Protocol, le K9 Mars Rover (NASA) et le Robot Dala (LAAS)
We are interested in model-based testing for real-time systems. Specifically, we study two classes of problems, namely: (I) state identification problems and (II) black-box conformance testing. For state identification problems, we are given the model of a machine with an initial unknown state and we look for an experiment to apply on the machine to identify the initial unknown state or the final state to which the machine has moved after the experiment. For black-box conformance testing, we are given a model of the machine and we want to check whether the machine conforms to its model or not. Our framework is mainly based on the model of partially-observable, nondeterministic timed automata. We argue that partial observability and non-determinism are essential features for ease of modeling, expressiveness and implementability. The framework allows the user to define, through appropriate modeling, assumptions on the environment of the system under test (SUT) as well as on the interface between the tester and the SUT. Before solving state identification problems for timed automata, we study these problems for the case of finite state transducers (FST). FST is an extension of the Mealy machine model. We show that these problems are undecidable for FST in general. We consider a subclass of FST, so-called, wait-synchronize transducers (WSFST) for which these problems are decidable. The first step to solve state identification problems for timed automata, consists in computing the time-abstracting bisimulation (TAB) quotient graph of the considered timed automaton. The second step is to transform this graph into a Mealy machine on which state-identification problems can be solved using existing techniques. For conformance testing, we consider two types of tests: analog-clock tests and digital-clock tests. Our algorithm to generate analog-clock tests is based on an on-the-fly determinization of the specification automaton during the execution of the test, which in turn relies on reachability computations. The latter can sometimes be costly, thus problematic, since the tester must quickly react to the actions of the system under test. Therefore, we provide techniques which allow analog-clock testers to be represented as deterministic timed automata, thus minimizing the reaction time to a simple state jump. We provide algorithms for static or on-the-fly generation of digital-clock tests. These tests measure time only with finite-precision, digital clocks, an essential condition for implementability. We propose a technique for location, edge and state coverage of the specification, by reducing the problem to covering a symbolic reachability graph. This avoids having to generate too many tests. We also propose digital-clock test generation techniques based on action refinement in order to reduce the size of generated tests. We report on a prototype tool TTG and four case studies: a lighting device, the Bounded Retransmission Protocol, the K9 Mars Rover (NASA) and the Dala Robot (LAAS)

Cet ouvrage aborde la génération de grilles de Voronoï sous contrainte pour réduire les erreurs liées à la géométrie des cellules lors de la simulation réservoir. Les points de Voronoï sont optimisés en minimisant des fonctions objectif correspondant à différentes contraintes géométriques. L'originalité de cette approche est de pouvoir combiner les contraintes simultanément : - la qualité des cellules, en plaçant les points de Voronoï aux barycentres des cellules ; - le raffinement local, en fonction d'un champ de densité [rho], correspondant à la perméabilité, la vitesse ou la vorticité ; - l'anisotropie des cellules, en fonction d'un champ de matrice M contenant les trois vecteurs principaux de l'anisotropie, dont l'un est défini par le vecteur vitesse ou par le gradient stratigraphique ; - l'orientation des faces des cellules, en fonction d'un champ de matrice M contenant les trois vecteurs orthogonaux aux faces, dont l'un est défini par le vecteur vitesse ; - la conformité aux surfaces du modèle structural, failles et horizons ; - l'alignement des points de Voronoï le long des puits. La qualité des grilles générées est appréciée à partir de critères géométriques et de résultats de simulation comparés à des grilles fines de référence. Les résultats indiquent une amélioration de la géométrie, qui n'est pas systématiquement suivie d'une amélioration des résultats de simulation
Voronoi grids are generated under constraints to reduce the errors due to cells geometry during flow simulation in reservoirs. The Voronoi points are optimized by minimizing objective functions relevant to various geometrical constraints. An original feature of this approach is to combine simultaneously the constraints: - Cell quality, by placing the Voronoi points at the cell barycenters. - Local refinement according to a density field rho, relevant to permeability, velocity or vorticity. - Cell anisotropy according to a matrix field M built with the three principal vectors of the anisotropy, which one is defined by the velocity vector or by the stratigraphic gradient. - Faces orientation according to a matrix field M built with the three vectors orthogonal to the faces, which one is defined by the velocity vector. - Conformity to structural features, faults and horizons. - Voronoï points alignment along well path. The quality of the generated grids is assessed from geometrical criteria and from comparisons of flow simulation results with reference fine grids. Results show geometrical improvements, that are not necessarily followed by flow simulation results improvements

Est-il possible de tester automatiquement le comportement temporisé des systèmes interactifs temps réel ? Ces travaux proposent une solution en fournissant un ensemble d’outils de test basé sur modèles pour Systèmes Musicaux Interactifs (SMI). Les SMIs doivent calculer et réagir pendant une performance musicale et ainsi accompagner les musiciens. Certains de ces SMIs peuvent être basés sur partition et doivent, dans ce cas, suivre à tout prix les contraintes temporelles imposées par le document haut-niveau appelé partition. En somme, pendant une performance, le système doit réagir en temps réel aux signaux audio venant des musiciens en suivant cette partition. Ceci demande au système une forte fiabilité temporelle et une robustesse face aux erreurs pouvant arriver en entrée du système. Hors, la vérification formelle de propriétés, comme la fiabilité temporelle avant l’exécution du système lors d’une performance, est insuffisamment traitée par la communauté de l’informatique musicale. Nous présentons dans cette thèse, la réalisation d’un ensemble d’outils de test basé sur modèles appliqué à un SMI. Il est à noter que ces outils de test ont été définis formellement dans le but de tester plus généralement le comportement temporelle des systèmes interactifs temps réel prenant en compte des évènements discrets et des durées définissables sur des échelles multiples. Pour ce résumé nous présentons rapidement l’état de l’art de nos travaux avant d’introduire la définition de notre modèle créé pour spécifier les aspects évènementiel («event-triggerred») et temporel («timed-driven») des SMIs. Ce modèle a la particularité d’être automatiquement construit depuis les conditions temporelles définies dans un document haut-niveau et peut être traduit vers un réseau d’Automates Temporisés (TA). Dans le cadre de la performance musique mixte électronique/instrumentale nous avons introduit une notion de durée multi-temps gérée par notre modèle et une génération de trace d’entrée musicalement pertinente par notre ensemble d’outils de test. Pour tester un SMI selon les différentes attentes de l’utilisateur, notre ensemble d’outils a été implémenté avec plusieurs options possibles. Parmi ces options, la possibilité de tester automatiquement, selon une approche différée ou temps réel, la conformité temporelle du SMI est proposée. En effet, l’approche différée utilise des outils de la gamme du logiciel Uppaal [44] pour générer une suite de traces d’entrées exhaustive et garantir la conformité temporelle du système testé. Il est également possible de tester une trace d’entrée particulière ou une version altérée («fuzzed») de la trace idéale définie par la partition. L’approche temps réel interprète quand-à elle directement le modèle comme des instructions de byte-code grâce à une machine virtuelle. Finalement, des expériences ont été conduites via une étude de cas sur le suiveur de partition Antescofo. Ces expériences ont permis de tester ce système et d’évaluer notre ensemble d’outils et ses différentes options. Ce cas d’étude applique nos outils de test sur Antescofo avec succès et a permit d’identifier des bogues parfois non triviaux dans ce SMI
Can real-time interactive systems be automatically timed tested ? This work proposes an answer to this question by providing a formal model based testing framework for Interactive Music Systems (IMS). IMSs should musically perform computations during live performances, accompanying and acting like real musicians. They can be score-based, and in this case must follow at all cost the timed high-level requirement given beforehand, called score. During performance, the system must react in real-time to audio signals from musicians according to this score. Such goals imply strong needs of temporal reliability and robustness to unforeseen errors in input. Be able to formally check this robustness before execution is a problem insufficiently addressed by the computer music community. We present, in this document, the concrete application of a Model-Based Testing (MBT) framework to a state-of-the-art IMS. The framework was defined on purpose of testing real-time interactive systems in general. We formally define the model in which our method is based. This model is automatically constructed from the high-level requirements and can be translated into a network of time automata. The mixed music environment implies the management of a multi-timed context and the generation of musically relevant input data through the testing framework. Therefore, this framework is both time-based, permitting durations related to different time units, and event-driven, following the musician events given in input. In order to test the IMS against the user’s requirements, multiple options are provided by our framework. Among these options, two approaches, offline and online, are possible to assess the system timed conformance fully automatically, from the requirement to the verdict. The offline approach, using the model-checker Uppaal, can generate a covering input suite and guarantee the system time reliability, or only check its behavior for a specific or fuzzed input sequence. The online approach, directly interprets the model as byte-code instructions thanks to a virtual machine. Finally, we perform experiments on a real-case study: the score follower Antescofo. These experiments test the system with a benchmark of scores and a real mixed-score given as input requirements in our framework. The results permit to compare the different options and scenarios in order to evaluate the framework. The application of our fully automatic framework to real mixed scores used in concerts have permitted to identify bugs in the target IMS

Pour satisfaire aux nouveaux besoins de flexibilité, modularité, d'adaptabilité et de distribution des applications, les paradigmes composants et services ont été déclinés dans des frameworks reconnus comme J2EE, OSGI, SCA ou encore Fractal. Néanmoins, ceux-ci offrent peu d'outils permettant de garantir la fiabilité des applications en raisonnant de manière générique sur leur configuration architecturale et les spécifications des participants. Dans cette thèse, j'envisage l'organisation de la vérification des assemblages, et le diagnostic des défaillances, sous l'angle de l'approche par contrat dirigée par les responsabilités. Pour cela, j'analyse d'abord sous quelles hypothèses intégrer différents formalismes à cette approche, puis comment appliquer cette approche à différentes architectures. J'étudie par ailleurs comment les intervenants de la mise en oeuvre des systèmes pourraient en bénéficier. Cela m'amène à présenter un modèle de contrat, qui intègre et organise différentes propriétés, analysées comme requises pour la validité de l'assemblage, conjointement et uniformément sur différentes architectures. J'en définis le modèle objet qui réifie la logique contractuelle, ainsi que son implémentation sous forme d'un framework. Ce dernier est validé sur l'architecture Fractal et deux formalismes contractuels, l'un à base d'assertions et l'autre de contraintes sur les séquences d'interactions valides entre participants. Une validation plus avancée est montrée sur l'exemple d'une application de communautés instantanées.

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 œuvre 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.

Les travaux présentés dans ce mémoire de thèse s'intéressent à la génération et à la mise en œuvre de séquences de test pour le test de conformité de contrôleurs logiques. Dans le cadre de ces travaux, le Grafcet (IEC 60848 (2002)), langage de spécification graphique utilisé dans un contexte industriel, a été retenu comme modèle de spécification. Les contrôleurs logiques principalement considérés dans ces travaux sont les automates programmables industriels (API). Afin de valider la mise en œuvre du test de conformité pour des systèmes de contrôle/commande critiques, les travaux présentés proposent: - Une formalisation du langage de spécification Grafcet. En effet, l'application des méthodes usuelles de vérification et de validation nécessitent la connaissance du comportement à partir de modèles formels. Cependant, dans un contexte industriel, les modèles utilisés pour la description des spécifications fonctionnelles sont choisis en fonction de leur pouvoir d'expression et de leur facilité d'utilisation, mais ne disposent que rarement d'une sémantique formelle. - Une étude de la mise en œuvre de séquences de test et l'analyse des verdicts obtenus lors du changement simultané de plusieurs entrées logiques. Une campagne d'expérimentation a permis de quantifier, pour différentes configurations de l'implantation, le taux de verdicts erronés dus à ces changements simultanés. - Une définition du critère de SIC-testabilité d'une implantation. Ce critère, déterminé à partir de la spécification Grafcet, définit l'aptitude d'une implantation à être testée sans erreur de verdict. La génération automatique de séquences de test minimisant le risque de verdict erroné est ensuite étudiée.

Les travaux présentés dans ce mémoire de thèse s'intéressent à la génération et à la mise en œuvre de séquences de test pour le test de conformité de contrôleurs logiques. Dans le cadre de ces travaux, le Grafcet (IEC 60848 (2002)), langage de spécification graphique utilisé dans un contexte industriel, a été retenu comme modèle de spécification. Les contrôleurs logiques principalement considérés dans ces travaux sont les automates programmables industriels (API). Afin de valider la mise en œuvre du test de conformité pour des systèmes de contrôle/commande critiques, les travaux présentés proposent: - Une formalisation du langage de spécification Grafcet. En effet, l'application des méthodes usuelles de vérification et de validation nécessitent la connaissance du comportement à partir de modèles formels. Cependant, dans un contexte industriel, les modèles utilisés pour la description des spécifications fonctionnelles sont choisis en fonction de leur pouvoir d'expression et de leur facilité d'utilisation, mais ne disposent que rarement d'une sémantique formelle. - Une étude de la mise en œuvre de séquences de test et l'analyse des verdicts obtenus lors du changement simultané de plusieurs entrées logiques. Une campagne d'expérimentation a permis de quantifier, pour différentes configurations de l'implantation, le taux de verdicts erronés dus à ces changements simultanés. - Une définition du critère de SIC-testabilité d'une implantation. Ce critère, déterminé à partir de la spécification Grafcet, définit l'aptitude d'une implantation à être testée sans erreur de verdict. La génération automatique de séquences de test minimisant le risque de verdict erroné est ensuite étudiée
The works presented in this PhD thesis deal with the generation and implementation of test sequences for conformance test of logic controllers. Within these works, Grafcet (IEC 60848 (2002)), graphical specification language used in industry, has been selected as the specification model. Logic controllers mainly considered in these works are Programmable Logic Controllers (PLC). In order to validate the carrying out of conformance test of critical control systems, this thesis presents: - A formalization of the Grafcet specification language. Indeed, to apply usual verification and validation methods, the behavior is required to be expressed through formal models. However, in industry, the models used to describe functional specifications are chosen for their expression power and usability, but these models rarely have a formal semantics. - A study of test sequences execution and analysis of obtained verdicts when several logical inputs are changed simultaneously. Series of experimentation have permitted to quantify, for different configurations of the implantation under test, the rate of erroneous verdicts due to these simultaneous changes. - A definition of the SIC-testability criterion for an implantation. This criterion, determined on the Grafect specification defines the ability of an implementation to be tested without any erroneous verdict. Automatic generation of test sequences that minimize the risk of erroneous verdict is then studied

Une preoccupation majeure dans le domaine des reseaux et systemes repartis est le test. Nous nous sommes interesses au test de conformite qui a pour but de verifier si une implantation est conforme a une specification de protocole donnee. Nous avons elabore des methodes permettant de repondre aux questions fondamentales du test de conformite: comment generer et selectionner des cas de test ? quelle est la couverture d'une suite de test ? la methode de generation proposee utilise la theorie des langages formels et en particulier la theorie du monoide. Les specifications sont representees par des automates. Un langage permet de decrire des objectifs de test. A partir des objectifs de test, on calcule les sous-specifications cibles correspondantes. Des criteres de generation sont exprimes sous forme de regles que doivent respecter les sequences generees. La couverture est etudiee en fonction de criteres de couverture exprimes grace au meme langage que les objectifs de test. La mesure de couverture consiste dans un premier temps a verifier qu'un critere de couverture est teste par au moins une sequence de test. Dans un deuxieme temps, une metrique de couverture est definie permettant de mieux apprecier la qualite d'une suite de test. La particularite commune a ces deux methodes est leur adaptabilite a un probleme de test particulier (modele de fautes, architecture de test, objectifs de test)

Cette thèse a été effectuée dans le cadre du projet Guide mené conjointement par le laboratoire de génie informatique et le centre de recherche Bull de Grenoble depuis mi 86. Guide est le support d'un ensemble de recherches sur la programmation des applications reparties. Ces recherches sont entreprises sur la base du développement d'un système expérimental : le système Guide. Ce dernier est un système d'exploitation reparti à objets qui fournit un haut niveau d'intégration (invisibilité de la répartition notamment). Un premier prototype du système fonctionne depuis fin 88 et permet la programmation et la mise œuvre d'applications par l'intermédiaire d'un langage de programmation spécifique. La thèse contient une présentation et une évaluation du modèle de programmation par objets mis œuvre par ce langage: la présentation met en évidence les principaux choix de conception et les justifie; l'évaluation est basée sur une étude comparative des modèles d'objets de Guide, de Trellis/Owl, d'Emerald et d'Eiffel, et sur des expériences de programmation réalisées sur le prototype. Elle met en évidence les aspects caractéristiques du modèle d'objets de guide, ses apports et ses limites

Cette thèse porte sur la génération de tests à partir d’un modèle pour les systèmes GALS (Globalement Asynchrones et Localement Synchrones). La combinaison des aspects synchrones et asynchrones en font des systèmes complexes, imposant de recourir à de nouvelles méthodes d’analyse. Pour faire face à cette complexité, nous explorons trois directions : (1) techniques pour les composants synchrones ; (2) techniques pour les protocoles de communication entre les composants ; et (3) techniques pour des systèmes GALS complets, combinant les résultats des deux directions précédentes.Dans la première direction, nous explorons des techniques formelles pour le test fonctionnel de composants synchrones. En tant qu’étude de cas, nous reprenons l’algorithme d’authentification de message (MAA), une fonction cryptographique conçue au milieu des années 80. Nous formalisons cet algorithme en tant que flux de données synchrone. La modélisation et la validation du MAA nous ont permis de découvrir diverses erreurs dans les spécifications (informelles et formelles) préalables du MAA, les vecteurs de test et code des normes ISO 1987 et ISO 1990 ; dans les compilateurs et outils de vérification que nous avons utilisés.Dans la seconde direction, nous explorons la formalisation et le test fonctionnel d’un protocole de communication. Dans notre étude de cas, nous évaluons le protocole d’établissement d’une liaison sécurisé au niveau de la couche de transport (TLS), responsable de l’authentification et de l’échange de clés nécessaires pour établir ou reprendre une communication sécurisée. Notre modèle de la version 1.3 TLS a été validé par une approche utilisant notre nouvel outil de génération de cas de test de conformité à la volée, nommé TESTOR, développé à partir de la boı̂te à outils CADP. Cet outil explore le modèle et génère automatiquement un ensemble de cas de tests ou un graphe de test complet (CTG),à exécuter sur une implémentation physique d’un système.Dans la troisième direction, nous proposons une méthodologie de test permettant d’analyser les systèmes GALS dans leur ensemble. Nous tirons parti de la génération de tests de conformité des systèmes asynchrones pour dériver automatiquement des scénarios réalistes (contraintes d’entrées et oracles), qui sont ardus à concevoir manuellement et sujet d’erreurs. Ainsi, notre méthodologie intègre (1) modèles concurrents synchrones et asynchrones; (2) les tests unitaires fonctionnels et les tests de conformité comportementale; et (3) diverses méthodes formelles et leurs outils. Nous illustrons notre méthodologie sur un exemple simple, mais représentatif inspiré des voitures autonomes
This dissertation focuses on the model-based testing of GALS (GloballyAsynchronous and Locally Synchronous) systems, which are inherentlycomplex because of the combination of synchronous and asynchronous aspects.To cope with this complexity, we explore three directions:(1) techniques for synchronous components;(2) techniques for communication protocols between components; and(3) techniques for complete GALS systems, combining theresults of the two previous directions.In the first direction, we explore formal techniques for the functionaltesting of synchronous components.As a case-study, we reconsider the Message Authenticator Algorithm(MAA), a pioneering cryptographic function designed in the mid-80s, andformalize it as a synchronous dataflow.The modeling and validation of the MAA enabled us to discover variousmistakes in prior (informal and formal) specifications of the MAA, thetest vectors and code of the ISO 1987 and ISO 1990 standards, and incompilers and verification tools used by us.In the second direction, we explore the formalization and the functionaltesting of a communication protocol. As a case-study, we reconsider the formalization of the Transport Layer Security (TLS) handshake, a protocol responsible for the authentication and exchange of keys necessary to establish or resume a secure communication.Our model of the TLS version 1.3 has been validated by an approach using our new on-the-fly conformance test case generation tool, named TESTOR, developed on top of the CADP toolbox.TESTOR explores the model and generates automatically a set of controllable testcases or a complete test graph (CTG) to be executed on a physical implementation ofthe system.In the third direction, we propose a testing methodology for GALSsystems combining the two previous directions.We leverage the conformance test generation for asynchronous systems toautomatically derive realistic scenarios (inputs constraints andoracles), which are necessary ingredients for the unit testing of individual synchronouscomponents, and are difficult and error-prone to design manually.Thus our methodology integrates(1) synchronous and asynchronous concurrent models;(2) functional unit testing and behavioral conformance testing;and (3) various formal methods and their tool equipments.We illustrate our methodology on a simple, but relevant example inspiredby autonomous cars

Dans cette thèse on s'est intéressé à l'étude de problèmes concernant la théorie des écoulements compressibles. Dans une première partie on a traité le problème de transport instationnaire avec un champ de vitesse peu régulier, on a établi un résultat d'existence en passant à la limite sur des schémas numériques volumes finis avec un choix décentré amont qui garantie la positivité de la masse volumique. Pour le problème de Stokes, le résultat est démontré par deux approches : une approche par schéma numérique et une approche par régularité visqueuse.Dans la première méthode on propose une discrétisation qui combine la méthode des éléments finis et la méthode des volumes finis qui repose sur les espaces Crouzeix-Raviart. Une première difficulté de ce travail est de démontrer les estimations sur la solution discrète, en particulier à cause de la présence de la gravité dans le terme source de l'équation de quantité de mouvement. Le fait de considérer une loi d'état très générale conduit des difficultés supplémentaires en particulier dans le passage à la limite sur cette équation.Dans la deuxième méthode, le résultat d'existence est démontré en utilisant une approximation par viscosité. Ceci consiste essentiellement en deux parties : l'étude du problème de convection diffusion (qui apparait dans le problème régularisé) où on démontre l'existence et l'unicité de solution et en deuxième partie le passage à la limite sur le problème régularisé
This thesis is concerned with the study of problems relating in the theory of compressible flows . We prove the existence of the considered problems in a first part by passing to the limit on the numerical schemes proposed for the discretisation of these problems. In the second part, the existence result is obtained by passing to the limit on the approximate solutions given by a corresponding regularized problem.The main result is to prove the existence of a solution of the stationnary compressible Stokes problem with a general equation of state.We first prove this result by passing to the limit on the numerical scheme as the mesh size tends to zero. The fact to consider a general E.O.S induces some additional difficulties in particular to get estimates on the discrete solution (which comes also from the presence of the gravity in the momentum equation) and in the passage to the limit on the E.O.S.We also prove the existence result by passing to the limit on a regularized problem. We first treat the convection-diffusion problem (which appears in the regularized problem), we give an existence and uniqueness result, and we then prove estimates on the approwimate solutions and pass to the limit on the regularized problem

La culture de sécurité s'impose à l'agenda des entreprises. Cette notion n'est pas nouvelle puisque le terme est apparu dès la fin des années 80 suite à l'accident de Tchernobyl. L'existence d'une culture de sûreté défaillante a été la principale cause expliquant la catastrophe.L'usage du terme s'est très largement répandu et les définitions sont nombreuses. En croisant différents travaux, trois grands facteurs explicatifs se révèlent prédominants dans la culture de sécurité : les facteurs " organisationnel ", " comportemental " et " psychologique ".L'objectif de ce travail de thèse est de concevoir un " système " de modèles permettant de décrire et d'évaluer sur le terrain chacun des trois facteurs. Pour ce faire, des " raccourcis " (ou " réductions " théorique et méthodologique), qui seront discutées et justifiées, ont été explorés.Ainsi, le facteur " organisationnel " est traduit selon le processus de l'analyse des conformités légales (le rapport au prescrit). ". Le facteur " comportemental " quant à lui assimilé au processus de maîtrise des risques (le rapport au réel). Enfin, le facteur " psychologique " est directement relié au processus d'évaluation du " climat de sécurité ".Chaque processus a fait l'objet d'un effort de modélisation. Chacun des modèles a permis de repérer des variables descriptives et explicatives. Certaines ont été reliées dans le but de traduire la relation entre les trois facteurs.Le " système " de modèles ainsi constitué a fait l'objet d'une expérimentation à grande échelle conduite en partenariat avec une entreprise française de rang mondial. Deux sites ont été impliqués. La thèse détaille le cadre théorique et méthodologique. Elle présente la démarche de modélisation mise en œuvre et discute amplement des résultats de l'expérimentation. Elle propose enfin des pistes de généralisation du dispositif constitué.

La culture de sécurité s'impose à l'agenda des entreprises. Cette notion n'est pas nouvelle puisque le terme est apparu dès la fin des années 80 suite à l'accident de Tchernobyl. L'existence d'une culture de sûreté défaillante a été la principale cause expliquant la catastrophe.L'usage du terme s'est très largement répandu et les définitions sont nombreuses. En croisant différents travaux, trois grands facteurs explicatifs se révèlent prédominants dans la culture de sécurité : les facteurs « organisationnel », « comportemental » et « psychologique ».L'objectif de ce travail de thèse est de concevoir un « système » de modèles permettant de décrire et d'évaluer sur le terrain chacun des trois facteurs. Pour ce faire, des « raccourcis » (ou « réductions » théorique et méthodologique), qui seront discutées et justifiées, ont été explorés.Ainsi, le facteur « organisationnel » est traduit selon le processus de l'analyse des conformités légales (le rapport au prescrit). ». Le facteur « comportemental » quant à lui assimilé au processus de maîtrise des risques (le rapport au réel). Enfin, le facteur « psychologique » est directement relié au processus d'évaluation du « climat de sécurité ».Chaque processus a fait l'objet d'un effort de modélisation. Chacun des modèles a permis de repérer des variables descriptives et explicatives. Certaines ont été reliées dans le but de traduire la relation entre les trois facteurs.Le « système » de modèles ainsi constitué a fait l'objet d'une expérimentation à grande échelle conduite en partenariat avec une entreprise française de rang mondial. Deux sites ont été impliqués. La thèse détaille le cadre théorique et méthodologique. Elle présente la démarche de modélisation mise en œuvre et discute amplement des résultats de l'expérimentation. Elle propose enfin des pistes de généralisation du dispositif constitué
Safety culture is increasingly important to the corporate agenda. The SafetyCulture concept is not new, but gained popularity in the late 80s following the Chernobyl accident. The main cause of the disaster was said to be a deficient Safety culture.The term is now used widely and definitions are numerous. The Safety culture literature contains three major explanatory factors shaping the formation of a safety culture: "organizational", "behavioural" and "psychological".The objective of this thesis is to develop a "system" of models which will enable description and evaluation of these three factors in applied settings. To achieve this goal, theoretical and methodological "shortcuts", or mappings, were developed and explored. The "organizational" factor is mapped with the process of compliance management. Similarly, the "behavioural" factor is likened to the process of risk management. Finally, the "psychological" factor is directly related to the assessment process of the "safety climate". The implications of these translations are discussed in this thesis.Each of these processes has been modelled. Every model has allowed the identification of descriptive and explanatory variables. Some have been linked to each other in order to translate the relationship between the three factors. The "system" of models was tested on a large sample in partnership with a global French company. Two locations were involved.This thesis describes the theoretical and methodological framework. It describes the modelling process that has been implemented and discusses the results of the experimentation. Finally it proposes possibilities for the enhancement of the models that have been developed

Un des objectifs prioritaires des industries aéronautiques est la réduction de la masse des structures, tout en permettant l'amélioration de leurs performances. Ceci passe notamment par l'utilisation de matériaux composites et le recours croissant à la simulation numérique, permettant la minimisation du nombre d'essais physiques et l'optimisation des structures.L'enjeu de ces travaux est de pouvoir calculer précisément, sur des matériaux architecturés, l'influence de la microstructure, modélisée par exemple directement par tomographie, sur la tenue de pièces complètes. Pour prendre en compte à la fois l'ensemble de la pièce et les effets de son chargement, une approche global/local multiéchelle semble adaptée tant du point de vue des méthodes de calcul que des modèles matériaux utilisés.Pour répondre à cette problématique, une méthode de couplage entre des modèles qui décrivent une même structure, mais à des échelles différentes, a été développée. Elle repose sur une séparation micro-macro des quantités d’interface, dans la zone de raccord surfacique entre les deux modèles. Pour faciliter son utilisation dans les bureaux d’étude, une technique de résolution itérative non-intrusive est également présentée. Elle permet de mettre en œuvre la méthode de couplage proposée dans un environnement logiciel industriel qui utilise bien souvent des codes éléments finis commerciaux fermés. La méthode est systématiquement comparée à d'autres méthodes de couplage de la littérature et la qualité des solutions est quantifiée par comparaison à une solution de référence obtenue par un calcul direct à l'échelle fine.Les principaux résultats sont encourageants dans la mesure où ils montrent, dans des cas d'étude représentatifs bidimensionnels et tridimensionnels, sous des hypothèses d’élasticité linéaire, des solutions cohérentes avec les théories de l’homogénéisation au premier et second ordre. De fait, les solutions obtenues sont systématiquement de meilleure qualité avec la méthode proposée qu'avec les méthodes de la littérature, non-adaptées à des cas de couplage pour modèles non-compatibles.Finalement, les perspectives sont multiples en raison des différentes alternatives de la méthode qui, dans un contexte industriel, pourrait offrir un véritable outil d'analyse visant à introduire un modèle local décrit à l'échelle fine dans un modèle global macroscopique homogénéisé
One of the priority objectives of the aeronautics industry is to reduce the mass of structures while improving their performances. This involves the use of composite materials and the increasing use of digital simulation to optimize structures.The major challenge of this project is to be able to accurately calculate the local variations of the microstructure - for instance detected by tomography and directly modelled from tomogram - on the behavior of an architectured material part. In order to take into account the whole structure and its load effects, a multi-scale approach seems to be a natural choice. Indeed, the related models to the part and its microstructure might use different formalisms according to each scale.In this context, a coupling formulation was proposed in order to replace, in a non-intrusive way, a part of a homogenized macroscopic finite-element model by a local one described at a microscopic level. It is based on a micro-macro separation of interface quantities in the coupling area between the two models. To simplify its use in design offices, a non-intrusive iterative resolution procedure has also been proposed. It allows the implementation of the proposed coupling method in an industrial software environment that often uses closed commercial finite element codes. Different mechanical problems under linear elasticity assumption are proposed. The proposed method is systematically compared with other coupling methods of the literature and the quality of the solutions is quantified compared to a reference one obtained by direct numerical simulation at a fine scale.The main results are promising as they show, for representatives test cases under linear elasticity assumption in two and three-dimensions, solutions that are consistent with first- and second-order homogenization theories. The solutions obtained with the proposed method are systematically the best approximations of the reference solution whereas the methods of the literature are less accurate and shown to be unsuitable to couple non-compatible models.Finally, there are many perspectives due to the different alternatives of the method which could become, in an industrial context, a real analytic tool that aims to introduce a local model described at a fine scale, into a homogenized macroscopic global one

Ce travail traite d’un problème de pollution liée à la présence de métaux de base dans des passifs environnementaux issus d’un traitement métallurgique des minerais sulfureux cuivre – zinc provenant de la mine de Kipushi en République Démocratique du Congo. L’objectif principal de ce travail a été d’arriver à proposer des scénarios de gestion durable au passif environnemental de la filière présentant les risques environnementaux les plus élevés. Pour cela, on a d’abord procédé à une identification des différents problèmes environnementaux tout au long de la filière de traitement sur les quatre sites d’exploitation. Ensuite on a prélevé des échantillons puis procéder par des tests de disponibilité à la lixiviation à l’eau déminéralisée pour évaluer les fractions solubles des métaux de base présents et aussi par des tests de conformité de mise en décharge afin de classer ces rejets conformément à la directive européenne 2003-33-CE. Ainsi, les rejets Ex – UZK ont été identifiés comme les plus dangereux de la filière au regard de cette directive, car les quantités lixiviées de cuivre et de zinc dans ces rejets ont dépassé largement les limites fournies par la directive, et donc ils ne peuvent même pas être mis en décharge de classe I sans traitement métallurgique préalable pouvant permettre leur dépollution.

Par contre, les autres rejets de la filière, en l’occurrence les rejets de flottation de Kipushi et les scories de fusion pour matte de cuivre, peuvent eux être acceptés en décharge de classe I, sans traitement préalable au regard des limites fournies par la même directive. Les procédés de lixiviation acide chaude et de digestion ont été proposés et retenus comme scénarios de gestion durable à appliquer à ces rejets Ex – UZK, car ils se réalisent tous deux en milieu acide sulfurique d’une part et d’autre part leur application et surtout leur faisabilité en République Démocratique du Congo reste possible ;en outre ils aboutissent à des nouveaux rejets contenant le fer sous forme d’hématite, pouvant être stocké aisément et durablement dans la nature, ce qui est conforme au principe du développement durable. Nous avons tenté de modéliser ces deux scénarios en discutant et comparant la circulation des flux de matière dans les deux procédés, d’abord autour de chaque opération métallurgique unitaire, et ensuite sur l’ensemble du procédé. Ainsi nous avons pu chiffrer tous les flux entrant et sortant dans le système étudié, en considérant 1000 kg de rejets Ex –UZK alimentés. Cette quantification nous a permis de comparer les coûts opératoires de ces deux procédés. Les résultats obtenus dans la présente étude sont encourageants et nous ont permis de formuler des recommandations pour les études ultérieures éventuelles dont les résultats pourront l’enrichir davantage, notamment sur les aspects technologiques, économiques et environnementaux, de manière à faciliter les applications sur terrain.

This work deals with environmental liabilities consisting of base metals pollution due to metallurgical processing of copper – zinc sulphide ores in Kipushi mine in Democratic Republic of Congo. The main objective of this work was to propose sustainable management scenarios for the most important environmental liabilities from metallurgical sector. For this purpose, liabilities were first identified on four metallurgical plants. Then, leaching tests with deionized water were carried out to assess the soluble fractions of base metals. These effluents were also classified according to the test described in european decision 2003-33-EC, which determines the conformity of waste to landfill. Ex – UZK effluents are the most dangerous from this sector, according to this directive, since the quantities of leached copper and zinc were far beyond the limits :they cannot be sent to class I landfill without prior metallurgical processing. However, other effluents like flotation wast and Lubumbashi slag originating from melting for copper matte, are acceptable without prior treatment. Hot acid leaching and digestion were proposed as sustainable management scenarios for to these Ex – UZK waste because :both can be performed in sulfuric acid and they are feasible in Democratic Republic of Congo. They also lead to an iron – rich waste consisting of hematite that can be stored easily and sustainably in nature, which is consistent with the principle of sustainable development. We have modeled these two scenarios by discussing and comparing the flows in both processes, first for each individual metallurgical unit process, and then for the whole chain of value. So we could assess all the inputs and outputs of the studied system, expressed per ton of Ex – UZK waste. The operating costs of both processes were calculated and compared. The results are encouraging. Recommendations were proposed for further studies, in order to investigate more deeply the technological, economical and environmental aspects, to facilitate the final application.
Doctorat en Sciences
info:eu-repo/semantics/nonPublished

Les simulateurs de conduite sont utilisées par l'industrie automobile pour le développement de systèmes d'aide à la conduite, des études d'ergonomie, de design, ou encore du comportement des conducteurs. L'objectif est d'améliorer la sécurité des véhicules, et de réduire coûts et délais des projets. Dans les simulateurs, le conducteur évolue dans un trafic simulé dont le réalisme est crucial pour la validité des résultats : les réactions d'un conducteur sont d'autant plus correctes qu'il perçoit l'environnement comme réel. Dans les approches centrées individu, comme ici le trafic, un des critères important pour le réalisme est la variété comportementale des agents. De plus, les comportements doivent également être cohérents : l'apparition de situations aberrantes est très pénalisante pour l'immersion. Cependant, ces deux aspects ne sont généralement pas pris en compte simultanément. Dans ce travail, nous nous sommes donc intéressés à la question suivante : dans les approches centrées individus, augmenter la variété des comportements des agents tout en préservant leur cohérence améliore-t-il le réalisme ? Par ailleurs, le contexte industriel des travaux, effectués en convention Cifre chez Renault, impliquait des besoins spécifiques : il fallait concevoir un outil qui permette à la fois aux experts de spécifier des comportements variés et cohérents, et aux utilisateurs finaux de les exploiter facilement. Nous proposons dans ce travail un modèle de différenciation comportementale, qui se décline en un outil dont les principaux apports sont d'être générique, non-intrusif, et de permettre une conception en dehors de l'agent. Le modèle s'articule selon trois axes. Tout d'abord, il décrit les comportements des agents par des normes. Celles-ci fournissent un profil comportemental à la conception, et un contrôle de la conformitéà l'exécution. Ensuite, le processus de génération des comportements permet d'autoriser la création d'agents déviants ou en violation. Il influe pour cela sur le déterminisme du mécanisme. Enfin, les normes peuvent être inférées à partir de simulations enregistrées ou de situations réelles, afin d'analyser les résultats des expérimentations et d'automatiser la configuration du modèle. Nous avons appliqué cet outil à la simulation de trafic dans scaner, l'application développée et utilisée par le Centre Technique de Simulation de Renault pour ses simulateurs de conduite. Les modules logiciels développés au cours de la thèse introduisent dans le trafic des styles de conduite spécifiés sous forme de normes, par exemple des conducteurs prudents ou agressifs. Ils permettent ensuite de peupler l'environnement de manière automatisée, et de faire évoluer facilement les scénarios existants. Ces développements sont d'ores et déjà intégrés dans la version commerciale de l'application. Au delà de l'amélioration subjective du réalisme, les expérimentations réalisées démontrent les apports de l'outil sur la variété et la représentativité des comportements obtenus.

Avec le développement de la fabrication additive (FA), l'intégration de la chaîne numérique et des normes d'échange de données deviennent un enjeu majeur. La chaîne numérique comporte différentes propres phases, dont notamment l’industrialisation et la fabrication. L'échange de données FA peut exploiter divers formats d'impression, tels que STL, AMF, 3MF et STEP. Par conséquent, la standardisation de la chaîne numérique et des formats de données devient un sujet de recherche majeur. Pour développer une approche permettant une meilleure intégration de la chaîne numérique, en particulier pour l’industrialisation et la fabrication une standardisation des formats de données est nécessaire pour améliorer l'interopérabilité entre les différentes applications informatiques (CAO / IPAO / FAO / MOCN). Deux types de problèmes doivent être surmontés : le premier est lié à l'intégration des processus clés, le second est lié au format de données. La contribution de la thèse s’appuie sur les normes STEP / STEP-NC pour les phases d’industrialisation et de fabrication. La première contribution propose la procédure de spécification de la chaîne numérique de FA, mobilisant des concepts, des normes, une représentation de modèle, des langages modélisation et une évaluation de modèle relatifs à cette technologie. La deuxième contribution, le modèle de données de processus FA, est proposée pour traiter les problèmes d'interopérabilité des données dans les phases d’industrialisation et de fabrication qui définissent les objets et entités de l'application, et créent des modèles de données du processus. La troisième contribution porte sur l'analyse de la conformité du modèle de données proposé, qui fournit la méthode d'analyse spécifique pour les opérations de fabrication par couche ou le trajet de la tête d’impression. Enfin, les propositions sont ensuite mises en œuvre dans une architecture globale exploitant la plateforme CatalystEX. Cette architecture assure une démonstration de l’interopérabilité du modèle de données proposé et met en œuvre une étude de cas à partir d’une pièce test NIST. Pour intégrer toutes les informations relatives à la planification et à la fabrication, un fichier physique étendu basé sur STEP / STEP-NC a été créé par STEP Partie-21 pour illustrer la planification de l'impression et les opérations spécifiques
Regarding the rapid development of additive manufacturing (AM) technology, the integration of digital thread and the standard of data exchange are becoming a huge trend. Digital thread has its own several stages, including production engineering and manufacturing operations. AM data exchange mainly focuses on various print formats, such as STL, AMF, 3MF, and STEP. Therefore, digital thread and information standard become increasing significant. In order to achieve a better integration of digital thread, data standard is needed further to enhance the interoperability among various computer-aided X systems (CAD/CAPP/CAM/CNC). Two kinds of problems must be overcome. The first problem is linked to process-related integration while the second is related to data standard. The contribution of the thesis is based on STEP/STEP-NC standards to integrated production engineering and manufacturing operations. The first contribution proposes the fundamental guideline for specifying AM digital thread, including concepts, standards, model representation, descriptive languages, and model assessment. The second contribution, AM process data model, is proposed to address the issues of data interoperability on production engineering and manufacturing operations that defines application objects and entities, and definitions process of data models. The third contribution focuses on the conformance assessment for proposed data model. It provides the specific analysis way for manufacturing layer and head path, respectively. Finally, the propositions are then implemented by a global architecture based on CatalystEX Platform. Such an architecture makes a demonstration on the interoperability of the developed data model and presents the use of a case study for NIST testing part. In order to integrate all the related information on production planning and manufacturing operations, extended STEP/STEP-NC physical file has been accomplished by STEP Part-21 to demonstrate the print planning and AM operations

Ce travail a pour objectif de développer et d'appliquer une méthode originale permettant de simuler l'écoulement dans un milieu poreux fracturé. Cette méthode repose sur une approche multicouches double continuum permettant de séparer le comportement des différents aquifères présents sur un site. La résolution des écoulements, basée sur la méthode des Eléments Finis de Crouzeix-Raviart, est associée à une méthode inverse (minimisation de type Quasi-Newton combinée à la méthode de l'état adjoint) et à une paramétrisation multi-échelle.La méthode est appliquée dans un premier temps sur l'aquifère fracturé du site expérimental de Poitiers. Les résultats montrent une bonne restitution du comportement de l'aquifère et aboutissent à des champs de transmissivité plus réguliers par rapport à ceux de l'approche simple continuum. L'application finale est réalisée sur le site de Cadarache (taille plus importante et données d'entrée moins denses). Le calage des deux aquifères présents sur le site est satisfaisant et montre que ceux-ci se comportent globalement de façon indépendante. Ce calage pourra être amélioré localement grâce à données de recharge plus fines.