This thesis describes an efficient method for speeding up functional verification of arithmetic circuits namely linear network such as wallace trees, counters using linear algebra techniques. The circuit is represented as a network of half adders, full adders and inverters, and modeled as a system of linear equations. The proof of functional correctness of the design is obtained by computing its algebraic signature using standard linear programming (LP) solver and comparing it with the reference signature provided by the designer. Initial experimental results and comparison with Satisfiability Modulo Theorem (SMT) solvers show that the method is efficient, scalable and applicable to complex arithmetic designs, including large multipliers. It is intended to provide a new front end theory/engine to enhance SMT solvers.

L'analyse statique de programme a pour but de prouver automatiquement qu'un programme vérifie certaines propriétés. L'interprétation abstraite est un cadre théorique permettant de calculer des invariants de programme. Ces invariants sont des propriétés sur les variables du programme vraies pour toute exécution. La précision des invariants calculés dépend de nombreux paramètres, en particulier du domaine abstrait et de l'ordre d'itération utilisés pendant le calcul d'invariants. Dans cette thèse, nous proposons plusieurs extensions de cette méthode qui améliorent la précision de l'analyse.Habituellement, l'interprétation abstraite consiste en un calcul de point fixe d'un opérateur obtenu après convergence d'une séquence ascendante, utilisant un opérateur appelé élargissement. Le point fixe obtenu est alors un invariant. Il est ensuite possible d'améliorer cet invariant via une séquence descendante sans élargissement. Nous proposons une méthode pour améliorer un point fixe après la séquence descendante, en recommençant une nouvelle séquence depuis une valeur initiale choisie judiscieusement. L'interprétation abstraite peut égalementêtre rendue plus précise en distinguant tous les chemins d'exécution du programme, au prix d'une explosion exponentielle de la complexité. Le problème de satisfiabilité modulo théorie (SMT), dont les techniques de résolution ont été grandement améliorée cette décennie, permettent de représenter ces ensembles de chemins implicitement. Nous proposons d'utiliser cette représentation implicite à base de SMT et de les appliquer à des ordres d'itération de l'état de l'art pour obtenir des analyses plus précises.Nous proposons ensuite de coupler SMT et interprétation abstraite au sein de nouveaux algorithmes appelés Modular Path Focusing et Property-Guided Path Focusing, qui calculent des résumés de boucles et de fonctions de façon modulaire, guidés par des traces d'erreur. Notre technique a différents usages: elle permet de montrer qu'un état d'erreur est inatteignable, mais également d'inférer des préconditions aux boucles et aux fonctions.Nous appliquons nos méthodes d'analyse statique à l'estimation du temps d'exécution pire cas (WCET). Dans un premier temps, nous présentons la façon d'exprimer ce problème via optimisation modulo théorie, et pourquoi un encodage naturel du problème en SMT génère des formules trop difficiles pour l'ensemble des solveurs actuels. Nous proposons un moyen simple et efficace de réduire considérablement le temps de calcul des solveurs SMT en ajoutant aux formules certaines propriétés impliquées obtenues par analyse statique. Enfin, nous présentons l'implémentation de Pagai, un nouvel analyseur statique pour LLVM, qui calcule des invariants numériques grâce aux différentes méthodes décrites dans cette thèse. Nous avons comparé les différentes techniques implémentées sur des programmes open-source et des benchmarks utilisés par la communauté. / Static program analysis aims at automatically determining whether a program satisfies some particular properties. For this purpose, abstract interpretation is a framework that enables the computation of invariants, i.e. properties on the variables that always hold for any program execution. The precision of these invariants depends on many parameters, in particular the abstract domain, and the iteration strategy for computing these invariants. In this thesis, we propose several improvements on the abstract interpretation framework that enhance the overall precision of the analysis.Usually, abstract interpretation consists in computing an ascending sequence with widening, which converges towards a fixpoint which is a program invariant; then computing a descending sequence of correct solutions without widening. We describe and experiment with a method to improve a fixpoint after its computation, by starting again a new ascending/descending sequence with a smarter starting value. Abstract interpretation can also be made more precise by distinguishing paths inside loops, at the expense of possibly exponential complexity. Satisfiability modulo theories (SMT), whose efficiency has been considerably improved in the last decade, allows sparse representations of paths and sets of paths. We propose to combine this SMT representation of paths with various state-of-the-art iteration strategies to further improve the overall precision of the analysis.We propose a second coupling between abstract interpretation and SMT in a program verification framework called Modular Path Focusing, that computes function and loop summaries by abstract interpretation in a modular fashion, guided by error paths obtained with SMT. Our framework can be used for various purposes: it can prove the unreachability of certain error program states, but can also synthesize function/loop preconditions for which these error states are unreachable.We then describe an application of static analysis and SMT to the estimation of program worst-case execution time (WCET). We first present how to express WCET as an optimization modulo theory problem, and show that natural encodings into SMT yield formulas intractable for all current production-grade solvers. We propose an efficient way to considerably reduce the computation time of the SMT-solvers by conjoining to the formulas well chosen summaries of program portions obtained by static analysis.We finally describe the design and the implementation of Pagai,a new static analyzer working over the LLVM compiler infrastructure,which computes numerical inductive invariants using the various techniques described in this thesis.Because of the non-monotonicity of the results of abstract interpretation with widening operators, it is difficult to conclude that some abstraction is more precise than another based on theoretical local precision results. We thus conducted extensive comparisons between our new techniques and previous ones, on a variety of open-source packages and benchmarks used in the community.

