SEARCH · Engineering Papers

Results for “Guaranteed performance”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

SourceResearch connectionFrom yearThrough year

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

At least 325 records · Page 18

All sources NASA NTRS DOE OSTI

NASA NTRS2009

Formally Verified Practical Algorithms for Recovery from Loss of Separation

In this paper, we develop and formally verify practical algorithms for recovery from loss of separation. The formal verification is performed in the context of a criteria-based framework. This framework provides rigorous definitions of horizontal and vertical maneuver correctness that guarantee divergence and achieve horizontal and vertical separation. The algorithms are shown to be independently correct, that is, separation is achieved when only one aircraft maneuvers, and implicitly coordinated, that is, separation is also achieved when both aircraft maneuver. In this paper we improve the horizontal criteria over our previous work. An important benefit of the criteria approach is that different aircraft can execute different algorithms and implicit coordination will still be achieved, as long as they all meet the explicit criteria of the framework. Towards this end we have sought to make the criteria as general as possible. The framework presented in this paper has been formalized and mechanically verified in the Prototype Verification System (PVS).

Butler, Ricky W.↗

NASA NTRS2013

Regression Verification Using Impact Summaries

Regression verification techniques are used to prove equivalence of syntactically similar programs. Checking equivalence of large programs, however, can be computationally expensive. Existing regression verification techniques rely on abstraction and decomposition techniques to reduce the computational effort of checking equivalence of the entire program. These techniques are sound but not complete. In this work, we propose a novel approach to improve scalability of regression verification by classifying the program behaviors generated during symbolic execution as either impacted or unimpacted. Our technique uses a combination of static analysis and symbolic execution to generate summaries of impacted program behaviors. The impact summaries are then checked for equivalence using an o-the-shelf decision procedure. We prove that our approach is both sound and complete for sequential programs, with respect to the depth bound of symbolic execution. Our evaluation on a set of sequential C artifacts shows that reducing the size of the summaries can help reduce the cost of software equivalence checking. Various reduction, abstraction, and compositional techniques have been developed to help scale software verification techniques to industrial-sized systems. Although such techniques have greatly increased the size and complexity of systems that can be checked, analysis of large software systems remains costly. Regression analysis techniques, e.g., regression testing [16], regression model checking [22], and regression verification [19], restrict the scope of the analysis by leveraging the differences between program versions. These techniques are based on the idea that if code is checked early in development, then subsequent versions can be checked against a prior (checked) version, leveraging the results of the previous analysis to reduce analysis cost of the current version. Regression verification addresses the problem of proving equivalence of closely related program versions [19]. These techniques compare two programs with a large degree of syntactic similarity to prove that portions of one program version are equivalent to the other. Regression verification can be used for guaranteeing backward compatibility, and for showing behavioral equivalence in programs with syntactic differences, e.g., when a program is refactored to improve its performance, maintainability, or readability. Existing regression verification techniques leverage similarities between program versions by using abstraction and decomposition techniques to improve scalability of the analysis [10, 12, 19]. The abstractions and decomposition in the these techniques, e.g., summaries of unchanged code [12] or semantically equivalent methods [19], compute an over-approximation of the program behaviors. The equivalence checking results of these techniques are sound but not complete-they may characterize programs as not functionally equivalent when, in fact, they are equivalent. In this work we describe a novel approach that leverages the impact of the differences between two programs for scaling regression verification. We partition program behaviors of each version into (a) behaviors impacted by the changes and (b) behaviors not impacted (unimpacted) by the changes. Only the impacted program behaviors are used during equivalence checking. We then prove that checking equivalence of the impacted program behaviors is equivalent to checking equivalence of all program behaviors for a given depth bound. In this work we use symbolic execution to generate the program behaviors and leverage control- and data-dependence information to facilitate the partitioning of program behaviors. The impacted program behaviors are termed as impact summaries. The dependence analyses that facilitate the generation of the impact summaries, we believe, could be used in conjunction with other abstraction and decomposition based approaches, [10, 12], as a complementary reduction technique. An evaluation of our regression verification technique shows that our approach is capable of leveraging similarities between program versions to reduce the size of the queries and the time required to check for logical equivalence. The main contributions of this work are: - A regression verification technique to generate impact summaries that can be checked for functional equivalence using an off-the-shelf decision procedure. - A proof that our approach is sound and complete with respect to the depth bound of symbolic execution. - An implementation of our technique using the LLVMcompiler infrastructure, the klee Symbolic Virtual Machine [4], and a variety of Satisfiability Modulo Theory (SMT) solvers, e.g., STP [7] and Z3 [6]. - An empirical evaluation on a set of C artifacts which shows that the use of impact summaries can reduce the cost of regression verification.

