Le développement de circuits électroniques et de systèmes logiciels critiques pour le ferroviaire ou l’avionique, par exemple, demande à être systématiquement associé à un processus de vérification formelle permettant de garantir l’exhaustivité des tests. L’approche formelle la plus répandue dans l’industrie est le Model Checking. Le succès de son adoption provient de deux caractéristiques : (i) son aspect automatique, (ii) sa capacité à produire un témoin (un scénario rejouable) lorsqu’un comportement indésirable est détecté, ce qui fournit une grande aide aux concepteurs pour corriger le problème. Néanmoins, la complexité grandissante des systèmes à vérifier est un réel défi pour le passage à l’échelle des techniques existantes. Pour y remédier, différents algorithmes de model checking (e.g., parcours symbolique des états du système, interpolation), diverses méthodes complémentaires (e.g., abstraction,génération automatique d’invariants), et de multiples procédures de décision(e.g., diagramme de décision, solveur SMT) sont envisageables.Dans cette thèse, nous nous intéressons plus particulièrement à l’induction temporelle.Il s’agit d’un algorithme de model checking très utilisé dans l’industrie pour vérifier les systèmes critiques. C’est également l’algorithme principal de l’outil développé au sein de l’entreprise Safe River, entreprise dans laquelle cette thèse a été effectuée. Plus précisément, l’induction temporelle combine deux techniques :(i) BMC (Bounded Model Checking), une méthode très efficace pour la détection debugs dans un système (ii) k-induction, une méthode ajoutant un critère de terminaison à BMC lorsque le système n’admet pas de bug. Ces deux techniques génèrent des formules logiques propositionnelles pour lesquelles il faut en déterminer la satisfaisabilité.Pour se faire, nous utilisons un solveur SAT, c’est-à-dire une procédure de décision qui détermine si une telle formule admet une solution.L’originalité des travaux proposés dans cette thèse repose en grande partie sur la volonté de renforcer la collaboration entre le solveur SAT et le model checker.Nos efforts visent à accroître l’interconnexion de ces deux modules en exploitant la structure haut niveau du problème. Nous avons alors défini des méthodes profitant de la structure symétrique des formules. Cette structure apparaît lors du dépliage successif de la relation de transition, et nous permet de dupliquer les clauses ou encore de déplier les transitions dans différentes directions (i.e., avant ou arrière). Nous avons aussi pu instaurer une communication entre le solveur SAT et le model checker permettant de : (i) simplifier la représentation au niveau du model checker grâce à des informations déduites par le solveur, et (ii) aider le solveur lors de la résolution grâce aux simplifications effectuées sur la représentation haut niveau. Une autre contribution importante de cette thèse est l’expérimentation des algorithmes proposées. Cela se concrétise par l’implémentation d’un model checker prenant en entrée des modèles AIG (And-Inverter Graph) dans lequel nous avons pu évaluer l’efficacité de nos différentes méthodes. / The design of electronic circuits and safety-critical software systems in railway or avionic domains for instance, is usually associated with a formal verification process. More precisely, test methods for which it is hard to show completeness are combined with approaches that are complete by definition. Model Checking is one of those approaches and is probably the most prevalent in industry. Reasons of its success are mainly due to two characteristics, namely: (i) its fully automatic aspect, and (ii) its ability to produce a short execution trace of undesired behaviors, which is very helpful for designers to fix the issues. However, the increasing complexity of systems to be verified is a real challenge for the scalability of existing techniques. To tackle this challenge, different model checking algorithms (e.g., symbolic model checking, interpolation), various complementary methods (e.g., abstraction, automatic generation of invariants) and multiple decision procedures (e.g., decision diagram, SMT solver) can be considered. In this thesis, we particularly focus on temporal induction. It is a model checking algorithm widely used in the industry to check safety-critical systems. This is also the core algorithm of the tool developed within SafeRiver, company in which this thesis was carried out. More precisely, temporal induction consists of a combination of BMC (Bounded Model Checking) and k-induction. BMC is a very efficient bugfinding method. While k-induction adds a termination criterion to BMC when the system does not admit bugs. These two techniques generate formulas for which it is necessary to determine their satisfiability. To this end, we use a SAT solver as a decision procedure to determine whether a propositional formula has a solution. The main contribution of this thesis aims to strengthen the collaboration between the SAT solver and the model checker. The improvements proposed mainly focus on increasing the interconnections of these two modules by exploiting the high-level structure of the problem.We have therefore defined several methods taking advantage of the symmetrical structure of the formulas. This structure emerges during the successive unfolding of the transition relation, and allows us to duplicate clauses or even unroll the transitions in different directions (i.e., forward or backward). We also established a communication between the solver and the model checker, which has for purpose to: (i) simplify the model checker representation using the information inferred by the solver, and (ii) assist the solver during resolution with simplifications performed on the high-level representation. Another important contribution of this thesis is the empirical evaluation of the proposed algorithms on well-established benchmarks. This is achieved concretely via the implementation of a model checker taking AIG (And-Inverter Graph) as input, from which we were able to evaluate the effectiveness of our algorithms.