L’acceptation et l’utilisation des services Web en industrie se développent de par leursupport au développement d’application distribuées comme compositions d’entitéslogicielles plus simples appelées services. En complément à la vérification, le testpermet de vérifier la correction d’une implémentation binaire (code source nondisponible) par rapport à une spécification. Dans cette thèse, nous proposons uneapproche boîte-noire du test de conformité de compositions de services centralisées(orchestrations). Par rapport à l’état de l’art, nous développons une approchesymbolique de façon à éviter des problèmes d’explosion d’espace d’état dus à la largeutilisation de données XML dans les services Web. Cette approche est basée sur desmodèles symboliques (STS), l’exécution symbolique de ces modèles et l’utilisationd’un solveur SMT. De plus, nous proposons une approche de bout en bout, quiva de la spécification à l’aide d’un langage normalisé d’orchestration (ABPEL) etde la possible description d’objectifs de tests à la concrétisation et l’exécution enligne de cas de tests symboliques. Un point important est notre transformation demodèle entre ABPEL et les STS qui prend en compte les spécifications sémantiquesd’ABPEL. L’automatisation de notre approche est supportée par un ensemble d’outilsque nous avons développés. / Web services are gaining industry-wide acceptance and usage by fostering the developmentof distributed applications out of the composition of simpler entities calledservices. In complement to verification, testing allows one to check for the correctnessof a binary (no source code) service implementation with reference to a specification.In this thesis, we propose black box conformance testing approach for centralizedservice compositions (orchestrations). With reference to the state of the art, wedevelop a symbolic approach in order to avoid state space explosion issues due to theXML data being largely used in Web services. This approach is based on symbolicmodels (STS), symbolic execution, and the use of a satisfiability modulo theory(SMT) solver. Further, we propose a comprehensive end-to-end approach that goesfrom specification using a standard orchestration language (ABPEL), and the possibledescription of test purposes, to the online realization and execution of symbolic testcases against an implementation. A crucial point is a model transformation fromABPEL to STS that we have defined and that takes into account the peculiarities ofABPEL semantics. The automation of our approach is supported by a tool-chainthat we have developed.