Backes, John↗

DOE OSTI2022

Accelerated Degradation in a Quasi-Single-Crystalline Layered Oxide Cathode for Lithium-Ion Batteries Caused by Residual Grain Boundaries

The rapidly growing demand of electrical vehicle (EV) requires high-energy-density lithium-ion batteries (LIBs) with excellent cycling stability and safety performance. However, conventional polycrystalline high-Ni cathodes severely suffer from intrinsic chemo-mechanical degradation and fast capacity fade. The emerging single-crystallization strategy offers a promising pathway to improve the chemo-mechanical stability, however, the single-crystallinity of the cathode is not always guaranteed and residual grain boundaries (GBs) could persist in nonideal synthesis conditions, leading to the formation of ‘quasi’ single-crystalline (QSC) cathodes. So far, there is a lack of understanding of the influence of these residual GBs on the electrochemical performance and structural stability. Herein, we investigate the degradation pathway of a QSC high-Ni cathode through transmission electron microscopy and X-ray techniques. The residual GBs caused by insufficient calcination time, dramatically exacerbate the cathode’s chemo-mechanical instability and cycling performance. Our work offers important guidance for the next-generation cathodes for long-life LIBs.

25 ENERGY STORAGE↗

DOE OSTI2025

Bridging interfacial properties and cell performance: A multiscale model for proton-exchange-membrane fuel cells

Here, to elucidate the impact of local interfaces on mass-transport resistance and overall cell performance of low-loaded proton-exchange-membrane fuel cells (PEMFCs), we present a multiscale modeling framework incorporating a novel modified agglomerate model. The model considers three distinct Pt-electrolyte interfaces: Pt on the carbon surface covered by either ionomer or water film and Pt inside carbon nanopores. Detailed mass-transport voltage-loss breakdowns reveal that coupled agglomerate-interface-scale mass transport dominates the mass-transport loss. The ionomer poisons the exterior-Pt surface through suppressing O 2 adsorption and intrinsic ORR activity, leading to low current-density performance. Conversely, interior-Pt interface enhances the kinetic performance but limits high current-density performance due to its low interfacial permeability. The exterior-Pt/water interface demonstrates superior kinetic performance and mass transport, though its practical implementation requires ensuring proton transport. By coupling the multiscale CL properties with ink parameters, the model identifies an optimal I to C ratio of approximately 0.5, a moderate value where the ionomer content is sufficient to guarantee proton transport without fully covering the Pt surface and forming large agglomeration, thus allowing the utilization of the Pt-water interface and avoiding high mass-transport loss. Overall, the model helps unravel limiting phenomena across different operating regimes and provides routes for optimizing performance.

Cell diagnostic↗

DOE OSTI2025

Dynamical Sketching for Enhanced Communication Efficiency in Federated Learning

Federated learning (FL) has revolutionized distributed machine learning by enabling collaborative model training without sharing local data. However, communication efficiency and privacy guarantees remain significant challenges. This paper introduces a dynamic sketching mechanism in FL, optimizing the trade-off between communication efficiency and model accuracy. By dynamically selecting the sketch matrix size, our approach adapts to the evolving characteristics of the data and the model, ensuring optimal performance across diverse scenarios. We leverage Bayesian optimization to systematically tune the sketch parameters, achieving an effective balance between resource efficiency and model performance. Experimental results on the MNIST dataset using a convolutional neural network (CNN) architecture validate the proposed method's efficiency and scalability. Our dynamic sketching approach significantly outperforms fixed-size sketching techniques, achieving higher compression ratios (up to 62x) and providing better privacy guarantees while maintaining high model accuracy. These findings highlight the robustness and versatility of our approach and make it a valuable solution for privacy-preserving, communication-efficient federated learning.

