MINING AND VERIFICATION OF TEMPORAL EVENTS WITH APPLICATIONS IN COMPUTER MICRO-ARCHITECTURE RESEARCH

Computer simulation programs are essential tools for scientists and engineers to understand a particular system of interest. As expected, the complexity of the software increases with the depth of the model used. In addition to the exigent demands of software engineering, verification of simulation programs is especially challenging because the models represented are complex and ridden with unknowns that will be discovered by developers in an iterative process. To manage such complexity, advanced verification techniques for continually matching the intended model to the implemented model are necessary. Therefore, the main goal of this research work is to design a useful verification and validation framework that is able to identify model representation errors and is applicable to generic simulators. The framework that was developed and implemented consists of two parts. The first part is First-Order Logic Constraint Specification Language (FOLCSL) that enables users to specify the invariants of a model under consideration. From the first-order logic specification, the FOLCSL translator automatically synthesizes a verification program that reads the event trace generated by a simulator and signals whether all invariants are respected. The second part consists of mining the temporal flow of events using a newly developed representation called State Flow Temporal Analysis Graph (SFTAG). While the first part seeks an assurance of implementation correctness by checking that the model invariants hold, the second part derives an extended model of the implementation and hence enables a deeper understanding of what was implemented. The main application studied in this work is the validation of the timing behavior of micro-architecture simulators. The study includes SFTAGs generated for a wide set of benchmark programs and their analysis using several artificial intelligence algorithms. This work improves the computer architecture research and verification processes as shown by the case studies and experiments that have been conducted.

Screening, optimization and extraction of polyhydroxyalkanoates and peptidoglycan from Bacillus megaterium

Bioplastics are polymers (such as polyesters) produced from bacterial fermentations that are biodegradable and nonhazardous. They are produced by a wide variety of bacteria and are made only when stress conditions allow, such as when nutrient levels are low, more specifically levels of nitrogen and oxygen. These stress conditions cause certain bacteria to build up excess carbon deposits as energy reserves in the form of polyhydroxyalkanoates (PHAs). PHAs can be extracted and formed into actual plastic with the same strength of conventional, synthetic-based plastics without the need to rely on foreign petroleum. The overall goal of this project was to select for a bacteria that could grow on sugars found in the lignocellulosic biomass, and get the bacteria to produce PHAs and peptidoglycan. Once this was accomplished the goal was to extract PHAs and peptidoglycan in order to make a stronger more rigid plastic, by combing them into a co-polymer. The individual goals of this project were to: (1) Select and screen bacteria that are capable of producing PHAs by utilizing the carbon/energy sources found in lignocellulosic biomass; (2) Maximize the utilization of those sugars present in woody biomass in order to produce optimal levels of PHAs. (3) Use room temperature ionic liquids (RTILs) in order to separate the cell membrane and peptidoglycan, allowing for better extraction of PHAs and more intact peptidoglycan. B. megaterium a Gram-positive PHA-producing bacterium was selected for study in this project. It was grown on a variety of different substrates in order to maximize both its growth and production of PHAs. The optimal conditions were found to be 30°C, pH 6.0 and sugar concentration of either 30g/L glucose or xylose. After optimal growth was obtained, both RTILs and enzymatic treatments were used to break the cell wall, in order to extract the PHAs, and peptidoglycan. PHAs and peptidoglycan were successfully extracted from the cell, and will be used in the future to create a new stronger co-polymer. Peptidoglycan recovery yield was 16% of the cells’ dry weight.

Computational simulations of latent heat thermal energy storage systems - with innovative and first-principles based simulation for the underlying unsteady melting (and solidification) processes

This thesis develops an effective modeling and simulation procedure for a specific thermal energy storage system commonly used and recommended for various applications (such as an auxiliary energy storage system for solar heating based Rankine cycle power plant). This thermal energy storage system transfers heat from a hot fluid (termed as heat transfer fluid - HTF) flowing in a tube to the surrounding phase change material (PCM). Through unsteady melting or freezing process, the PCM absorbs or releases thermal energy in the form of latent heat. Both scientific and engineering information is obtained by the proposed first-principle based modeling and simulation procedure. On the scientific side, the approach accurately tracks the moving melt-front (modeled as a sharp liquid-solid interface) and provides all necessary information about the time-varying heat-flow rates, temperature profiles, stored thermal energy, etc. On the engineering side, the proposed approach is unique in its ability to accurately solve – both individually and collectively – all the conjugate unsteady heat transfer problems for each of the components of the thermal storage system. This yields critical system level information on the various time-varying effectiveness and efficiency parameters for the thermal storage system.

DIFFERENTIATING PATH AND SOURCE PROCESSES IN COMPLEX GEOLOGIC STRUCTURE THROUGH PASSIVE SEISMIC STUDIES: BERING GLACIER, ALASKA AND VILLARRICA VOLCANO, CHILE

Measuring shallow seismic sources provides a way to reveal processes that cannot be directly observed, but the correct interpretation and value of these signals depend on the ability to distinguish source from propagation effects. Furthermore, seismic signals produced by a resonating source can look almost identical to those produced by impulsive sources, but modified along the path. Distinguishing these two phenomena can be accomplished by examining the wavefield with small aperture arrays or by recording seismicity near to the source when possible. We examine source and path effects in two different environments: Bering Glacier, Alaska and Villarrica Volcano, Chile. Using three 3-element seismic arrays near the terminus of the Bering Glacier, we have identified and located both terminus calving and iceberg breakup events. We show that automated array analysis provided a robust way to locate icequake events using P waves. This analysis also showed that arrivals within the long-period codas were incoherent within the small aperture arrays, demonstrating that these codas previously attributed to crack resonance were in fact a result of a complicated path rather than a source effect. At Villarrica Volcano, seismometers deployed from near the vent to ~10 km revealed that a several cycle long-period source signal recorded at the vent appeared elongated in the far-field. We used data collected from the stations nearest to the vent to invert for the repetitive seismic source, and found it corresponded to a shallow force within the lava lake oriented N75°E and dipping 7° from horizontal. We also used this repetitive signal to search the data for additional seismic and infrasonic properties which included calculating seismic-acoustic delay times, volcano acoustic-seismic ratios and energies, event frequency, and real-time seismic amplitude measurements. These calculations revealed lava lake level and activity fluctuations consistent with lava lake level changes inferred from the persistent infrasonic tremor.