Les travaux présentés dans cette thèse proposent une méthode de génération automatique de tests à partir de modèles.Cette méthode emploie deux langages de modélisations UML4MBT et OCL4MBT qui ont été spécifiquement dérivées d’ UML et OCL pour la génération de tests. Ainsi les comportements, la structure et l’état initial du système sont décrits au travers des diagrammes de classes, d’objets et d’états-transitions.Pour générer des tests, l’évolution du modèle est représente sous la forme d’un système de transitions. Ainsi la construction de tests est équivalente à la découverte de séquences de transitions qui relient l’´état initial du système à des états validant les cibles de test.Ces séquences sont obtenues par la résolution de scénarios d’animations par des prouveurs SMT et solveurs CSP. Pour créer ces scénarios, des méta-modèles UML4MBT et CSP4MBT regroupant formules logiques et notions liées aux tests ont été établies pour chacun des outils.Afin d’optimiser les temps de générations, des stratégies ont été développé pour sélectionner et hiérarchiser les scénarios à résoudre. Ces stratégies s’appuient sur la parallélisation, les propriétés des solveurs et des prouveurs et les caractéristiques de nos encodages pour optimiser les performances. 5 stratégies emploient uniquement un prouveur et 2 stratégies reposent sur une collaboration du prouveur avec un solveur.Finalement l’intérêt de cette nouvelle méthode à été validée sur des cas d’études grâce à l’implémentation réalisée. / This thesis describes an automatic test generation process from models.This process uses two modelling languages, UML4MBT and OCL4MBT, created specificallyfor tests generation. Theses languages are derived from UML and OCL. Therefore the behaviours,the structure and the initial state of the system are described by the class diagram, the objectdiagram and the state-chart.To generate tests, the evolution of the model is encoded with a transition system. Consequently,to construct a test is to find transition sequences that rely the initial state of the system to thestates described by the test targets.The sequence are obtained by the resolution of animation scenarios. This resolution is executedby SMT provers and CSP solvers. To create the scenario, two dedicated meta-models, UML4MBTand CSP4MBT have been established. Theses meta-models associate first order logic formulas withthe test notions.7 strategies have been developed to improve the tests generation time. A strategy is responsiblefor the selection and the prioritization of the scenarios. A strategy is built upon the properties ofthe solvers and provers and the specification of our encoding process. Moreover the process canalso be paralleled to get better performance. 5 strategies employ only a prover and 2 make theprover collaborate with a solver.Finally the interest of this process has been evaluated through a list of benchmark on variouscases studies.

La nano-organisation de la membrane cellulaire est essentielle à la régulation de certaines fonctions cellulaires. Dans cette thèse, les récepteurs EGF, CPεT et de la transferrine ont été marqués avec des nanoparticules luminescentes et ont été suivis à la fois dans leur environnement local dans la membrane cellulaire vivantes pour de longues durées et sous un flux hydrodynamique. Nous avons alors appliqué des techniques d'inférence bayésienne, d’arbre de décision et de clustering de données extraire des informations quantitatives sur les paramètres caractéristiques du mouvement des récepteurs, notamment la forme de leur confinement dans des microdomaines. L’application d’une force hydrodynamique sur les nanoparticules nous a alors permis de sonder les interactions auxquelles ces récepteurs sont soumis. Nous avons appliqué cette approche in vitro pour favoriser et mesurer la dissociation in vitro de paires récepteur / ligand à haute affinité entre des récepteurs membranaires et leurs ligands pharmaceutiques, telles que HB-EGF et DTR et l’avons ensuite appliqué à l’étude d’interactions à la membrane cellulaire. Nous avons ainsi mis en évidence trois modes différents d'organisation de la membrane et de confinement des récepteurs: le confinement de CPεTR est déterminé par l'interaction entre les récepteurs et les constituants lipidiques / protéiques des microdomaines, le potentiel de confinement de l'EGFR résulte de l'interaction avec les lipides et les protéines de l’environnement du radeau et de l’interaction avec la F-actine; les récepteurs de la transferrine diffusent librement dans la membrane, uniquement limités stériquement par des barrières d’actine, selon le modèle ‘picket-and-fence’. Nous avons de plus montré que les nanodomaines de type radeau sont rattachés au cytoskelette d’actine. Ce travail présente donc à la fois un aperçu quantitatif du récepteur membranaire, des mécanismes d’organisation à l’échelle nanométrique, et établit un cadre méthodologique avec lequel différents types de propriétés membranaires peuvent être étudiés. / In this thesis, EGF, CPεT and transferrin receptors were labeled with luminescent nanoparticles, , and were tracked both in their local environment in the cell membrane and under a hydrodynamic flow. Bayesian inference, Bayesian decision tree, and data clustering techniques can then be applied to obtain quantitative information on the receptor motion parameters. Furthermore, we introduced hydrodynamic force application in vitro to study biomolecule dissociation between membrane receptors and their pharmaceutical ligands in high affinity receptor- ligand pairs, such as HB-EGF and DTR. Finally, three different modes of membrane organization and receptor confinement were revealed: the confinement of CPεTR is determined by the interaction between the receptors and the lipid/protein constituents of the raft; the confining potential of EGFR results from the interaction with lipids and proteins of the raft environment and from the interaction with F-actin; transferrin receptors diffuse freely in the membrane, only sterically limited by actin barriers, according to the “picket-and-fence” model. We moreover showed that all raft nanodomains are attached to the actin cytoskeleton.