Afrose, Sharmin [ORNL]↗

NASA NTRS2020

Improving Trust in Deep Neural Networks with Nearest Neighbors

Deep neural networks are used increasingly for perception and decision-making in UAVs. For example, they can be used to recognize objects from images and decide what actions the vehicle should take. While deep neural networks can perform very well at complex tasks, their decisions may be unintuitive to a human operator. When a human disagrees with a neural network prediction, due to the black box nature of deep neural networks, it can be unclear whether the system knows something the human does not or whether the system is malfunctioning. This uncertainty is problematic when it comes to ensuring safety. As a result, it is important to develop technologies for explaining neural network decisions for trust and safety. This paper explores a modification to the deep neural network classification layer to produce both a predicted label and an explanation to support its prediction. Specifically, at test time, we replace the final output layer of the neural network classifier by a k-nearest neighbor classifier. The nearest neighbor classifier produces 1) a predicted label through voting and 2) the nearest neighbors involved in the prediction, which represent the most similar examples from the training dataset. Because prediction and explanation are derived from the same underlying process, this approach guarantees that the explanations are always relevant to the predictions. We demonstrate the approach on a convolutional neural network for a UAV image classification task. We perform experiments using a forest trail image dataset and show empirically that the hybrid classifier can produce intuitive explanations without loss of predictive performance compared to the original neural network. We also show how the approach can be used to help identify potential issues in the network and training process.

Lee, Ritchie↗

DOE OSTI2020

Suppressing Co-Crystallization of Halogenated Non-Fullerene Acceptors for Thermally Stable Ternary Solar Cells

While photovoltaic blends based on non-fullerene acceptors are touted for their thermal stability, this type of acceptor tends to crystallize, which can result in a gradual decrease in photovoltaic performance and affects the reproducibility of the devices. Two halogenated indacenodithienothiophene-based acceptors that readily co-crystallize upon mixing are studied, which indicates that the use of an acceptor mixture alone does not guarantee the formation of a disordered mixture. The addition of the donor polymer to the acceptor mixture readily suppresses the crystallization, which results in a fine-grained ternary blend with nanometer-sized domains that do not coarsen due to a high T g ≈ 200 °C. As a result, annealing at temperatures of up to 170 °C does not markedly affect the photovoltaic performance of ternary devices, in contrast to binary devices that suffer from acceptor crystallization in the active layer. The results indicate that the ternary approach enables the use of high-temperature processing protocols, which are needed for upscaling and high-throughput fabrication of organic solar cells. Further, ternary devices display a stable photovoltaic performance at 130 °C for at least 205 h, which indicates that the use of acceptor mixtures allows to fabricate devices with excellent thermal stability.

14 SOLAR ENERGY↗

DOE OSTI2023

HCPerf: Driving Performance-Directed Hierarchical Coordination for Autonomous Vehicles

The rapid development of autonomous driving poses new research challenges to the on-vehicle computing system. In particular, the execution time of autonomous driving tasks highly depends on the specific driving environment. For instance, the execution time of configurable sensor fusion increases significantly as the scene becomes complex, which leads to end-to-end deadline misses from sensing to control and may cause accidents. Thus, a framework that can effectively utilize the system resources to guarantee the end-to-end deadlines of autonomous driving tasks as well as effectively prioritize the responsiveness and throughput of the control commands is crucial for autonomous driving. In this paper, we propose HCPerf, a performance-directed hierarchical coordination framework that intelligently coordinates the autonomous driving tasks with high execution time variation and complex dependencies according to the driving performance in real-time. Specifically, HCPerf mainly consists of two coordinators. The internal coordinator intelligently schedules the tasks according to the driving performance of the vehicle in order to help them meet the end-to-end deadlines while well prioritizing the responsiveness and throughput of the control commands. At the same time, the external coordinator dynamically tunes the rates of tasks according to the schedulability in order to efficiently utilize the system resource. We conduct extensive experiments on both simulation and hardware testbeds with the representative autonomous driving application. The results show that HCPerf can effectively improve the driving performance by 7.69%-45.94% in different driving scenarios.