The goal of this thesis is creation of methodology for repeatable transformation of customer business needs and goals resulting from company IT strategy to system functionality and process implementation in Business/IT Service Management projects using BMC Atrium and Remedy products. This methodology will be based on existing project management methodologies PRINCE2 and SCRUM. In the thesis I also refer to parts of ITIL v3 process framework. The aim of the thesis is to provide a project delivery framework for IT Consultancy organizations. The framework will foster efficient planning, tracking and communication of requirements and deliverables between IT Consultancy and their customer during entire project lifecycle and will therefore enable repeatable and consistent high quality delivery of customer success.

Since its introduction in 1999, bounded model checking (BMC) has quickly become a serious and indispensable tool for the formal verification of hardware designs and, more recently, software. By leveraging propositional satisfiability (SAT) solvers, BMC overcomes some of the shortcomings of more conventional model checking methods. In model checking we automatically verify whether a state transition system (STS) describing a design has some property, commonly expressed in linear temporal logic (LTL). BMC is the restriction to only checking the looping and non-looping runs of the system that have bounded descriptions. The conventional BMC approach is to translate the STS runs and LTL formulae into propositional logic and then conjunctive normal form (CNF). This CNF expression is then checked by a SAT solver. In this thesis we study the effect on the performance of BMC of changing the translation to propositional logic. One novelty is to use a normal form for LTL which originates in resolution theorem provers. We introduce the normal form conversion early on in the encoding process and examine the simplifications that it brings to the generation of propositional logic. We further enhance the encoding by specialising the normal form to take advantage of the types of runs peculiar to BMC. We also improve the conversion from propositional logic to CNF. We investigate the behaviour of the new encodings by a series of detailed experimental comparisons using both hand-crafted and industrial benchmarks from a variety of sources. These reveal that the new normal form based encodings can reduce the solving time by a half in most cases, and up to an order of magnitude in some cases, the size of the improvement corresponding to the complexity of the LTL expression. We also compare our method to the popular automata-based methods for model checking and BMC.

The diploma thesis presents the usability of a new thermosetting material BMC for the construction of a car headlight. In the theoretical part there are described headlights, basic characteristics and properties of plastics focussing on polymer composite materials and material testing. The practical part deals with the processing of test samples for mechanical testing by compression moulding and also with the production of real samples of reflectors and carrier frames by injection moulding. The evaluation is based on comparison of the results of the performed tests of alternative material and the currently used BMC TETRADUR TD 492/2 in HELLA Autotechnik Nova s.r.o. Basic physical-mechanical properties such as strength, stiffness, toughness and hardness are tested and monitored. The reflectors and carrier frames are assembled into the headlight and then tested according to legal and customers´ requirements for climate and vibration resistance and photometry.