Today’s Web Public Key Infrastructure (PKI) builds on a homogeneous trust model. All Certificate Authorities (CAs) are equally trusted once they are marked as trusted CAs on the client side. As a result, the security of the Web PKI depends on the weakest CA. Trust heterogeneity and flexibility can be introduced in today’s Web PKI to mitigate the problem. Each client could have different levels of trust in each trusted CA, according to the properties of each CA, such as the location, reputation and scale of the CA. As a result, the loss caused by the compromise of a less trusted CA will be relieved. In this work, we study Flexible-PKI (F-PKI), which is an enhancement of Web PKI, and propose Lite Flexible-PKI (LF-PKI) to address the limitations of F-PKI. LF-PKI is designed to securely and efficiently manage domain policies and enable trust heterogeneity on the client side. The domain owner can issue domain policies for their domains, and the client will have a complete view of the domain policies issued for a specific domain. Based on the collection of domain policies from LF-PKI, trust heterogeneity can be achieved on the client side. Each client will choose the domain policies based on the trust levels of the CA. On the basis of the LF-PKI design, a high-performance implementation of LF-PKI was developed, optimized, and analyzed. The optimized implementation can provide the LF-PKI services for worldwide domains on a single server with moderate hardware. / Dagens Web Public Key Infrastructure (PKI) bygger på en homogen förtroendemodell. Alla certifikatutfärdare (CA) är lika betrodda när de är markerade som betrodda certifikatutfärdare på klientsidan. Som ett resultat beror säkerheten för webb-PKI på den svagaste CA. Förtroendeheterogenitet och flexibilitet kan införas i dagens webb-PKI för att mildra problemet. Varje klient kan ha olika nivåer av förtroende för varje betrodd certifikatutfärdare, beroende på egenskaperna hos varje certifikatutfärdare, såsom certifikatutfärdarens plats, rykte och omfattning. Som ett resultat kommer förlusten som orsakats av kompromissen av en mindre pålitlig CA att avhjälpas. I detta arbete studerar vi Flexible-PKI (F-PKI), som är en förbättring av webb-PKI, och föreslår Lite Flexible-PKI (LF-PKI) för att ta itu med begränsningarna hos F-PKI. LF-PKI är utformad för att säkert och effektivt hantera domänpolicyer och möjliggöra förtroendeheterogenitet på klientsidan. Domänägaren kan utfärda domänpolicyer för sina domäner, och klienten kommer att ha en fullständig bild av domänpolicyerna som utfärdats för en specifik domän. Baserat på insamlingen av domänpolicyer från LF-PKI kan förtroendeheterogenitet uppnås på klientsidan. Varje klient kommer att välja domänpolicyer baserat på förtroendenivåerna för CA. På basis av LF-PKI-designen utvecklades, optimerades och analyserades en högpresterande implementering av LF-PKI. Den optimerade implementeringen kan tillhandahålla LF-PKI-tjänster för världsomspännande domäner på en enda server med måttlig hårdvara.

