Browsing by Subject "Alloy"
Now showing 1 - 14 of 14
Results Per Page
Sort Options
Item Application of local semantic analysis in fault prediction and detection(2010-05) Shao, Danhua; Khurshid, Sarfraz; Perry, Dewayne E.; Julien, Christine; Barber, Suzanne; Browne, James C.; Lifschitz, VladimirTo improve quality of software systems, change-based fault prediction and scope-bounded checking have been used to predict or detect faults during software development. In fault prediction, changes to program source code, such as added lines or deleted lines, are used to predict potential faults. In fault detection, scope-bounded checking of programs is an effective technique for finding subtle faults. The central idea is to check all program executions up to a given bound. The technique takes two basic forms: scope-bounded static checking, where all bounded executions of a program are transformed into a formula that represents the violation of a correctness property and any solution to the formula represents a counterexample; or scope-bounded testing where a program is tested against all (small) inputs up to a given bound on the input size. Although the accuracies of change-based fault prediction and scope-bounded checking have been evaluated with experiments, both of them have effectiveness and efficiency limitations. Previous change-based fault predictions only consider the code modified by a change while ignoring the code impacted by a change. Scope-bounded testing only concerns the correctness specifications, and the internal structure of a program is ignored. Although scope-bounded static checking considers the internal structure of programs, formulae translated from structurally complex programs might choke the backend analyzer and fail to give a result within a reasonable time. To improve effectiveness and efficiency of these approaches, we introduce local semantic analysis into change-based fault prediction and scope-bounded checking. We use data-flow analysis to disclose internal dependencies within a program. Based on these dependencies, we identify code segments impacted by a change and apply fault prediction metrics on impacted code. Empirical studies with real data showed that semantic analysis is effective and efficient in predicting faults in large-size changes or short-interval changes. While generating inputs for scope-bounded testing, we use control-flow to guide test generation so that code coverage can be achieved with minimal tests. To increase the scalability of scope-bounded checking, we split a bounded program into smaller sub-programs according to data-flow and control-flow analysis. Thus the problem of scope-bounded checking for the given program reduces to several sub-problems, where each sub-problem requires the constraint solver to check a less complex formula, thereby likely reducing the solver’s overall workload. Experimental results show that our approach provides significant speed-ups over the traditional approach.Item AUnit - a testing framework for alloy(2014-05) Sullivan, Allison; Khurshid, SarfrazWriting declarative models of software designs and analyzing them to detect defects is an effective methodology for developing more dependable software systems. However, writing such models correctly can be challenging for practitioners who may not be proficient in declarative programming, and their models themselves may be buggy. We introduce the foundations of a novel test automation framework, AUnit, which we envision for testing declarative models written in Alloy -- a first-order, relational language that is supported by its SAT-based analyzer. We take inspiration from the success of the family of xUnit frameworks that are used widely in practice for test automation, albeit for imperative or object-oriented programs. The key novelty of our work is to define a basis for unit testing for Alloy, specifically, to define the concepts of test case and test coverage as well as coverage criteria for declarative models. We reduce the problems of declarative test execution and coverage computation to partial evaluation without requiring SAT solving. Our vision is to blend how developers write unit tests in commonly used programming languages with how Alloy users formulate their models in Alloy, thereby facilitating the development and testing of Alloy models for both new Alloy users as well as experts. We illustrate our ideas using a small but complex Alloy model. While we focus on Alloy, our ideas generalize to other declarative languages (such as Z, B, ASM).Item Chemical modification of nanocolumnar semiconductor electrodes for enhanced performance as lithium and sodium-ion battery anode materials(2014-08) Abel, Paul Robert; Mullins, C. B.Chemical EngineeringItem Contract-based data structure repair using alloy(2010-05) Nokhbeh Zaeem, Razieh; Khurshid, Sarfraz; McKinley, Kathryn S.Contracts and specifications have long been used in object-oriented design, programming and testing to enhance reliability before software deployment. However, the use of specifications in deployed software is commonly limited to runtime checking where assertions form a basis for detecting incorrect program states to terminate the erroneous executions. We present a contract-based approach for data structure repair, which repairs erroneous states in deployed software. The key novelty is the support for rich behavioral specifications, such as those that relate pre-states with post-states of a method to accurately specify expected behavior and precise repair. The approach is based on the view of a specification as a non-deterministic implementation. The key insight is to use any correct state mutations by an otherwise erroneous execution to prune non-determinism in the specification, thereby transmuting the specification to an implementation that does not incur a prohibitively high performance penalty. While invariants, pre-conditions and post-conditions could be provided in different modeling languages, we leverage the Alloy tool-set, specifically the Alloy language and the Alloy Analyzer for systematically repairing erroneous states. Four different algorithms are presented and implemented in our data structure repair framework. These algorithms can repair a medium sized erroneous data structure in a few seconds. We introduce repair guide annotations defined by the user to improve the accuracy and performance of the repair mechanism. Experiments using complex specifications show the approach holds much promise in increasing software reliability.Item Contract-driven data structure repair : a novel approach for error recovery(2014-05) Nokhbeh Zaeem, Razieh; Khurshid, SarfrazSoftware systems are now pervasive throughout our world. The reliability of these systems is an urgent necessity. A large degree of research effort on increasing software reliability is dedicated to requirements, architecture, design, implementation and testing---activities that are performed before system deployment. While such approaches have become substantially more advanced, software remains buggy and failures remain expensive. We take a radically different approach to reliability from previous approaches, namely contract-driven data structure repair for runtime error recovery, where erroneous executions of deployed software are corrected on-the-fly using rich behavioral contracts. Our key insight is to transform the software contract---which gives a high level description of the expected behavior---to an efficient implementation which repairs the erroneous data structures in the program state upon an error. To improve efficiency, scalability, and effectiveness of repair, in addition to rich behavioral contracts, we leverage the current erroneous state, dynamic behavior of the program, as well as repair history and abstraction. A core technical problem our approach to repair addresses is construction of structurally complex data that satisfy desired properties. We present a novel structure generation technique based on dynamic programming---a classic optimization approach---to utilize the recursive nature of the structures. We use our technique for constraint-based testing. It provides better scalability than previous work. We applied it to test widely-used web browsers and found some known and unknown bugs. Our use of dynamic programming in structure generation opens a new future direction to tackle the scalability problem of data structure repair. This research advances our ability to develop correct programs. For programs that already have contracts, error recovery using our approach can come at a low cost. The same contracts can be used for systematically testing code before deployment using existing as well as our new techniques. Thus, we enable a novel unification of software verification and error recovery.Item A demonstration of applying alloy to mechanical synthesis of electromechanical systems(2015-12) Liu, David Allen; Khurshid, Sarfraz; Garg, VijayFormal verification methods have traditionally been used in industry for proofs of functional correctness; more recent advances in their use have given rise to additional applications in new domains. Electromechanical systems such as automotive transmissions or robotics have relied heavily on software and mechanical modeling to operate and test the given design; modeling tools that support automated analysis such as Alloy allow formal analysis techniques to apply to this domain, and also enable synthesis. Specifically, Alloy provides a language and toolset that can abstractly represent and solve for real-world instances, which enable engineers to develop a deeper understanding of the systems they are building. This goal of the report is to demonstrate the potential of applying the Alloy toolset for modeling and analysis to assist in the synthesis and operational correctness of software-driven mechanical designs. A survey of literature has been included to demonstrate the foundation of concepts and previous research done in the area, spanning both formal verification and electromechanical design fields. The report also includes two small but illustrative case studies that attempt at mechanical synthesis (or design seeding) using Alloy, and report the abstraction methods and techniques that succeeded in demonstrating design synthesis efforts.Item Methods for modifying the physical and catalytic properties of surfaces(2010-05) Flaherty, David William, 1980-; Mullins, C. B.; Henkelman, Graeme; Hwang, Gyeong S.; Korgel, Brian A.; Sitz, Greg O.Catalysts can be significantly improved by modifying their structure or composition. Simple adaptations of the physical structure of a catalyst can give rise to changes in the chemical behavior, in part, due to alterations in the coordination of active sites. Modifications in the surface or bulk composition of a material have a profound impact on the chemistry that is promoted as a result of electronic and physical factors. Optimizing these qualities may enhance the catalyst’s activity, selectivity or stability. In this dissertation, we explore the application of two distinct approaches for modifying the chemical properties of catalytically active materials. Through the use of a broad array of techniques we quantify changes in critical properties such as physical-crystallographic structure; morphology, surface area and porosity; as well as catalytic activity, selectivity and stability. First, reactive ballistic deposition of metal atoms within a low pressure gas provides a unique opportunity for synthesizing thin films of a wide variety of materials. The morphology, structure, and porosity of the resulting material can be tailored through control of the deposition angle and substrate temperature. By conducting deposition perpendicular to the surface, a film can be grown with a dense, conformal structure. On the other hand, deposition at oblique angles results in high surface area, porous films comprised of regular arrays of nanocolumnar structures. Furthermore, variations in the deposition angle allow for the inclusion of under-coordinated sites which change the chemical activity of the surface. Improvements in the activity, selectivity and stability of transition metal catalysts can be made by alloying the catalyst with a second element. The formation of molybdenum carbide decreases the strength of chemisorption on the surface, with respect to molybdenum, and improves selectivity for the dehydrogenation of formic acid. Platinum is active for the water-gas shift reaction. However, this catalyst cannot operate at low temperatures due to CO poisoning and is susceptible to deactivation due to accumulation of carbonaceous deposits. The formation of a platinum-copper near-surface alloy dramatically modifies the interactions of the surface with CO, H₂O and H₂ which can enhance the performance of this catalyst for the water-gas shift reaction.Item MuAlloy : an automated mutation system for alloy(2015-05) Wang, Kaiyuan; Khurshid, Sarfraz; Perry, Dewayne E.Mutation is a powerful technique that researchers have studied for several decades in the context of imperative code. For example, mutation testing is commonly considered a '"gold standard"' for test suite quality. Mutation in the context of declarative languages is a less studied problem. This thesis introduces a foundation for mutation-driven analyses for Alloy, a first-order, declarative language based on relations. Specifically, we introduce a family of mutation operators for Alloy models and define algorithms for applying the operators on different parts of the models. We embody these operators and algorithms in our prototype tool MuAlloy that provides a GUI-based front-end for customizing the application of mutation operators. To demonstrate the potential of our approach, we illustrate the use of MuAlloy in two application scenarios: (1) mutation testing for Alloy (in the spirit of traditional mutation testing for imperative languages); and (2) program repair for Alloy using mutation.Item Shape memory response of ni2mnga and nimncoin magnetic shape memory alloys under compression(2009-05-15) Brewer, Andrew LeeIn this study, the shape memory response of Ni2MnGa and NiMnCoIn magnetic shape memory alloys was observed under compressive stresses. Ni2MnGa is a magnetic shape memory alloy (MSMA) that has been shown to exhibit fully reversible, stressassisted magnetic field induced phase transformation (MFIPT) in the I X-phase transformation because of a large magnetostress of 7 MPa and small stress hysteresis. The X-phase is a recently discovered phase that is mechanically induced, however, the crystal structure is unknown. To better understand the transformation behavior of Ni2MnGa single crystal with [100] orientation, thermal cycling and pseudoelasticity tests were conducted with the goal of determining the Clausius-Clapeyron relationships for the various phase transformations. This information was then used to construct a stresstemperature phase diagram that illustrates the stress and temperature ranges where MFIPT is possible, as well as where the X-phase may be found. NiMnCoIn is a recently discovered meta-magnetic shape memory alloy (MMSMA) that exhibits unique magnetic properties. The ferromagnetic parent phase and the paramagnetic martensite phase allow the exploitation of the Zeeman energy. To gain a better understanding of the transformation behavior of NiMnCoIn, thermal cycling and pseudoelasticity tests were conducted on single crystals from two different batches with crystallographic orientations along the [100](011), [087], and [25 7 15] directions. A stress-temperature phase diagram was created that illustrates the Clausius- Clapeyron relationships for each orientation and batch. SQUID tests revealed the magnetic response of the alloy as well as the suppression of the martensite start temperature with increasing magnetic field. Pseudoelasticity experiments with and without magnetic field were conducted to experimentally quantify the magnetostress as a function of magnetic field. For the first time, it has been shown that NiMnCoIn is capable of exhibiting magnetostress levels of 18-36 MPa depending upon orientation, as well as nearly 6.5% transformation strain in the [100] direction. The results of this study reveal increased actuation stress levels in NiMnCoIn, which is the main limitation in most MSMAs. With this increased blocking stress, NiMnCoIn is a strong candidate for MFIPT.Item Simulation tools for predicting the atomic configuration of bimetallic catalytic surfaces(2012-12) Stephens, John Adam; Hwang, Gyeong S.Transition metal alloys are an important class of materials in heterogeneous catalysis due in no small part to the often greatly enhanced activity and selectivity they exhibit compared to their monometallic constituents. A host of experimental and theoretical studies have demonstrated that, in many cases, these synergistic effects can be attributed to atomic-scale features of the catalyst surface. Realizing the goal of designing -- rather than serendipitously discovering -- new alloy catalysts thus depends on our ability to predict their atomic configuration under technologically relevant conditions. This dissertation presents original research into the development and use of computational tools to accomplish this objective. These tools are all based on a similar strategy: For each of the alloy systems examined, cluster expansion (CE) Hamiltonians were constructed from the results of density functional theory (DFT) calculations, and then used in Metropolis Monte Carlo (MC) simulations to predict properties of interest. Following a detailed description of the DFT+CE+MC simulation scheme, results for the AuPd/Pd(111) and AuPt/Pt(111) surface alloys are presented. These two systems exhibit considerably different trends in their atomic arrangement, which are explicable in terms of their interatomic interactions. In AuPd, a preference for heteronuclear, Au-Pd interactions results in the preferential formation of Pd monomers and other small ensembles, while in AuPt, a preference for homonuclear interactions results in the opposite. AuPd/Pd(100) and AuPt/Pt(100) were similarly examined, revealing not only the effects of the same heteronuclear/homonuclear preferences in this facet, but also a propensity for the formation of second nearest-neighbor pairs of Pd monomers, in close agreement with experiment. Subsequent simulations of the AuPd/Pd(100) surface suggest the application of biaxial compressive strain as a means increasing the population of this catalytically important ensemble of atoms. A method to incorporate the effects of subsurface atomic configuration is also presented, using AuPd as an example. This method represents several improvements over others previously reported in the literature, especially in terms of its simplicity. Finally, we introduce the dimensionless scaled pair interaction, whereby the finite-temperature atomic configuration of any bimetallic surface alloy may be predicted from a small number of relatively inexpensive calculations.Item Synthesis and characterization of patterned surfaces and catalytically relevant binary nanocrystalline intermetallic compounds(2009-05-15) Cable, Robert E.As devices and new technologies continue to shrink, nanocrystalline multi-metal compounds are becoming increasingly important for high efficiency and multifunctionality. However, synthetic methods to make desirable nanocrystalline multi-metallics are not yet matured. In response to this deficiency, we have developed several solution-based methods to synthesize nanocrystalline binary alloy and intermetallic compounds. This dissertation describes the processes we have developed, as well as our investigations into the use of lithographically patterned surfaces for template-directed self-assembly of solution dispersible colloids. We used a modified polyol process to synthesize nanocrystalline intermetallics of late transition and main-group metals in the M-Sn, Pt-M?, and Co-Sb systems. These compounds are known to have interesting physical properties and as nanocrystalline materials they may be useful for magnetic, thermoelectric, and catalytic applications. While the polyol method is quite general, it is limited to metals that are somewhat easy to reduce. Accordingly, we focused our synthetic efforts on intermetallics comprised of highly electropositive metals. We find that we can react single-metal nanoparticles with zero-valent organometallic Zinc reagents in hot, coordinating amine solvents via a thermal decomposition process to form several intermetallics in the M??-Zn system. Characterization of the single-metal intermediates and final intermetallic products shows a general retention of morphology throughout the reaction, and changes in optical properties are also observed. Following this principle of conversion chemistry, we can employ the high reactivity of nanocrystals to reversibly convert between intermetallic phases within the Pt-Sn system, where PtSn2 ? PtSn ? Pt3Sn. Our conversion chemistry occurs in solution at temperatures below 300 ?C and within 1 hour, highlighting the high reactivity of our nanocrystalline materials compared to the bulk. Some evidence of the generality for this process is also presented. Our nanocrystalline powders are dispersible in solution, and as such are amenable to solution-based processing techniques developed for colloidal dispersions. Accordingly, we have investigated the use of lithographically patterned surfaces to control the self-assembly of colloidal particles. We find that we can rapidly crystallize 2-dimensional building blocks, as well as use epitaxial templates to direct the formation of interesting superlattice structures comprised of a bidisperse population of particles.Item Synthesis of vinyl acetate on palladium-based catalysts(2009-06-02) Kumar, DheerajVinyl acetate (VA) is an important monomer used in the production of paints, surface coatings and adhesives. Synthesis of VA is usually carried out over supported Pd alloy catalysts with a selectivity as high as 96% and described as C2H4 + CH3COOH + ? O2 -> C2H3OOCCH3 + H2O Although the VA synthesis reaction has been industrially carried out for many years, the nature of the active sites and the reaction mechanism is still unclear. The goal of this study was to acquire a fundamental understanding of the VA reaction mechanism by carrying out detailed kinetic and spectroscopic investigations on single crystals and supported Pd catalysts, and to detail the role of alloying in optimizing the selectivity of this important industrial reaction. A combination of surface science techniques and kinetic measurements has been used to address the mechanism. Supported catalysts, 1 wt% Pd/SiO2 and 5 wt% Pd/SiO2, and 1 wt% Pd-0.5 wt% Au/SiO2, were prepared by an incipient wet-impregnation method and characterized using XRD and TEM. On Pd-only catalysts the reaction rates were found to be: Pd(100) < 5 wt% Pd/SiO2 (dpd = 4.2 nm) < 1 wt% Pd/SiO2 (dpd = 2.5 nm). Particle size-dependence of the reaction rates is evident for the Pd-only catalysts, which suggests a degree of structure sensitivity of the reaction. There is an increased availability of uncoordinated, edge atoms on small particles. With a Pd single crystal, fewer less-coordinated surface sites are present compared to a comparable area on a small Pd particle on a supported Pd catalyst. The formation of Pd carbide (PdCx) during the synthesis of VA was investigated over Pd/SiO2 catalysts with two different Pd particle sizes, as well as over a Pd-Au/SiO2 mixed-metal catalyst. XRD data indicate that smaller Pd particles show greater resistance to the formation of PdCx. The alloying of Au with Pd is apparently very effective in preventing PdCx formation in Pd-based catalysts for VA synthesis. Addition of Au to Pd/SiO2 catalysts significantly enhances the VA formation rate and selectivity. Infrared reflection absorption spectroscopy (IRAS) of CO on Pd/Au(100) and Pd/Au(111) confirms the presence of Pd as isolated monomers on a Au-rich surface. A pair of Pd monomers is the most favorable active site for the formation of VA. The spacing between the two active isolated Pd atoms is critical and is demonstrated by the relative rates of VA formation on Pd/Au model catalysts, i.e. Pd/Au(111) < Pd/Au(100). The role of Au is to isolate the surface Pd atoms and thus suppress the formation of by products, CO and CO2. A pair of Pd monomers required for VA synthesis is further confirmed by the results from model studies of Sn-Pd.Item Systematic testing using test summaries : effective and efficient testing of relational applications(2011-12) Abdul Khalek, Shadi; Khurshid, Sarfraz; Perry, Dewayne E.; Batory, Don; Emerson, Allen E.; Aziz, AdnanThis dissertation presents a novel methodology based on test summaries, which characterize desired tests as constraints written in a mixed imperative and declarative notation, for automated systematic testing of relational applications, such as relational database engines. The methodology has at its basis two novel techniques for effective and efficient testing: (1) mixed-constraint solving, which provides systematic generation of inputs characterized by mixed-constraints using translations among different data domains; and (2) clustered test execution, which optimizes execution of test suites by leveraging similarities in execution traces of different tests using abstract-level undo operations, which allow common segments of partial traces to be executed only once and the execution results to be shared across those tests. A prototype embodiment of the methodology enables a novel approach for systematic testing of commonly used database engines, where test summaries describe (1) input SQL queries, (2) input database tables, and (3) expected output of query execution. An experimental evaluation using the prototype demonstrates its efficacy in systematic testing of relational applications, including Oracle 11g, and finding bugs in them.Item Theoretical study of correlation between structure and function for nanoparticle catalysts(2014-12) Zhang, Liang, 1986; Henkelman, GraemeThe science and technology of catalysis is more important today than at any other time in our history due to the grand energy and environment challenges we are facing. With the explosively growth of computation power nowadays, computer simulation can play an increasingly important role in the design of new catalysts, avoiding the costly trail-and-error attempts and facilitating the development cycle. The goal to inverse design of new materials with desired catalytic property was once far off, but now achievable. The major focus of this dissertation is to find the general rules that govern the catalytic performance of a nanoparticle as the function of its structure. Three types of multi-metallic nanoparticles have been investigated in this dissertation, core-shell, random alloy and alloy-core@shell. Significant structural rearrangement was found on Au@Pt and Pd@Pt nanoparticle, which is responsible for a dramatic improvement in catalytic performance. Nonlin- ear binding trends were found and modeled for random alloy nanoparticles, providing a prescription for tuning catalytic activity through alloying. Studies of ORR on Pd/Au random alloy NP and hydrogenation reaction on Rh/Ag random alloy NP revealed that binding on individual ensemble should be in- vestigated when large disparity of adsorbate affinity is presented between two alloying elements. In the alloy-core@shell system, I demostrated a general linear correlations between the adsorbate binding energy to the shell of an alloy-core@shell nanoparticle and the composition of the core. This relation- ship allows for interpolation of the properties of single-core@shell particles and an approach for tuning the catalytic activity of the particle. A series of promising catalysts were then predicted for ORR, HER and CO oxidation. As a first attempt to bridge the material gap, bimetallic nano clus- ter supported on CeO₂(111) was investigated for CO oxidation. A strong support-metal interaction induces a preferential segregation of the more reac- tive element to the NC-CeO₂ perimeter, generating an interface with the Au component. (Au-Cu)/CeO₂ was found to be optimal for catalyzing CO oxida- tion via a bifunctional mechanism. O₂ preferentially binds to the Cu-rich sites whereas CO binds to the Au-rich sites. A method called distributed replica dynamics (DRD) is proposed at last to utilize enormous distributed computing resources for molecular dynamics simulations of rare-event in chemical reac- tions. High efficiency can be achieved with an appropriate choice of N [subscript rep] and t [subscript rep] for long-time MD simulation.