Ce travail porte sur la vérification de composants logiciels dans les systèmes embarqués critiques avioniques. Les conséquences d’une erreur dans de tels systèmes pouvant s'avérer catastrophiques, il se doivent de respecter leur spécification. La vérification formelle tend à prouver cette adéquation si elle est vraie, ou à produire un contre-exemple si elle ne l’est pas. Les méthodes actuelles ne sont pas capable de traiter les les systèmes industriels. La découverte d’informations supplémentaires (invariants) sur le système permet de réduire l’espace de recherche afin de renforcer l’objectif de preuve: les informations découvertes sont suffisantes pour conclure “facilement”. Nous définissons une architecture parallèle permettant à des méthodes de découverte d’invariants de collaborer autour d’un moteur de kinduction. Dans ce contexte nous proposons HullQe, une nouvelle heuristique de génération d’invariants potentiels combinant un calcul de pré-image par élimination de quantificateurs et des calculs d’enveloppes convexes. Nous montrons que HullQe est capable, automatiquement, de renforcer des objectifs de preuve correspondant à la vérification de patrons de conception courants en avionique. Pour autant que nous sachions, les méthodes actuelles sont incapables de conclure sur ces problèmes. Nous détaillons nos améliorations de l’algorithme d’élimination de quantificateurs de Monniaux afin d’assurer le passage à l’échelle sur nos systèmes. Notre framework formel Stuff est une implémentation de notre architecture parallèle composée de HullQe, d'une technique de découverte d’invariants basée sur des templates, et d'une généralisation de PDR à l’arithmétique. / This work studies the verification of software components in avionics critical embedded systems. As the failure of suchsystems can have catastrophic consequences, it is mandatory to make sure they are consistent with their specification.Formal verification consists in proving that a system respects its specification if it does, or to produce a counterexample if itdoes not. Current methods are unable to handle the verification problems stemming from realistic systems. Discoveringadditional information (invariants) on the system can however restrict the search space enough to strengthen the proofobjective: the information discovered allow to "easily" reach a conclusion. We define a parallel architecture for invariantdiscovery methods allowing them to collaborate around a k-induction engine. In this context we propose a new heuristic forthe generation of potential invariants by combining an iterated preimage calculus by quantifier elimination with convexhull computations, called HullQe. We show that HullQe is able to automatically strengthen proof objectives correspondingto safety properties on widespread design patterns in our field. To the best of our knowledge, these systems elude currenttechniques. We also detail our improvements to the quantifier elimination algorithm by David Monniaux in 2008, so that itscales to computing preimages on our systems. Our formal framework Stuff is an implementation of the parallel architecturewe propose in which we implemented not only HullQe, but also a template-based invariant discovery technique, and ageneralisation to Property Directed Reachability to linear real arithmetic and integer octagons.

This work concerns the fractionation of phosphorus present in sediments from the Macela Reservoir, located in the city of Itabaiana (Sergipe State, Brazil). Two sediment cores were obtained, each to a depth of approximately 30 cm, which were divided into 5 cm sections. The analytical method employed a Standards, Measurements, and Testing (SMT) protocol, in which the phosphorus was split into the fractions: total (PT), inorganic (PI), organic (PO), non-apatite (PNAP), and apatite (PAP). The technique was validated in terms of the limits of detection (DL) and quantification (QL) for each fraction. No significant contamination was observed. The accuracy was in the range 99-101%, and the relative standard deviation (RSD) was better than 2%. The measured phosphorus concentrations were in the ranges 441.60-1335.47 µg g-1 (PT), 409.54-1209.86 µg g-1 (PI), and 21.35-195.87 µg g-1 (PO). For the inorganic forms, the concentrations of PNAP and PAP were in the ranges 106.82-541.09 µg g-1 and 238.56-698.01 µg g-1, respectively. The concentrations of the phosphorus fractions were highest in Core 2. The contents of Fe, Al, Ca, and Corg were 3.45-4.95%, 4.85-7.73%, 1.02-1.89%, and 1.88-8.55%, respectively. Correlation analysis using the Spearman test identified iron and aluminum as the most important controlling factors for P in the sediments studied. The application of principal components analysis (PCA) and hierarchical clustering analysis (HCA) to the measured parameters divided the sediment samples into two groups, according to their similarities. This was also confirmed using analysis of variance (ANOVA, p<0.05). / Neste trabalho foi realizado o fracionamento do fósforo em sedimentos do Reservatório Macela, localizado na cidade de Itabaiana, Sergipe, Brasil. Foram tomados dois testemunhos com profundidade de aproximadamente 30 cm cada, que foram seccionados de 5 cm em 5 cm. O método analítico utilizado foi o Protocolo desenvolvido pelo Standards, Measurements and Testing (SMT), que fracionou o fósforo nos sedimentos em total (PT), inorgânico (PI), orgânico (PO), não apatita (PNAP) e apatita (PAP). A validação da metodologia foi verificada através dos valores de limite de detecção (LD) e de limite de quantificação (LQ) para PT, PI, PO, PNAP e PAP, onde se observou que não houve contaminação significativa. A exatidão do método foi conferida através dos valores de concordância variando 99 a 101% e o desvio padrão relativo (RSD) foi melhor que 2%. A concentração de P variaram entre 441,60 e 1335,47 µg g-1 para PT, entre 409,54 e 1209,86 µg g-1 para PI e entre 21,35 e 195,87 µg g-1 para Po. Para as formas inorgânicas o valor das concentrações de PNAP variou de 106,82 e 541,09 µg g-1 e de PAP variou de 238,56 a 698,01 µg g-1. As concentrações das frações de fósforo nos sedimentos analisados foram maiores no testemunho II. Os conteúdos de Fe, Al, Ca e Corg variaram de 3,45 a 4,95 %, de 4,85 a 7,73 %, de 1,02 a 1,89 % e de 1,88 a 8,55 %. A matriz de correlação de Sperman identificou o ferro e o alumínio como os fatores controladores mais importantes dos P nos sedimentos analisados. A análise de componentes principais (PCA) e analise de agrupamento hierárquico (HCA), aplicada aos parâmetros medidos, dividiu as amostras de sedimentos em dois grupos, de acordo com suas similaridades. Esta tendência foi confirmada pela análise de variância (ANOVA, p< 0,05).