Examensarbetet utfördes under våren 2021 på ett svenskt företag i Centrala Sverige. Uppdraget har som syfte haft att få en objektiv inblick i företagets lagersituation för försäljningen i EMEA. Uppdragets mål var att undersöka vart kostnadsbesparingar kunde göras, hur koldioxidutsläpp kunde reduceras för transporter av SMT produkter och hur servicenivån till kunderna kunde öka med att korta ned interna och externa ledtider. För att möjliggöra dessa kriterier undersöktes den befintliga lagersituationen mot en omställning för att komma närmare kunderna i EMEA. Med syfte att minska på transportdistanserna från lager till kund och från produktion till lager. För att möjliggöra arbete har information givits av företaget där ansvariga personer för respektive avdelning och en förstudie om vart ett lager bör placeras. Förstudien har jämförts mot den interna datainsamlingen. Interndatasamlingen har bestått av intervjuer och analyser utav tidigare arbeten i form av säljvolym och kundlokalisation granskats för att få en inblick i hur materialet flödar vid försäljning i EMEA. Logistiken för nuläget har gett en djupare förståelse i hur problemet uppstått och varför förbättringar önskats. När slut produktionen ligger närmare slutkunden än vad det befintliga central lagret gör i dagensläge antas att förbättringar kan göras. Med en granskning av företagets transportkostnader, lagerkostnader och distansen till samtliga kunder har resultatet visat på att vinningar kan göras på samtliga punkter. / This thesis project was carried out in the spring of 2021 at a Swedish owned company located in central Sweden. The purpose of the assignment was to gain an objective insight into the company’s stock situation for sales in EMEA. Then to investigate where cost savings could be made, how carbon dioxide emissions could be reduced for transport of SMT, and finally how the level of service to customers could increase by shorting internal and external lead times. To enable these criteria, the existing stock situation was examined towards a changeover to get closer to the customers in EMEA. Thus aiming to reduce the transport distance from warehouse to customer and from production to warehouse. To enable this project, information has been provided by the people responsible for each department and a feasibility study was carried out on where the warehouse should be located. The feasibility study has been compared with the internal data collection. This collection has consisted of interviews and analyzes of previous work in the form of sales volume. Customer locations has also been examined to get an insight into how the material flows during sales in EMEA. The logistics for the current situation provide a deeper understanding of how the problem arose and why improvements were needed. When the finishing production is closer to the customers of the company than what the existing warehouse does in the current situation, it is assumed that improvements can be made. With a careful examination of the company’s transport costs, warehouse costs and the distance to all customers in EMEA, the results have shown that gains can be made on all points.

The main aim of this study was to investigate the role of school management in promoting healthy school environments for Grade R learners in the Sedibeng West District. A literature review revealed that there are two types of health programmes: those that support the curriculum and those that are part of the curriculum. School managers have to focus on both in their efforts to promote health in schools. South African schools adapted a Whole School Approach in creating and sustaining healthy environments. Whole School Approach includes the development of health policies, health education, community, learner, teacher involvement, nutrition and prevention of communicable diseases. A qualitative research approach was used and data was generated by means of interviews, documents, photographs and narratives. Four research sites were purposefully selected and four principals, three Heads of Departments for Foundation Phase, four health coordinators and four Grade R practitioners participated in this research. Only one of the research sites had a School Based Health Centre. The study revealed that curriculum-based health programmes including physical education, physical activities and health education were effectively implemented although they were not effectively monitored and evaluated. Health programmes supporting the curriculum include nutrition, first aid and health services. Both health services and nutrition were effectively implemented and monitored whilst there were serious problems with first aid. Practitioners were not trained for first aid, in the three schools where first aid kits were available were not checked therefore not replenished. In one school there was no first aid kit, thus, there was not much focus on precautionary measures in the participating school. There was therefore, no strategies in place for the management of health programmes that support the curriculum. / MEd (Education Management), North-West University, Vaal Triangle Campus, 2014