In den letzten Jahren haben regenerative Therapieansätze zur Behandlung der chronischen Herzinsuffizienz mit Einsatz adulter Stammzellen größere Aufmerksamkeit erfahren. Zahlreiche klinische Studien an Patienten mit ischämischer Kardiomyopathie zeigten erfolgversprechende Ergebnisse mit der Transplantation autologer Knochenmarkstammzellen (BMC). Es existieren Hinweise, dass BMC Connexin43 exprimieren könnten. In der hier vorgelegten Arbeit erfolgte in einem Ischämie-Reperfusions-Modell am autonom schlagenden Langendorff-Herzen nach passagerer Ligatur einer Koronarie mit Induktion einer Myokardischämie eine unselektive transkoronare Injektion autologer BMC in der frühen Reperfusionsphase. Zu überprüfen war die Hypothese, dass BMC in dieser Phase der Reperfusion sicher administriert werden können und bereits ein ischämiegetriggertes Homing im Infarktareal zeigen. Zudem sollte überprüft werden, ob c-kit+ (CD117) BMC in der Lage sind Connexin43 zu exprimieren. Additiv wurde am Beispiel von NF-κB postuliert, dass auch die Aktivierung früher Gene einen Einfluss auf das Homing von c-kit+ BMC haben. Die Applikation einer großen Zellzahl (durchschnittlich 1,8 Mio. /g Myokard) mit Infusionsraten von 0,5 - 2,6 Mio. Zellen pro Minute hatte hierbei keinen negativen Einfluss auf Hämodynamik und rhythmogene Stabilität. Akute Myokardischämien traten nicht auf. Der gewählte Applikationsweg und -zeitpunkt führten zu einer quantitativ adäquaten Zellretention. Immunhistologisch ließen sich die Tendenz zum 'Homing' von c-kit+ BMC im ischämischen linksventrikulären Myokard sowie Zeichen der ischämiegetriggerten Extravasation nachweisen. Eine signifikante Expression von Connexin43 an c-kit+ BMC konnte nicht gezeigt werden. Somit kann eine gap-junction-vermittelte Kommunikation zwischen c-kit+ BMC zu diesem Zeitpunkt nicht bestätigt werden. Im direkten Umfeld c-kit+ BMC fand sich keine vermehrte Aktivierung von NF-κB.

Aim. Bone changes in size and density in response to different levels of stress. Alterations to bone mineral density (BMD) appear to occur in a site specific manner. Even though BMD has been examined in many populations there is a paucity of data looking at strength-power athletes, such as throwers. Therefore, the purpose of this study was to examine the BMD of a group of USA Division I collegiate throwers (e.g. shot put, discus, etc.). Methods. Seven throwers (4 males; 3 females) who were 19.0 ± 0.9 years had their BMD compared to an age matched control group (n=14; 8 women and 6 men) and normative data. BMD was measured with dual X-ray absorptometry. Potential right/left side and sex difference in BMD were also examined. Maximal isometric strength was assessed using a mid-thigh pull while standing on a forceplate which generated force-time curves. Peak force (PF) and normalized peak force (PFa) were then correlated with BMDs. Results. Generally, throwers had denser bones with male throwers tending to have a greater total BMD (Ps<0.05). The dominant arm BMD was slightly greater when compared to non-dominant arm (P≤0.05). Furthermore, total body BMD was related to PF (r=0.68, r2 =0.46) and PFa (r=0.56, r2=0.31). Conlcusion. Throwers have greater BMDs than non-athletes and most other athletes. However, throwers only showed a small indication of sidedness. It is likely that the BMDs observed in this study stem from the training intervention (e.g. whole body heavy lifting) undertaken by this population.