The subject of this diploma thesis is the design of a conveyor superstructure of a collaborative mobile robot MiR. The first part is a theoretical research basis focused on mobile collaborative technologies and information related to Mobile industrial Robots. The following is a practical part built on previous acquired knowledge. The key issue of the solution is the logistics transport of the PCB magazine in the field of SMT industry. There are created two structural design variants of the superstructure arrangement for the transport of two binders and the most suitable variant is selected on the basis of the multicriteria basic method. The selected alternative of the conveyor top module is then subjected to design calculations. In order to obtain a comprehensive overview of the prototype production, the following section contains drawing documentation, including relevant comments, an economic cost estimate and a risk analysis.

Chez les personnes post-AVC (Accident Vasculaire Cérébral), spasticité, faiblesse et toute autre coactivation anormale proviennent de limitations dans la régulation de la gamme des seuils des réflexes d'étirement. Nous avons voulu savoir si les déficits dans les influences corticospinales résiduelles contribuaient à la limitation de la gamme des seuils et au développement de la spasticité chez les patients post-AVC. La stimulation magnétique transcranienne (SMT) a été appliquée à un site du cortex moteur où se trouvent les motoneurones agissant sur les fléchisseurs et extenseurs du coude. Des potentiels évoqués moteurs (PEM) ont été enregistrés en position de flexion et d'extension du coude. Afin d'exclure l'influence provenant de l'excitabilité motoneuronale sur l'évaluation des influences corticospinales, les PEM ont été suscités lors de la période silencieuse des signaux électromyographiques (EMG) correspondant à un bref raccourcissement musculaire juste avant l'enclenchement de la SMT. Chez les sujets contrôles, il y avait un patron réciproque d'influences corticospinales (PEM supérieurs en position d'extension dans les extenseurs et vice-versa pour les fléchisseurs). Quant à la plupart des sujets post-AVC ayant un niveau clinique élevé de spasticité, la facilitation corticospinale dans les motoneurones des fléchisseurs et extenseurs était supérieure en position de flexion (patron de co-facilitation). Les résultats démontrent que la spasticité est associée à des changements substantiels des influences corticospinales sur les motoneurones des fléchisseurs et des extenseurs du coude. / In post-stroke patients, spasticity, weakness and abnormal coactivation result from limitations in the range of regulation of stretch reflex thresholds. We investigated whether the deficits in residual corticospinal influences contribute to the limitation in the regulation of those thresholds and as a result to spasticity in post-stroke subjects. A single-pulse transcranial magnetic stimulation (TMS) was applied to the site of the motor cortex projecting to motoneurons of elbow flexors and extensors. Responses to TMS (motor evoked potentials or MEPs) were recorded at a flexion and an extension position of the elbow joint. To exclude the influence of background motoneuronal excitability on the evaluation of corticospinal influences, MEPs were elicited during the electromyographic (EMG) silent period produced by brief muscle shortening prior to TMS. In control subjects, corticospinal facilitation of flexor motoneurons was usually larger whereas that of extensor motoneurons was smaller during actively maintained flexion than when the extension position was maintained (reciprocal pattern of position-related changes in flexor and extensor MEPs). In most post-stroke subjects with high clinical spasticity scores, corticospinal facilitation of both flexor and extensor motoneurons was greater at the actively established flexion position (co-facilitation pattern). Results show that spasticity is associated with substantial changes in the corticospinal influences on flexor and extensor motoneurons. Corticospinal co-facilitation of the two groups of motoneurons may be related to the necessity to overcome resistance of spastic muscles during active changes in the elbow joint angle.

The fundamental requirement of the research reported within this thesis is the provision of physical models to enable model based simulation of mainstream printed circuit assembly (PCA) process discrete events for use within to-be-developed (or under development) software tools which codify cause & effects knowledge for use in product and process design optimisation. To support a national competitive advantage in high reliability electronics UK based producers of aircraft electronic subsystems require advanced simulation tools which offer model based guidance. In turn, maximization of manufacturability and minimization of uncontrolled rework must therefore enhance inservice sustainability for 'power-by-the-hour' commercial aircraft operation business models.

Asynchronous message passing systems are fast becoming a common means for communication between devices. Two problems existing in message passing programs are difficult to solve. The first problem, intended or otherwise, is message-race where a receive may match with more than one send in the runtime system. This non-determinism often leads to intermittent and unexpected behavior depending on the resolution of the race. Another problem is deadlock, which is a situation in that each member process of the group is waiting for some member process to communicate with it, but no member is attempting to communicate with it. Detecting if message-race and/or deadlocks exist in a message passing program are both NP-complete. The difficulty of solving the two problems also comes from three factors that complicate the semantics: asynchronous communication, synchronous barrier, and buffering settings including infinite buffering (the system can buffer messages) and zero buffering (the system has no internal buffering). To solve the above problems with complicating factors, this research provides a novel predictive analysis that initializes a concrete execution and then predicts the behavior of other executions that arise from the initial execution. This research starts with Satisfiability Modulo Theories (SMT) based model checking that provides precise analysis for the program behavior. Unfortunately, a precise analysis using SMT does not scale to large programs. As such, the SMT based model checking is combined with heuristic search for witnessing program properties. The heuristic search is efficient in identifying how sends may match with receives in the runtime as it only looks for the match relations for sends and receives in a small searching space initially; the space is increased only if the program property is not witnessed, until all possible match relations for sends and receives reflected in message non-determinism are found. This research also gives a static analysis approach that is scalable as it does not need to analyze the full set of program behaviors; rather, the static analysis only uses polynomial-time algorithms to identify all potential deadlocks in a send-receive templates given a set of pre-defined deadlock patterns. Given the predictive analysis consisting of SMT based model checking with heuristic search and static analysis, this research is able to solve the two problems above. The work in this dissertation also demonstrates that the predictive analysis is more efficient than the existing tools for verifying message passing programs.

Les méthodes formelles pour la conception des software et hardware génèrent souvent des formules qui doivent être validées, de manière interactive ou automatique. Parmi les outils automatiques, les solveurs SMT (Satisfiabilité Modulo Théories) sont particulièrement adaptés à la résolution de ces obligations de preuve, puisque leur langage d'entrée est la logique équationnelle avec des symboles provenant de divers fragments décidables utiles tels que les symboles non interprétés, l'arithmétique linéaire et des structures de données habituelles comme les tableaux ou les listes. Dans cette thèse, nous présentons une approche pour combiner des procédures de décision et des solveurs propositionnels dans un solveur SMT. Cette approche est fondée non seulement sur l'échange d'égalités déductibles entre les procédures de décision, mais aussi sur la génération d'égalités de modèle par des procédures de décision. Cela étend très bien la procédure classique de combinaison due à Nelson-Oppen dans une simple plate-forme pour combiner sans heurts des théories convexes et non convexes. Deuxièmement, nous présentons un algorithme original pour le fragment de l'arithmétique, appelé la logique de différence, et les détails sur la façon de mettre en oeuvre une procédure de décision basée sur cet algorithme. La logique de différence est modélisée en utilisant la théorie des graphes. Les déductions et les vérification de la cohérence effectués par l'algorithme se font par des recherches de cycles négatifs et des calculs de plus courts chemins de manière incrémentale. La dernière partie de la thèse présente une variation incrémentale originale de la méthode du simplexe que nous utilisons pour construire une procédure de décision pour l'arithmétique linéaire. Comme pour la logique de différence, nous présentons les détails de la procédure de décision qui la rend approprié pour notre plate-forme de combinaison utilisée par des solveurs SMT. Les méthodes et les techniques décrites dans cette thèse ont été mises en oeuvre et sont disponibles dans notre solveur SMT open-source, veriT.

<p>The Transport division is responsible for the internal transports on Sandvik Material</p><p>Technology AB. At the moment there is no clear picture of how the straddle carriers are</p><p>moving at the division Primary Products and if it is working in a satisfying way. It is</p><p>important to see the whole picture of the transportation flow so improvements can be made.</p><p>The purpose of this essay is to survey and analyse the truck flow in a Lean Production</p><p>perspective. The essay is delimited to only include straddle carriers transportation ways in the</p><p>Primary Products division. To survey the truck flow we have used a method called Walkthrough.</p><p>This means that we have walked thorough the whole production flow and</p><p>interviewed some of the employed on the way to get the necessary information. We have also</p><p>made an extensive literature study to gather all the necessary theories that is relevant for this</p><p>essay.</p><p>Since 2003 Sandvik Material Technology is running a project called “ledtidsprojektet”, the</p><p>purpose of this project is to create a more efficient production. This project is based on the</p><p>Japanese philosophy Lean Production but is audited to be suitable to Sandviks organisation.</p><p>Today most of the producing divisions within SMT are working according to</p><p>”ledtidsprogrammet”, unfortunately it is not introduced on the Transport division yet.</p><p>The result we got by studying the use of the straddle carriers showed that 40 % where with</p><p>cargo, 35 % without and 25 % where remaining times were breaks are included. The basis of</p><p>the study is from a GPS-transmitter which is placed on one of the straddle carrier. We have</p><p>also made our own study where we followed on the straddle carrier and measured the time for</p><p>the different activities. To get a more statistical secured investigation it is necessary to make a</p><p>more extensive study, when these study where made during a limited time.</p><p>On the basis of the truck flows survey some suggestions for improvements have been</p><p>identified. It has showed that today’s key measurements have to be overlooked to give a fair</p><p>picture of the situation. They also have to improve the way they are planning the transports.</p><p>This can be made by better communication with the producing divisions.</p><p>For the straddle carriers to be more Lean first the producing divisions have to work according</p><p>to the Lean philosophy. It is up to them to try to reduce the stock level and get a more evenly</p><p>production.</p>

The Transport division is responsible for the internal transports on Sandvik Material Technology AB. At the moment there is no clear picture of how the straddle carriers are moving at the division Primary Products and if it is working in a satisfying way. It is important to see the whole picture of the transportation flow so improvements can be made. The purpose of this essay is to survey and analyse the truck flow in a Lean Production perspective. The essay is delimited to only include straddle carriers transportation ways in the Primary Products division. To survey the truck flow we have used a method called Walkthrough. This means that we have walked thorough the whole production flow and interviewed some of the employed on the way to get the necessary information. We have also made an extensive literature study to gather all the necessary theories that is relevant for this essay. Since 2003 Sandvik Material Technology is running a project called “ledtidsprojektet”, the purpose of this project is to create a more efficient production. This project is based on the Japanese philosophy Lean Production but is audited to be suitable to Sandviks organisation. Today most of the producing divisions within SMT are working according to ”ledtidsprogrammet”, unfortunately it is not introduced on the Transport division yet. The result we got by studying the use of the straddle carriers showed that 40 % where with cargo, 35 % without and 25 % where remaining times were breaks are included. The basis of the study is from a GPS-transmitter which is placed on one of the straddle carrier. We have also made our own study where we followed on the straddle carrier and measured the time for the different activities. To get a more statistical secured investigation it is necessary to make a more extensive study, when these study where made during a limited time. On the basis of the truck flows survey some suggestions for improvements have been identified. It has showed that today’s key measurements have to be overlooked to give a fair picture of the situation. They also have to improve the way they are planning the transports. This can be made by better communication with the producing divisions. For the straddle carriers to be more Lean first the producing divisions have to work according to the Lean philosophy. It is up to them to try to reduce the stock level and get a more evenly production.

Simultaneous multithreading (SMT) processors can issue multiple instructions from distinct processes or threads in the same cycle. This technique effectively increases the overall throughput by keeping the pipeline resources more occupied at the potential expense of reducing single thread performance due to resource sharing. In the software domain, an increasing number of Dynamically Linked Libraries (DLL) are used by applications and operating systems, providing better flexibility and modularity, and enabling code sharing. It is observed that a significant amount of execution time in software today is spent in executing standard DLL instructions, that are shared among multiple threads or processes. However, for an SMT processor with a virtually-indexed based cache implementation, existing instruction fetching mechanisms can induce unnecessary false cache misses caused by the DLL-based instructions, which were intended to be shared. This problem is more conspicuous when multiple independent threads are executing concurrently in an SMT processor. This work investigates an often-neglected form of contention between running threads in the I-TLB and I-cache caused by DLLs. To address these shortcomings, we propose a system level technique involving a light-weight modification in the microarchitecture and the OS. By exploiting the nature of the DLLs in our new architecture, we are able to reinstate physical sharing of the DLLs in an SMT machine. Using Microsoft Windows based applications, our simulation results show that the optimized instruction fetching mechanism can reduce the number of DLL misses up to 5.5 times and improve the instruction cache hit rates by up to 62%, resulting in upto 30% DLL IPC improvements and upto 15% overall IPC improvements.