Ma, Jialiang↗

DOE OSTI2025

Faster solutions to the interdiction defense problem using suboptimal solutions

The interdiction defense (ID) problem solves a defender-attacker-defender model where the defender and attacker share the same set of components to harden and target. Here, we build upon the best response intersection (BRI) algorithm by developing the BRI with suboptimal solutions (BRI-SS) algorithm to solve the ID problem. The BRI-SS algorithm utilizes off-the-shelf optimization solvers that return suboptimal solutions at no additional computation cost. We derive novel cuts from suboptimal solutions, reducing the number of iterations required for the algorithm to converge while maintaining optimality guarantees. We also present a heuristic that utilizes all obtained suboptimal solutions to select the next defense to evaluate at each iteration. We perform computational experiments applied to power grid interdiction on standard test cases. Our results demonstrate that the BRI-SS algorithm consistently outperforms the BRI algorithm across all test cases.

Computer science↗

DOE OSTI2021

Unbalanced Parallel I/O: An Often-Neglected Side Effect of Lossy Scientific Data Compression

Lossy compression techniques have demonstrated promising results in significantly reducing the scientific data size while guaranteeing the compression error bounds. However, one important yet often neglected side effect of lossy scientific data compression is its impact on the performance of parallel I/O. Our key observation is that the compressed data size is often highly skewed across processes in lossy scientific compression. To understand this behavior, we conduct extensive experiments where we apply three lossy compressors MGARD, ZFP, and SZ, which are specifically designed and optimized for scientific data, to three real-world scientific applications Gray-Scott simulation, WarpX, and XGC. Our analysis result demonstrates that the size of the compressed data is always skewed even if the original data is evenly decomposed among processes. Such skewness widely exists in different scientific applications using different compressors as long as the information density of the data varies across processes. We then systematically study how this side effect of lossy scientific data compression impacts the performance of parallel I/O. We observe that the skewness in the sizes of the compressed data often leads to I/O imbalance, which can significantly reduce the efficiency of I/O bandwidth utilization if not properly handled. In addition, writing data concurrently to a single shared file through MPI-IO library is more sensitive to the unbalanced I/O loads. Therefore, we believe our research community should pay more attention to the unbalanced parallel I/O caused by lossy scientific data compression.

Wang, Xinying↗

NASA NTRS1991

An empirical approach to predicting long term behavior of metal particle based recording media

Alpha iron particles used for magnetic recording are prepared through a series of dehydration and reduction steps of alpha-Fe2O3-H2O resulting in acicular, polycrystalline, body centered cubic (bcc) alpha-Fe particles that are single magnetic domains. Since fine iron particles are pyrophoric by nature, stabilization processes had to be developed in order for iron particles to be considered as a viable recording medium for long term archival (i.e., 25+ years) information storage. The primary means of establishing stability is through passivation or controlled oxidation of the iron particle's surface. Since iron particles used for magnetic recording are small, additional oxidation has a direct impact on performance especially where archival storage of recorded information for long periods of time is important. Further stabilization chemistry/processes had to be developed to guarantee that iron particles could be considered as a viable long term recording medium. In an effort to retard the diffusion of iron ions through the oxide layer, other elements such as silicon, aluminum, and chromium have been added to the base iron to promote more dense scale formation or to alleviate some of the non-stoichiometric behavior of the oxide or both. The presence of water vapor has been shown to disrupt the passive layer, subsequently increasing the oxidation rate of the iron. A study was undertaken to examine the degradation in magnetic properties as a function of both temperature and humidity on silicon-containing iron particles between 50-120 deg C and 3-89 percent relative humidity. The methodology to which experimental data was collected and analyzed leading to predictive capability is discussed.

Hadad, Allan S.↗

NASA NTRS1993

Rapid transaction-undo recovery using twin-page storage management