Indiana University-Purdue University Indianapolis (IUPUI) / Bronze is a popular metal for many important uses. Currently, there are no economical 3D printers that can print Bronze powders. A recent product, Bronze Metal Clay (BMC) has arrived. Additionally, commercial metal 3D printers require laser or electron beam sources, which are expensive and not easily accessible. The objective of this research is to develop a new two-step processing technique to produce 3D printed metallic component. The processing step includes room temperature 3D printing followed by high-temperature sintering. Since no material data exists for this clay, the tensile strength and hardness properties of BMC are compared to wrought counterpart. In this research tests are completed to determine the mechanical properties of Cu89Sn11 Bronze Metal Clay. The author of this thesis compares the physical properties of the same material in two different formats: 3D printed clay and molded clay. Using measured stress-strain curves and derived mechanical properties, including Young's modulus, yield strength, and ultimate tensile strength, the two formats demonstrate inherit differences. The Ultimate tensile strength for molded BMC and 3D-printed specimens sintered at 960 C was 161.94 MPa and 157 MPa, respectively. A 3D printed specimen which was red at 843 C had 104.32 MPa tensile strength. Factory acquired C90700 specimen had an ultimate stress of 209.29 MPa. The Young's modulus for molded BMC and 3D-printed specimens sintered at 960 C was 36.41 GPa and 37.05 GPa, respectively. The 843 C 3D-printed specimen had a modulus of 22.12 GPa. C90700 had the highest modulus of 76.81 GPa. The Yield stress values for molded BMC and 3D-printed specimens sintered at 960 C was 77.81 MPa and 72.82 MPa, respectively. The 3D-printed specimen had 46.44 MPa. C90700 specimen had 115.21 MPa. Hand molded specimens had a Rockwell hardness HRB85, while printed samples had a mean of HRB69. Also, molded samples recorded a higher Young's Modulus of 43 GPa vs. 33 GPa for the printed specimens. Both samples were weaker than the wrought Cu88:8Sn11P0:2 which had a 72 GPa. Cu88:8Sn11P0:2 also was a harder material with an HRC45. The property di erence between 3D printed, molded, and wrought samples was explained by examining their micro structures. It shows that 3D printed sample had more pores than the molded one due to printing process. This study demonstrates the flexibility and feasibility of using 3D printing to produce metallic components, without laser or electron beam source.

År 2022 genomfördes en plockanalys på Biomedicinskt centrum, BMC, i Uppsala för att bland annat studera mängd och sorts plast som behandlas vid källsortering. Fastighetsägaren Akademiska Hus har som övergripande mål att nå klimatneutralitet år 2035 och arbetar mot detta med andra lokala aktörer i fokusgruppen Jakten på plasten. Fokusgruppen är ett forum där olika aktörer kan mötas för att öka uppmärksamhet kring källsortering och återvinning. Plockanalysen visade att det finns möjlighet till förbättring kring återvinningen av plast. Denna rapport ämnar studera hur källsorteringssystemet ser ut idag och vilka orsaker som ligger till grund för att plast sorteras ut felaktigt. I slutsatserna från plockanalysen lyftes frigolit fram som särskilt problematisk. Den skickas enligt instruktion som restavfall, vilket beror på frigolitens skrymmande egenskaper och bristande möjligheter till liknande komprimering som övrigt plastavfall. I containern för restavfall finns en komprimator som lämpar sig bättre för frigolit. I rapporten har extra fokus lagts på just frigoliten och alternativa lösningar till återvinning har studerats utifrån deras klimatnytta.  I en enkätundersökning framkom det att medarbetare på BMC i hög utsträckning tycker att källsortering av plast är viktigt men att det inte alltid är tydligt hur plasten ska sorteras ut. Både när det kommer till riktlinjer från BMC men också utifrån osäkerhet kring vilken typ av plast det är och därav hur den ska sorteras. Förslag på lösningar till detta är att öka informationen genom att se till att all information finns tillgänglig på både svenska och engelska och grundligare information skulle kunna finnas att tillgå via exempelvis en QR-kod på sopkärlen. Om man vill förnya det visuella systemet kring återvinning skulle loggorna kunna uppdateras utifrån ett standardiserat nordiskt system som Avfall Sverige varit med att ta fram. Om frigolit skickas till materialåtervinning istället för energiåtervinning skulle klimatnyttan bli cirka 400 kg koldioxidekvivalenter per år. Transporten har en relativt liten inverkan på klimatnyttan medan återvinningen av frigoliten spelar större roll. Därför kan det finnas intresse av att skicka frigolit till materialåtervinning, även om detta inte kan göras lokalt likt energiåtervinning. Kostnader för de olika alternativen har ej jämförts men en komprimeringsmaskin skulle kunna minska frigolitens volym med upp till en faktor 50. En sådan maskin skulle troligtvis kosta mer jämfört med att, som nu, sortera ut frigoliten i restavfall. Med alternativet att komprimera frigolit skulle transportutgifter kunna minskas.  Som framtida steg skulle djupare samarbeten mellan producenter, användare och återvinnare kunna utvecklas för att hitta lösningar som fungerar för samtliga aktörer i kedjan. Jakten på plasten lämpar sig för detta där Akademiska Hus kan knyta band till andra företag med liknande behov för att tillsammans hitta kostnadseffektiva lösningar på exempelvis uppsamling och transport av frigolit för att öka attraktiviteten kring materialåtervinning jämfört med energiåtervinning.

