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.

Sustainable Energy Production in the United States: Life Cycle Assessment of Biofuels and Bioenergy

The United States of America is making great efforts to transform the renewable and abundant biomass resources into cost-competitive, high-performance biofuels, bioproducts, and biopower. This is the key to increase domestic production of transportation fuels and renewable energy, and reduce greenhouse gas and other pollutant emissions. This dissertation focuses specifically on assessing the life cycle environmental impacts of biofuels and bioenergy produced from renewable feedstocks, such as lignocellulosic biomass, renewable oils and fats. The first part of the dissertation presents the life cycle greenhouse gas (GHG) emissions and energy demands of renewable diesel (RD) and hydroprocessed jet fuels (HRJ). The feedstocks include soybean, camelina, field pennycress, jatropha, algae, tallow and etc. Results show that RD and HRJ produced from these feedstocks reduce GHG emissions by over 50% compared to comparably performing petroleum fuels. Fossil energy requirements are also significantly reduced. The second part of this dissertation discusses the life cycle GHG emissions, energy demands and other environmental aspects of pyrolysis oil as well as pyrolysis oil derived biofuels and bioenergy. The feedstocks include waste materials such as sawmill residues, logging residues, sugarcane bagasse and corn stover, and short rotation forestry feedstocks such as hybrid poplar and willow. These LCA results show that as much as 98% GHG emission savings is possible relative to a petroleum heavy fuel oil. Life cycle GHG savings of 77 to 99% were estimated for power generation from pyrolysis oil combustion relative to fossil fuels combustion for electricity, depending on the biomass feedstock and combustion technologies used. Transportation fuels hydroprocessed from pyrolysis oil show over 60% of GHG reductions compared to petroleum gasoline and diesel. The energy required to produce pyrolysis oil and pyrolysis oil derived biofuels and bioelectricity are mainly from renewable biomass, as opposed to fossil energy. Other environmental benefits include human health, ecosystem quality and fossil resources. The third part of the dissertation addresses the direct land use change (dLUC) impact of forest based biofuels and bioenergy. An intensive harvest of aspen in Michigan is investigated to understand the GHG mitigation with biofuels and bioenergy production. The study shows that the intensive harvest of aspen in MI compared to business as usual (BAU) harvesting can produce 18.5 billion gallons of ethanol to blend with gasoline for the transport sector over the next 250 years, or 32.2 billion gallons of bio-oil by the fast pyrolysis process, which can be combusted to generate electricity or upgraded to gasoline and diesel. Intensive harvesting of these forests can result in carbon loss initially in the aspen forest, but eventually accumulates more carbon in the ecosystem, which translates to a CO2 credit from the dLUC impact. Time required for the forest-based biofuels to reach carbon neutrality is approximately 60 years. The last part of the dissertation describes the use of depolymerization model as a tool to understand the kinetic behavior of hemicellulose hydrolysis under dilute acid conditions. Experiments are carried out to measure the concentrations of xylose and xylooligomers during dilute acid hydrolysis of aspen. The experiment data are used to fine tune the parameters of the depolymerization model. The results show that the depolymerization model successfully predicts the xylose monomer profile in the reaction, however, it overestimates the concentrations of xylooligomers.