This paper presents a twin-page storage method, which is an alternative to the TWIST (twin slot) approach by Reuter, for rapid transaction-undo recovery. In contrast to TWIST, our twin-page approach allows dirty pages in the buffer to be written at any instant onto disk without the requirement of undo logging, and, when a transaction is aborted, no explicit undo is required. As a result, all locks accumulated by the aborted transaction can be released earlier, allowing other transactions waiting for the locks to proceed. Through maintenance of aborted transaction identifiers, invalid pages written by the aborted transaction coexist with other valid pages and are guaranteed not be accessed by subsequent transactions. Instead of an explicit undo, most of the invalid pages are overwritten by subsequent normal updates. Performance in terms of disk I/O and CPU overhead for transaction-undo recovery is analyzed and compared with TWIST. It is shown that our scheme is particularly suited for applications where there are a large number of updates written onto disk when transactions are aborted, and there are frequent aborts. The approach, however, is not as applicable to environments where transactions are typically short or rarely aborted, or most updates are not written onto disk before a commitment.

Wu, Kun-Lung↗

DOE OSTI2021

Scalable Plug-and-Play ADMM with Convergence Guarantees

Plug-and-play priors (PnP) is a broadly applicable methodology for solving inverse problems by exploiting statistical priors specified as denoisers. Recent work has reported the state-of-the-art performance of PnP algorithms using pre-trained deep neural nets as denoisers in a number of imaging applications. However, current PnP algorithms are impractical in large-scale settings due to their heavy computational and memory requirements. This work addresses this issue by proposing an incremental variant of the widely used PnP-ADMM algorithm, making it scalable to problems involving a large number measurements. Here, we theoretically analyze the convergence of the algorithm under a set of explicit assumptions, extending recent theoretical results in the area. Additionally, we show the effectiveness of our algorithm with nonsmooth data-fidelity terms and deep neural net priors, its fast convergence compared to existing PnP algorithms, and its scalability in terms of speed and memory.

97 MATHEMATICS AND COMPUTING↗

NASA NTRS2004

Closed Loop System Identification with Genetic Algorithms

High performance control design for a flexible space structure is challenging since high fidelity plant models are di.cult to obtain a priori. Uncertainty in the control design models typically require a very robust, low performance control design which must be tuned on-orbit to achieve the required performance. Closed loop system identi.cation is often required to obtain a multivariable open loop plant model based on closed-loop response data. In order to provide an accurate initial plant model to guarantee convergence for standard local optimization methods, this paper presents a global parameter optimization method using genetic algorithms. A minimal representation of the state space dynamics is employed to mitigate the non-uniqueness and over-parameterization of general state space realizations. This control-relevant system identi.cation procedure stresses the joint nature of the system identi.cation and control design problem by seeking to obtain a model that minimizes the di.erence between the predicted and actual closed-loop performance.

Whorton, Mark S.↗

NASA NTRS2019

Trends in Human Spaceflight: Failure Tolerance, High Reliability and Correlated Failure History

In a half century of human spaceflight, NASA has continuously refined agency safety and reliability requirements in response to mission demands, critical failures, and technology development. Early spacecraft, including Mercury, Gemini and Apollo vehicles, were highly reliant on dissimilar redundancy and demonstrated test margins. Later programs, such as the reusable Space Transportation System (STS) and International Space Station (ISS), introduced probabilistic studies and isolated two-failure tolerance to improve robustness at the expense of added complexity. More recently, the Orion Multi-Program Crew Vehicle (MPCV) program adopted universal single-failure tolerance with two categorical exceptions; Zero-Failure Tolerant (0FT) and Design for Minimum Risk (DFMR) hardware. Failure tolerance variances are defined and managed in accordance with agency human-rating requirements, and require concurrence from program Technical Authorities (TA) as well as the MPCV Safety and Mission Assurance Safety and Engineering Review Panel (MSERP). To understand and reaffirm standards applied to Apollo, Space Shuttle and Orion vehicles, Orion and Deep Space Gateway Safety and Mission Assurance (S&MA) representatives conducted accelerated research to compare unique safety and reliability criteria against ground and flight anomalies, based on information contained in post-mission reports and the Problem Reporting and Corrective Action (PRACA) database. In some cases, high-profile failures and narrow escapes have reinforced decisions to maintain or adapt safety requirements. In others, empirical trends have highlighted the need for vigilance and innovative safety guidelines. Given the inability to achieve absolute compliance with evolving safety and reliability requirements, the team conducted a targeted review of DFMR and 0FT propulsion elements within the framework of changing system design, inspection, materials and process developments to formulate conclusions on technological maturity, failure density, and net changes in safety risk. Based on the aggregate performance of high-reliability and failure-tolerant systems, the authors have attempted to establish best practices and guidelines to inform future program decisions. On a somewhat cautionary note, this study is not intended to direct a universal set of requirements for future missions based on prior lessons learned. Spacecraft safety is a multi-variable problem, and attempts to mitigate past failures will not guarantee future success. However, this assessment offers a retrospective review of policy changes, implementation and effectiveness. In the future, NASA, European Space Agency (ESA) and industry partners may benefit from a more robust correlation between requirements and performance, as space-faring nations work toward more challenging, complex and long-duration commercial and deep-space ventures.