Many Chinese students seek an international education and they are often a target for international universities. These universities utilize online platforms for advertising to reach students. Various domestic and international intermediaries join to facilitate this online informing as well. On the market combined of the universities and the intermediaries, the online education search service is one of the most popular witnesses. The purpose of this thesis is to investigate the gap between Chinese students and the existing market, and to express how international online education search services should best approach the market. Key value propositions will also be formulated to detail these international services. The research method in this thesis is qualitative, and based on a case study of an international company in Sweden. This company is active in the online education search service and interested in the Chinese market. The case study comprises a pilot launch in China, as well as qualitative semi-structured interviews with employees within the company and with sample students in China. Two additional expert interviews have been conducted external to the case company, in order to increase the reliability of the study. The analysis of this empirical material in conjunction with the literature leads to my conclusion that Chinese students favor complete resources and integrated information, as well as a combination of online and offline practices. Furthermore, the Business Model Canvas is utilized as a theoretical foundation for investigating relevant elements of the value propositions. Finally, I propose a model of approach in both theoretical and practical formats to guide how international online education search services should approach the Chinese market.

With the advances in VLSI and System-On-Chip (SOC) technology, the complexity of hardware systems has increased manifold. Today, 70% of the design cost is spent in verifying these intricate systems. The two most widely used formal methods for design verification are Equivalence Checking and Model Checking. Equivalence Checking requires that the implementation circuit should be exactly equivalent to the specification circuit (golden model). In other words, for each possible input pattern, the implementation circuit should yield the same outputs as the specification circuit. Model checking, on the other hand, checks to see if the design holds certain properties, which in turn are indispensable for the proper functionality of the design. Complexities in both Equivalence Checking and Model Checking are exponential to the circuit size. In this thesis, we firstly propose a novel technique to improve SAT-based Combinational Equivalence Checking (CEC) and Bounded Model Checking (BMC). The idea is to perform a low-cost preprocessing that will statically induce global signal relationships into the original CNF formula of the circuit under verification and hence reduce the complexity of the SAT instance. This efficient and effective preprocessing quickly builds up the implication graph for the circuit under verification, yielding a large set of logic implications composed of direct, indirect and extended backward implications. These two-node implications (spanning time-frame boundaries) are converted into two-literal clauses, and added to the original CNF database. The added clauses constrain the search space of the SAT-solver engine, and provide correlation among the different variables, which enhances the Boolean Constraint Propagation (BCP). Experimental results on large and difficult ISCAS'85, ISCAS'89 (full scan) and ITC'99 (full scan) CEC instances and ISCAS'89 BMC instances show that our approach is independent of the state-of-the-art SAT-solver used, and that the added clauses help to achieve more than an order of magnitude speedup over the conventional approach. Also, comparison with Hyper-Resolution [Bacchus 03] suggests that our technique is much more powerful, yielding non-trivial clauses that significantly simplify the SAT instance complexity. Secondly, we propose a novel global learning technique that helps to identify highly non-trivial relationships among signals in the circuit netlist, thereby boosting the power of the existing implication engine. We call this new class of implications as 'extended forward implications', and show its effectiveness through additional untestable faults they help to identify. Thirdly, we propose a suite of lemmas and theorems to formalize global learning. We show through implementation that these theorems help to significantly simplify a generic CNF formula (from Formal Verification, Artificial Intelligence etc.) by identifying the necessary assignments, equivalent signals, complementary signals and other non-trivial implication relationships among its variables. We further illustrate through experimental results that the CNF formula simplification obtained using our tool outshines the simplification obtained using other preprocessors. / Master of Science