458 research outputs found
Wave-front phase retrieval in transmission electron microscopy via ptychography
No full textThere are many different strategies that allow the solving of the well-known phase problem corresponding to the loss of phase information during a physical measurement. In microscopy, and, in particular, in transmission electron microscopy, most of these strategies focus on the retrieval of high-resolution information with the importance of lower resolution data often overlooked. Ptychography offers a means to investigate such data. Ptychography is a robust diffractive imaging technique with fast convergence for phase retrieval but, until now, has not been applied at the nanoscale. In this paper, we use the ptychographical iterative engine to retrieve the phase change at the exit plane of metallic nanoparticles using a conventional transmission electron microscope. Ptychographical reconstructions yielded images with a phase resolution of π/10 and a spatial resolution of 1 nm. These results stand as a first step toward aberration-free lensless imaging. The technique lends itself to be an alternative to off-axis electron holography or focal series reconstructio
Detection of time shift failure to control of production flows in the semiconductor industry
No full textL'objectif de cette thèse en contrat CIFRE avec STMicroelectronics Crolles est de développer des méthodologies et des outils d'aide à la décision permettant de gérer efficacement les flux de production de l'usine Crolles300 en détectant au plus tôt les ralentissements voire les retards d'une ligne automatisée de production sur l'ensemble des produits. Dans ces travaux, on décrit dans un premier temps le fonctionnement des usines de semiconducteurs, les principes de planification sur des chaînes de production complexes et en particulier le fonctionnement des outils de planification. Ce contexte industriel est sujet à une forte variabilité et son analyse a permis d'identifier que la détection des retards entre la production et la planification ne pouvait se faire par comparaison qu'au niveau élémentaire des opérations sur la chaîne de production. Pour résoudre ce problème, on propose de définir un ensemble de méthodes formelles de diagnostic à base de modèle en s'appuyant sur la modélisation du système à l'aide du formalime des Graphes d'Evénements Temporisés (GET) en vue de détecter et de localiser des dérives temporelles. Les GET sont une sous-classe des réseaux de Petri temporels qui permet de représenter graphiquement des systèmes (max,+)-linéaires. Deux méthodes de détection sont proposées. La première est définie à l'aide d'observateurs (max,+) permettant d'estimer l'état courant du système faisant face à des perturbations. Cette méthode peut également être exploitée pour localiser la dérive temporelle dans le système (max,+)-linéaire. La seconde méthode proposée s'applique sur des systèmes (max,+) linéaires à temps incertain borné, c'est-à-dire des systèmes dont les temps d'attente dans les états ne sont plus fixes mais appartenant à des intervalles. Enfin, l'utilisation de ces deux méthodes est illustrée sur un exemple en s'appuyant sur des données réelles de la chaîne de production.The objective of this thesis, funded as a CIFRE contract with STMicroelectronics Crolles, is to develop methodologies and decision support tools that allow the efficient management of production flows in the Crolles300 plant by detecting, as early as possible, any slowdowns or even delays in an automated production line for all products. In this work, we first describe how semiconductor factories operate, how planning is performed on complex production lines and how planning softwares actually create production plans. This industrial business is subject to a strong variability and the analysis of this variability has led us to assert that the detection of time drifts between the real production flow and the plan could be only achieved by comparing flows at the elementary operational level of the production line. To solve this problem, we propose to define a set of formal model-based diagnostic methods over systems that can modeled as Timed Event Graph (TEG) in order to detect and localize time drifts. TEGs are a subclass of time Petri nets that graphically represent (max,+)-linear systems. Two detection methods are then proposed. The first one is based on (max,+) observers that estimate the current state of the system facing time disturbances. This method can also be used to localize time drifts in (max,+)-linear systems. The second proposed method applies to linear (max,+)-systems with bounded uncertain time, i.e. systems whose waiting time in state is no longer punctual but belongs to a time interval. Finally, the use of both methods is illustrated on an example using real data from the production line
Diagnosability and diagnosabilisation of time patterns in time Petri nets
No full textLa diagnosticabilité est la propriété d'un système de produire suffisament d'observations (par l'intermédiaire de capteurs) pour différencier les comportements nominaux des comportements fautifs. Il est possible pour un système diagnosticable pour une faute (ou défaut) donnée de produire un diagnostic certain, les informations observables retournées par le système étant différentes selon si une faute a eu lieu ou non. Vérifier une telle propriété sur un système est donc une étape importante dans le processus de construction d'algorithmes de détection et d'isolation de telles fautes. Ce problème a fait l'objet de multiples études dans les Systèmes à Événements Discrets (SED) atemporels (STL, réseaux de Petri, etc.) et dans les modèles SED temporels (automates temporisés, réseaux de Petri temporels, etc.), que ce soit pour des fautes simples (modélisées par l'occurrence d'un unique événement) ou pour des comportements plus complexes appelés motifs de faute.Dans ce travail nous proposons une méthode d'analyse de diagnosticabilité de réseaux de Petri temporels pour un nouveau type de défaut appelé motif temporel. Les motifs temporels consistent en l'occurrence de différents événements contraints temporellement. Cette méthode se base sur une abstraction des préfixes du langage d'un réseau de Petri temporel sous forme de polyèdres qui constitue la première contribution de cette thèse.La seconde contribution de ce travail est une condition nécessaire et suffisante de diagnosticabilité, qui permet d'une part de vérifier si un système est diagnosticable pour un motif temporel, et de fournir des explications structurelles de non-diagnosticabilité le cas échéant. Cette méthode se base sur l'analyse des polyèdres de l'abstraction présentée, qui sont découpés en différentes zones partageant des propriétés de diagnostic communes. De cette analyse de zones est synthétisé un graphe regroupant les différentes sources d'ambiguïtés dans les différentes exécutions du système étudié.La dernière contribution de ce travail est une méthode de vérification pour le problème de diagnosticabilisation temporelle qui consiste à paramétriser les intervalles statiques du réseau de Petri temporel initial et de trouver des valeurs pour ces paramètres pour lesquelles le réseau ainsi généré soit diagnosticable pour le motif étudié. Nous proposons une méthode de vérification de cette propriété garantissant certaines propriétés sur le réseau de Petri engendré. Cette méthode de vérification se base sur l'abstraction polyédrique précédemment citée, et consiste en la construction d'ensembles de contraintes linéaires. La vérification de l'existence de solution peut être réalisée par la suite à l'aide d'un solveur SMT.Diagnosability is the property of a system to produce sufficient observations (via sensors) to differentiate nominal behaviour from faulty behaviour. It is possible for a diagnosable system to produce a certain diagnosis for a given fault, with the observable information returned by the system being different depending on whether or not a fault has occurred. Verifying such a property on a system is therefore an important step in the process of building fault detection and isolation algorithms. This problem has been studied extensively in atemporal Discrete Event Systems (DES) (STL, Petri nets, etc.) and in temporal DES models (timed automata, time Petri nets, etc.), both for simple faults (modelled by the occurrence of a single event) and for more complex behaviour called fault patterns.In this work we propose a method for analysing the diagnosability of time Petri nets for a new type of fault called a time pattern. Time patterns consist of the occurrence of different temporally constrained events. This method is based on an abstraction of the language prefixes of a time Petri net in the form of polyhedra, which constitutes the first contribution of this thesis.The second contribution of this work is a necessary and sufficient condition for diagnosability, which makes it possible to check whether a system is diagnosable for a temporal reason, and to provide structural explanations for non-diagnosability if necessary. This method is based on the analysis of the polyhedra of the abstraction presented, which are divided into different zones sharing common diagnosis properties. From this analysis of zones, a graph is synthesised grouping together the different sources of ambiguity in the different executions of the system under study.The final contribution of this work is a verification method for the time diagnosabilisation problem, which consists of parameterising the static intervals of the initial time Petri net and finding values for these parameters for which the net thus generated is diagnosable for the pattern under study. We propose a method for verifying this property that guarantees certain properties of the generated time Petri net. This verification method is based on the polyhedral abstraction mentioned above, and consists of constructing sets of linear constraints. The existence of a solution can then be verified using an SMT solver
DdAutomata (Automata tools)
No full textDdAutomata is a set of tools to manipulate automata mainly used in the context of model based diagnosis (Diades collection). Among the proposed tools, ddautomata can determine, minimize, simulate, synchronize automata. It also can compute observers, diagnosers, fault signatures, twin plants, consistent traces..
DdAutomata (Automata tools)
No full textDdAutomata is a set of tools to manipulate automata mainly used in the context of model based diagnosis (Diades collection). Among the proposed tools, ddautomata can determine, minimize, simulate, synchronize automata. It also can compute observers, diagnosers, fault signatures, twin plants, consistent traces..
Discrete-Event systems: Symbolic representations
No full textInternational audienceDoctoralThis lecture introduces symbolic representations of discrete event systems and their use for diagnosing discrete event system
Discrete-Event systems: Diagnosis with Petri nets
No full textInternational audienceDoctoralThis lecture introduces Petri Nets and their use to solve model-based diagnosis problems
DdPetri (Outil de manipulation de réseaux de Petri pour Diades)
No full textInternational audiencePetri net library as a standalone project (source code in submodules ddpetri_subm). This library is a component of the Diades collection tools that performs model-based diagnosis on discrete event system.Until now this module provides only two command tools for untimed Petri nets: dd-lpn-dot and dd-lpn-sync.It also provides an API to manipulate Petri net and Time Petri nets (especially specific synchronization operations). Based on the file format of the Tina toolbox developed in LAAS-CNRS, Toulouse, FranceBibliothèque de réseaux de Petri en tant que projet autonome (code source dans les sous-modules ddpetri_subm). Cette bibliothèque est un composant de la collection d'outils Diades qui effectue des diagnostics basés sur des modèles sur des systèmes à événements discrets.Jusqu'à présent, ce module ne fournit que deux outils de commande pour les réseaux de Petri non temporisés : dd-lpn-dot et dd-lpn-sync.Il fournit également une API pour manipuler les réseaux de Petri et les réseaux de Petri temporels (en particulier des opérations de synchronisation spécifiques). Basé sur le format de fichier de la boîte à outils Tina développée au LAAS-CNRS, Toulouse, France
Diagnostic : étude d’un raisonnement complexe et multi-dimensionnel
No full textNational audienceDiagnosing is a general reasoning task that aims at identifying the nature of a situation (misbehaviour, illness, problem,..) by interpreting output signs (observations, measurements, alarms). This type of reasoning can be applied in many social and economical domains. This defense will present a synthesis of the contributions for the development of diagnostic agents on a various type of systems (from statical logical-based systems till timed discrete event systems). The way such agents are involved in decision processes such as corrective and predictive maintenance will be also discussed.Le diagnostic est un raisonnement général qui consiste à identifier la nature d'une situation (dysfonctionnement, maladie, problème...) par l'interprétation de signes extérieurs (observations, mesures, alarmes). Par sa nature, ce type de raisonnement peut s’appliquer à de nombreux domaines socio-économiques. Cette soutenance a pour objectif de présenter une synthèse des contributions à la mise en œuvre effective d’agents diagnostiqueurs sur des types de systèmes variés (allant des systèmes logiques statiques à des systèmes à événements discrets temporels) ainsi que de leur intégration dans des systèmes d’aide à la décision, notamment pour la maintenance corrective et prévisionnelle de systèmes
diades (Diagnostic de systèmes à événements discrets)
No full textInternational audienceDiades is a collection of tools for performing diagnosis of discrete event systems. Four tools are available:1) dd-lpn-diagnose: tool that performs the diagnosis of the occurrence of event patterns in Labeled Petri nets by a model-checking technique (see demos/dx2017)2) dd-lpn-diagnosability-checker: tool that performs the diagnosability analysis of the occurrence of event patterns in Labeled Petri nets by a model-checking technique (see demos/jdeds2017)3) dd-ltpn-diagnose: tool that performs the diagnosis of the occurrence of event patterns in Labeled Time Petri nets by a model-checking technique (see demos/dx2021)4) dd-ltpn-diagnosability-checker: tool that performs the diagnosability analysis of the occurrence of event patterns in Labeled Time Petri nets by a model-checking technique (see demos/jdeds2021)Diades est une collection d'outils permettant de diagnostiquer les systèmes à événements discrets. Quatre outils sont disponibles :1) dd-lpn-diagnose : outil qui effectue le diagnostic de l'occurrence de motifs d'événements dans les réseaux de Petri étiquetés par une technique de model-checking (voir demos/dx2017)2) dd-lpn-diagnosability-checker : outil qui effectue l'analyse de diagnostic de l'occurrence de motifs d'événements dans les réseaux de Petri étiquetés par une technique de model-checking (voir demos/jdeds2017)3) dd-ltpn-diagnose : outil qui effectue le diagnostic de l'occurrence de motifs d'événements dans les réseaux de Petri temporels étiquetés par une technique de vérification de modèle (voir demos/dx2021)4) dd-ltpn-diagnosability-checker : outil qui effectue l'analyse de diagnostic de l'occurrence de motifs d'événements dans les réseaux de Petri temporels étiquetés par une technique de model-checking (voir demos/jdeds2021
- …