Green, Carrie↗

DOE OSTI2022

An Algorithmic and Software Pipeline for Very Large Scale Scientific Data Compression with Error Guarantees

Efficient data compression is becoming increasingly critical for storing scientific data because many scientific applications produce vast amounts of data. This paper presents an end-to-end algorithmic and software pipeline for data compression that guarantees both error bounds on primary data (PD) and derived data, known as Quantities of Interest (QoI).We demonstrate the effectiveness of the pipeline by compressing fusion data generated by a large-scale fusion code, XGC, which produces tens of petabytes of data in a single day. We demonstrate that the compression is conducted by setting aside computational resources known as staging nodes, and does not impact the simulation performance. For efficient parallel I/O, the pipeline uses ADIOS2, which many codes such as XGC already use for their parallel I/O. We show that our approach can compress the data by two orders of magnitude while guaranteeing high accuracy on both the PD and the QoIs. Further, the amount of resources required by compression is a few percent of the resources required by simulation while ensuring that the compression time for each stage is less than the corresponding simulation time.This pipeline consists of three main steps. The first step decomposes the data using domain decomposition into small subdomains. Each subdomain is then compressed independently to achieve a high level of parallelism. The second step uses existing techniques that guarantee error bounds on the primary data for each subdomain. The third step uses a post-processing optimization technique based on Lagrange multipliers to reduce the QoI errors for data corresponding to each subdomain. The Lagrange multipliers generated can be further quantized or truncated to increase the compression level. All of the above characteristics of our approach make it highly practical to apply on-the-fly compression while guaranteeing errors on QoIs that are critical to the scientists.

Banerjee, Tania↗

DOE OSTI2023

Resonant anomaly detection with multiple reference datasets

An important class of techniques for resonant anomaly detection in high energy physics builds models that can distinguish between reference and target datasets, where only the latter has appreciable signal. Such techniques, including Classification Without Labels (CWoLa) and Simulation Assisted Likelihood-free Anomaly Detection (SALAD) rely on a single reference dataset. They cannot take advantage of commonly available multiple datasets and thus cannot fully exploit available information. In this work, we propose generalizations of CWoLa and SALAD for settings where multiple reference datasets are available, building on weak supervision techniques. We demonstrate improved performance in a number of settings with realistic and synthetic data. As an added benefit, our generalizations enable us to provide finite-sample guarantees, improving on existing asymptotic analyses.

72 PHYSICS OF ELEMENTARY PARTICLES AND FIELDS↗

DOE OSTI2024

Local convergence analysis of an inexact trust-region method for nonsmooth optimization

In Baraldi, we introduced an inexact trust-region algorithm for minimizing the sum of a smooth nonconvex function and a nonsmooth convex function in Hilbert space—a class of problems that is ubiquitous in data science, learning, optimal control, and inverse problems. Furthermore, this algorithm has demonstrated excellent performance and scalability with problem size. In this paper, we enrich the convergence analysis for this algorithm, proving strong convergence of the iterates with guaranteed rates. In particular, we demonstrate that the trust-region algorithm recovers superlinear, even quadratic, convergence rates when using a second-order Taylor approximation of the smooth objective function term.

97 MATHEMATICS AND COMPUTING↗