The main aim of this study was to investigate the role of school management in promoting healthy school environments for Grade R learners in the Sedibeng West District. A literature review revealed that there are two types of health programmes: those that support the curriculum and those that are part of the curriculum. School managers have to focus on both in their efforts to promote health in schools. South African schools adapted a Whole School Approach in creating and sustaining healthy environments. Whole School Approach includes the development of health policies, health education, community, learner, teacher involvement, nutrition and prevention of communicable diseases. A qualitative research approach was used and data was generated by means of interviews, documents, photographs and narratives. Four research sites were purposefully selected and four principals, three Heads of Departments for Foundation Phase, four health coordinators and four Grade R practitioners participated in this research. Only one of the research sites had a School Based Health Centre. The study revealed that curriculum-based health programmes including physical education, physical activities and health education were effectively implemented although they were not effectively monitored and evaluated. Health programmes supporting the curriculum include nutrition, first aid and health services. Both health services and nutrition were effectively implemented and monitored whilst there were serious problems with first aid. Practitioners were not trained for first aid, in the three schools where first aid kits were available were not checked therefore not replenished. In one school there was no first aid kit, thus, there was not much focus on precautionary measures in the participating school. There was therefore, no strategies in place for the management of health programmes that support the curriculum. / MEd (Education Management), North-West University, Vaal Triangle Campus, 2014

Sabemos que em placas de circuito impresso montadas com tecnologia SMD Surface Mount Device podem ocorrer problemas com a migração eletroquímica. O fenômeno aparece principalmente porque os novos encapsulamentos possuem terminais com espaçamentos muito próximos. A migração eletroquímica pode tornar-se um potencial problema no processo de soldagem eletrônica quando é utilizado a tecnologia Lead Free na montagem das placas. O processo de migração eletroquímica ocorre quando temos metal, isolante e metal, em ambiente de alta umidade e sobre polarização elétrica, o metal deixa a posição inicial em forma de íon e se redeposita sobre o isolante. Em uma placa de circuito impresso, dois terminais adjacentes podem tornar-se eletrodos, dessa forma as dendritas crescem do cátodo para o ânodo. Podem aparecer diferentes morfologias com diferentes elementos envolvidos no processo de migração, dependendo da composição da pasta de solda ou acabamento da placa de circuito impresso. Uma estrutura do tipo pente comb feita sobre laminado FR4 foi utilizada nos experimentos. A distância entre as trilhas foram de 102 e 254 mícrons para simular uma distancia real dos terminais dos dispositivos. Os fatores considerados durante os experimentos foram: A distancia entre os terminais na estrutura (102 ou 254 mícrons), tensão aplicada (2 ou 3 V). Foi observado que a pasta de solda e o acabamento final não influenciam no processo de migração eletroquímica. O Estanho foi o principal metal que migrou. Todos os resultados obtidos nesse estudo concordam com a literatura. / It is well known that in printed circuits boards assembled by SMT technology may occur Electrochemical migration (ECM). This phenomenon appears mainly because the new packaging has the terminals very close. Also the Electrochemical migration may become a potential reliability problem in electronic soldering when lead free technology is used in soldering electronic devices. Electrochemical migration is an electrochemical process where metal on an insulating material, in a humid environment and under an applied electric field, leaves its initial location in ionic form and redeposit. In a PCB two adjacents terminal may behave as electrodes so the dendrites grow from cathode to anode. It can show different morphologies with the different migration elements involved depending on the solder paste composition or PCB surface finishing. A structure with a comb shape printed on FR4 substrate was used in the experiments. The distance between the fingers in the structure was 102 or 254 microns, in order to simulate a real distance between dispositive terminals. The factors considered during the experiments were surface finishing (ENIG or HASL), solder paste composition, distance between terminals (102 or 254 microns) and applied voltage (2 or 3 V). It was observed that the solder paste and the surface finishing dont influence the ECM process. Tin was the main metal that migrates. All the results obtained in these study agrees with the literature.