Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Formal Methods”

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.

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

At least 55 records · Page 3
All sourcesNASA NTRSDOE OSTI
DOE OSTI2020

On the Formalization of Development and Assessment Process for Digital Twins in the Nearly Autonomous Management and Control System

In recent years, the autonomous control system has been encouraged in advanced reactors for restoring economic viability, simplifying the operation and maintenance, and enabling remote-site power generations [1]. Since the reactor is expected to be operated for a long period of time with a limited number of individuals onsite, it is recommended that the autonomous control system should have access to very realistic models of the state of processes in the whole lifecycle, together with these process behaviors in interaction with their environment in the real world. As a result, digital twin (DT) technology is suggested in autonomous control systems. DT is defined as a digital representation of a physical object or system, which contains a record for the histories of loads, operation and maintenance status, predictions for the near-term transient of important state variables, and decision-making process [2]. Since machine learning (ML) can recognize patterns within a complex system in real-time applications, it has been used to build DTs in the autonomous control systems for advanced reactors. Meanwhile, due to the rareness of operation data in accident scenarios, the development and assessment of DTs is expected to be mainly driven by simulations. Although the capability and feasibility of ML-based DTs are recognized in improving the safety and efficiency of reactor control, a major concern from the regulatory commission and the nuclear industry is whether the information from a DT is developed and assessed in accordance with expectation and requirements by the target decision. Such concerns not only affect the acceptance criteria for DTs, but also values that can be extracted from DTs and autonomous control system during operations. Inspired by the success of formal methods in improving the reliability and robustness of computer programming and software development, it is suggested that the development and assessment process (DAP) for both separate DTs and integral control system should be formalized in a transparent, consistent, and improvable manner. In this study, a digital-twin development and assessment process (DT-DAP) is proposed by adapting the evaluation model development and assessment process (EMDAP) [3] to requirements by the autonomous control system, ML algorithms, and DT technology. To demonstrate the framework, a baseline nearly autonomous management and control (NAMAC) system with ML-based DTs for diagnosis and prognosis is developed and assessed based on the framework. It is found that with selected testing methods and techniques, the DT-DAP can help identify errors in DTs and NAMAC which would otherwise be left unverified. Meanwhile, it is found that the DT-DAP can improve the DTs and NAMAC by continuously learning and iterating through different elements.

22 GENERAL STUDIES OF NUCLEAR REACTORS↗
DOE OSTI2015

A paradigm shift - the key to optimal, defensible and transparent waste management, disposal and remediation decisions - 15236

Current methods for structuring nuclear waste management, disposal, and remediation decisions are subject to three major limitations. First, they are based on a series of extraordinarily conservative assumptions. The dominant way of thinking is that, for example, conservative models yield better, safer decisions. Second, they lack methods to meaningfully address and incorporate the 'human dimension'. The dominant way of thinking is that the current approach is sufficient to bring together the values and interests of both internal and external stakeholders in making a decision. And third, they lack a formal method through which both internal and external stakeholders are encouraged collectively to 'think through' complex problems that contain multiple competing objectives so that wise, socially acceptable, and scientifically-defensible decisions are made. To overcome these limitations, a paradigm shift is needed towards a holistic, integrated approach to structure nuclear waste management, disposal and remediation decisions. The first requirement of this paradigm shift is the realization and recognition that the problems faced are decision problems, and that there is a formal theory of decision analysis that can, and should, be used to support finding the best solutions. Decision analysis, very simply, is formalized common sense. The reason it is needed for complex problems is that there are too many moving parts (variables) for humans to manage with out the formalism. Decision analysis leads to addressing problem solving using a combination of a science-based model and a costs/values model. Expectation ('realism') and uncertainty are addressed in the science-based models, whereas stakeholder values, preferences, and desires are addressed when modeling costs and value judgments. Science-based modeling tools have been developed, improved, and used since the current regulatory setting was introduced about 30 years ago. However, modeling of costs and value judgments has not often been addressed using any formal approach, despite the openings that exist in regulations (e.g., CERCLA's modifying criteria and the concept of 'as low as reasonably achievable' referenced in DOE Orders). A discussion of the need and rationale for this paradigm shift is presented, followed by a description of the technical basics of this approach to decision modeling, and ending with an explanation of the steps that are taken in this approach to structured decision-making. A software framework program called Guided Interactive Statistical Decision Tools (GiSdT - pronounced 'gist') is introduced that supports this paradigm shift. (authors)

12 MANAGEMENT OF RADIOACTIVE AND NON-RADIOACTIVE W↗
DOE OSTI2022

Multinode Multi-GPU Two-Electron Integrals: Code Generation Using the Regent Language

The computation of two-electron repulsion integrals (ERIs) is often the most expensive step of integral-direct self-consistent field methods. Formally it scales as O(N 4 ), where N is the number of Gaussian basis functions used to represent the molecular wave function. In practice, this scaling can be reduced to O(N 2 ) or less by neglecting small integrals with screening methods. The contributions of the ERIs to the Fock matrix are of Coulomb (J) and exchange (K) type and require separate algorithms to compute matrix elements efficiently. We previously implemented highly efficient GPU-accelerated J-matrix and K-matrix algorithms in the electronic structure code TeraChem. Although these implementations supported the use of multiple GPUs on a node, they did not support the use of multiple nodes. This presents a key bottleneck to cutting-edge ab initio simulations of large systems, e.g., excited state dynamics of photoactive proteins. We present our implementation of multinode multi-GPU J- and K-matrix algorithms in TeraChem using the Regent programming language. Regent directly supports distributed computation in a task-based model and can generate code for a variety of architectures, including NVIDIA GPUs. We demonstrate multinode scaling up to 45 GPUs (3 nodes) and benchmark against hand-coded TeraChem integral code. Finally, we also outline our metaprogrammed Regent implementation, which enables flexible code generation for integrals of different angular momenta.

37 INORGANIC, ORGANIC, PHYSICAL, AND ANALYTICAL CH↗
DOE OSTI2018

The multi-assumption architecture and testbed (MAAT v1.0): R code for generating ensembles with dynamic model structure and analysis of epistemic uncertainty from multiple sources

Abstract. Here, computer models are ubiquitous tools used to represent systems across many scientific and engineering domains. For any given system, many computer models exist, each built on different assumptions and demonstrating variability in the ways in which these systems can be represented. This variability is known as epistemic uncertainty, i.e. uncertainty in our knowledge of how these systems operate. Two primary sources of epistemic uncertainty are (1) uncertain parameter values and (2) uncertain mathematical representations of the processes that comprise the system. Many formal methods exist to analyse parameter-based epistemic uncertainty, while process-representation-based epistemic uncertainty is often analysed post hoc, incompletely, informally, or is ignored. In this model description paper we present the multi-assumption architecture and testbed (MAAT v1.0) designed to formally and completely analyse process-representation-based epistemic uncertainty. MAAT is a modular modelling code that can simply and efficiently vary model structure (process representation), allowing for the generation and running of large model ensembles that vary in process representation, parameters, parameter values, and environmental conditions during a single execution of the code. MAAT v1.0 approaches epistemic uncertainty through sensitivity analysis, assigning variability in model output to processes (process representation and parameters) or to individual parameters. In this model description paper we describe MAAT and, by using a simple groundwater model example, verify that the sensitivity analysis algorithms have been correctly implemented. The main system model currently coded in MAAT is a unified, leaf-scale enzyme kinetic model of C 3 photosynthesis. In the Appendix we describe the photosynthesis model and the unification of multiple representations of photosynthetic processes. The numerical solution to leaf-scale photosynthesis is verified and examples of process variability in temperature response functions are provided. For rapid application to new systems, the MAAT algorithms for efficient variation of model structure and sensitivity analysis are agnostic of the specific system model employed. Therefore MAAT provides a tool for the development of novel or toy models in many domains, i.e. not only photosynthesis, facilitating rapid informal and formal comparison of alternative modelling approaches.

54 ENVIRONMENTAL SCIENCES↗
DOE OSTI2016

A Paradigm Shift continued: An Application of Structured Decision Making for Sustainable Waste Management - 16486

Structured decision making presents an opportunity for DOE and others engaged in solving complex environmental and waste management problems to find solutions that are stakeholder engaged and cost effective. This approach represents a paradigm shift that was introduced in a series of papers and a panel session at the WM2015 Symposium. The advantages of structured decision making over less formal approaches to decision making include technical defensibility, traceability and transparency. Structured decision making also overcomes the limitations of misapplication of conservatism in modeling, addresses stakeholder concerns and competing objectives directly, and provides a formal method through which internal and external stakeholders are encouraged to collectively and carefully consider all relevant attributes of solving complex problems. The first requirement of this paradigm shift is a realization and recognition that the problems faced are inherently decision problems, and that there is a formal theory of decision analysis that can, and should, be used to support finding the best solutions. Structured decision making is, very simply, formalized common sense. The formalities include: framing the problem; identification of objectives and measures for valuing those objectives; costs or values associated with those objectives; management options or alternatives for taking action that are tied directly to the objectives; and, science-based models to evaluate the options. Decision analysis is used to evaluate objectives and choose management options by balancing probability and consequence. The science-based models are built probabilistically based on expectation and uncertainty, and costs and value judgments are used to fulfill addressing stakeholder concerns. Consequently, this approach avoids misplaced conservatism in science-based modeling and properly places values in the objectives component of a decision model. This approach honestly addresses uncertainty and value judgments and balances these competing components to find the most effective decision. A software framework program called Guided Interactive Statistical Decision Tools (GiSdT - pronounced 'gist') is used to support an application of this paradigm shift towards structured decision making. In this application objectives and management options for a waste disposal problem at the Los Alamos National Laboratory are identified, and features, events and processes are described and defined to form the basis of a conceptual site model. This establishes the decision model structure. Objectives are addressed through the three pillars of sustainability - economic, environmental, and social - and also address regulatory concerns or constraints. Management options include removal of waste to another location and engineering designs for leaving waste in place. Using structured decision making, the relationship between objectives, management options, and the conceptual site model is made clear, and leads to a comprehensive, defensible, transparent and traceable approach to effective decision making. (authors)

12 MANAGEMENT OF RADIOACTIVE AND NON-RADIOACTIVE W↗
DOE OSTI2025

Towards Automated Reasoning Chains for Verification of LLM-Generated Scientific Code

With the rise of Large Language Model (LLM) generated code, including in domains like scientific computing, ensuring not only syntactical, but also mathematical correctness, has become a critical task. Traditional formal methods approaches often struggle with the ambiguity of floating-point code, and full symbolic execution is extremely costly and limited. We propose a chain-of-reasoning approach that iteratively lifts basic semantics from code into the SPIRAL system and then establishes numerical equivalency to the desired mathematical operation. Here, we leverage the ample mathematical knowledge already formalized in SPIRAL to enable the system to recognize not just different implementations of the same algorithm but fully separate approaches to solving the given problem. The chain establishes tight error bounds on the output of given code with respect to the true continuous solution it approximates, quantifying all sources of error. We demonstrate this approach by establishing the correctness of a pseudospectral solver for a simple 1-dimensional Poisson problem.

Oschatz, Quentin [Carnegie Mellon University,Pitts↗
DOE OSTI2016

A combinatorial model for dentate gyrus sparse coding

The dentate gyrus forms a critical link between the entorhinal cortex and CA3 by providing a sparse version of the signal. Concurrent with this increase in sparsity, a widely accepted theory suggests the dentate gyrus performs pattern separation—similar inputs yield decorrelated outputs. Although an active region of study and theory, few logically rigorous arguments detail the dentate gyrus’s (DG) coding. We suggest a theoretically tractable, combinatorial model for this action. The model provides formal methods for a highly redundant, arbitrarily sparse, and decorrelated output signal.To explore the value of this model framework, we assess how suitable it is for two notable aspects of DG coding: how it can handle the highly structured grid cell representation in the input entorhinal cortex region and the presence of adult neurogenesis, which has been proposed to produce a heterogeneous code in the DG. We find tailoring the model to grid cell input yields expansion parameters consistent with the literature. In addition, the heterogeneous coding reflects activity gradation observed experimentally. Lastly, we connect this approach with more conventional binary threshold neural circuit models via a formal embedding.

60 APPLIED LIFE SCIENCES↗
DOE OSTI2024

Results of an interlaboratory study on the working curve in vat photopolymerization

The working curve informs resin properties and print parameters for stereolithography, digital light processing, and other photopolymer additive manufacturing (PAM) technologies. First demonstrated in 1992, the working curve measurement of cure depth vs radiant exposure of light is now a foundational measurement in the field of PAM. Despite its widespread use in industry and academia, there is no formal method or procedure for performing the working curve measurement, raising questions about the utility of reported working curve parameters. Here, an interlaboratory study (ILS) is described in which 24 individual laboratories performed a working curve measurement on an aliquot from a single batch of PAM resin. The ILS reveals that there is enormous scatter in the working curve data and the key fit parameters derived from it. Further, the measured depth of light penetration D p varied by as much as 7x between participants, while the critical radiant exposure for gelation E c varied by as much as 70x. This significant scatter is attributed to a lack of common procedure, variation in light engines, epistemic uncertainties from the Jacobs equation, and the use of measurement tools with insufficient precision. The ILS findings highlight an urgent need for procedural standardization and better hardware characterization in this rapidly growing field.

36 MATERIALS SCIENCE↗
DOE OSTI2018

Optimal subhourly electricity resource dispatch under multiple price signals with high renewable generation availability

This article proposes a system-wide optimal resource dispatch strategy that enables a shift from a primarily energy cost-based approach, to a strategy using simultaneous price signals for energy, power and ramping behavior. A formal method to compute the optimal sub-hourly power trajectory is derived for a system when the price of energy and ramping are both significant. Optimal control functions are obtained in both time and frequency domains, and a discrete-time solution suitable for periodic feedback control systems is presented. The method is applied to North America Western Interconnection for the planning year 2024, and it is shown that an optimal dispatch strategy that simultaneously considers both the cost of energy and the cost of ramping leads to significant cost savings in systems with high levels of renewable generation: the savings exceed 25% of the total system operating cost for a 50% renewables scenario.

29 ENERGY PLANNING, POLICY, AND ECONOMY↗
DOE OSTI2025

Inference of phase field fracture models

The phase field approach to modeling fracture uses a diffuse damage field to represent cracks. This representation mollifies singularities that arise in computations with sharp interface models and some of the resultant difficulties in the mathematical and numerical treatment of fracture. Phase field fracture models have proven effective at representing crack propagation, branching, and merging. Specific formulations, beginning with brittle fracture, have also been shown to converge to classical solutions. Extensions to cover the range of material failure, including ductile and cohesive fracture, lead to an array of possible models. There exists a large body of literature focusing on this class of models and on the impact of model form on the predicted crack evolution. However, there have not been systematic studies into how optimal models may be chosen. Here, we take a first step in this direction by developing formal methods for identification of the best parsimonious model of phase field fracture given full-field data on the damage and deformation fields. We consider some of the main models that have been used for the degradation of elastic response due to damage and its propagation. Our approach builds upon Variational System Identification (VSI), a weak form variant of the Sparse Identification of Nonlinear Dynamics (SINDy). Furthermore, in this first communication we focus on synthetically generated data but we also consider central issues associated with the use of experimental full-field data, such as data sparsity and noise.

71 CLASSICAL AND QUANTUM MECHANICS, GENERAL PHYSIC↗
DOE OSTI2019

A Framework for Quantifying Energy and Productivity Benefits of Smart Manufacturing Technologies

The transformative possibilities of smart manufacturing, which is defined by digitization, enhanced connectivity, advanced analytics, and integrated cyber-physical systems in manufacturing processes and systems, have been extensively discussed in the literature. Potential benefits underscored include cost reduction, production flexibility, shorter product times-to-market, energy efficiency, environmental impact reduction, and increased productivity. Scant attention has been given to formal methods for quantifying and analyzing energy productivity to aid a broad range of manufacturing industries in evaluating the merits of adoption. Here we present a strategic analysis framework to estimate cost-effective improvements in energy efficiency and productivity that may be realized through smart manufacturing. The framework uses the cost of conserving energy (CCE) as a complementary measure to determine the feasibility of a set of smart manufacturing interventions in the context of a specific factory, firm, or entire industry. Guided by a function-driven approach based on key performance indicators, the CCE measure accounts for system-wide changes in direct and indirect costs and total energy use relative to the same manufacturing system without smart manufacturing interventions. These changes include cost of cyber-physical systems, which include components such as sensors, controllers, smart equipment, and information and communication technology (ICT) equipment. Additionally, cost and savings are accounted from changes in primary and intermediate inputs, production time, off-spec production, and waste. Energy calculations include upstream energy use of the cyber-physical systems. For complex processes with significant circularity and/or feedbacks, we propose the use of input-output models to characterize elements of the CCE. The framework is discussed in the context of recent efforts in craft breweries to use smart manufacturing for reducing energy intensity and increasing product yield.

Supekar, Sarang D.↗
DOE OSTI2021

Evaluation of Force Fields for Molecular Dynamics Simulations of Platinum in Bulk and Nanoparticle Forms

Here, understanding the size- and shape-dependent properties of platinum nanoparticles is critical for enabling the design of nanoparticle-based applications with optimal and potentially tunable functionality. Toward this goal, we evaluated nine different empirical potentials with the purpose of accurately modeling faceted platinum nanoparticles using molecular dynamics simulation. First, the potentials were evaluated by computing bulk and surface properties - surface energy, lattice constant, stiffness constants, and the equation of state - and comparing these to prior experimental measurements and quantum mechanics calculations. Then, the potentials were assessed in terms of the stability of cubic and icosahedral nanoparticles with faces in the {100} and {111} planes, respectively. Although none of the force fields predicts all the evaluated properties with perfect accuracy, one potential - the embedded atom method formalism with a specific parameter set - was identified as best able to model platinum in both bulk and nanoparticle forms.

37 INORGANIC, ORGANIC, PHYSICAL, AND ANALYTICAL CH↗
DOE OSTI2015

Surface defects characterization in a quantum wire by coherent phonons scattering

The influence of surface defects on the scattering properties of elastic waves in a quasi-planar crystallographic waveguide is studied in the harmonic approximation using the matching method formalism. The structural model is based on three infinite atomic chains forming a perfect lattice surmounted by an atomic surface defect. Following the Landauer approach, we solve directly the Newton dynamical equation with scattering boundary conditions and taking into account the next nearest neighbour’s interaction. A detailed study of the defect-induced fluctuations in the transmission spectra is presented for different adatom masses. As in the electronic case, the presence of localized defect-induced states leads to Fano-like resonances. In the language of mechanical vibrations, these are called continuum resonances. Numerical results reveal the intimate relation between transmission spectra and localized defect states and provide a basis for the understanding of conductance spectroscopy experiments in disordered mesoscopic systems. The results could be useful for the design of phononic devices.

71 CLASSICAL AND QUANTUM MECHANICS, GENERAL PHYSIC↗
DOE OSTI2022

Quantitative assessment of fitting errors associated with streak camera noise in Thomson scattering data analysis

Thomson scattering measurements in high energy density experiments are often recorded using optical streak cameras. In the low-signal regime, noise introduced by the streak camera can become an important and sometimes the dominant source of measurement uncertainty. In this paper, we present a formal method of accounting for the presence of streak camera noise in our measurements. We present a phenomenological description of the noise generation mechanisms and present a statistical model that may be used to construct the covariance matrix associated with a given measurement. This model is benchmarked against simulations of streak camera images. We demonstrate how this covariance may then be used to weight fitting of the data and provide quantitative assessments of the uncertainty in the fitting parameters determined by the best fit to the data and build confidence in the ability to make statistically significant measurements in the low-signal regime, where spatial correlations in the noise become apparent. These methods will have general applicability to other measurements made using optical streak cameras.

47 OTHER INSTRUMENTATION↗
DOE OSTI2025

Using the optimal combined index weight ratio to improve the probability of anomaly detection in big area additive manufacturing

Big Area Additive Manufacturing (BAAM) of composites requires significant time, energy, and material, so it is critical to reduce production inefficiencies to make functional parts without multiple iterations. Statistical process control coupled with Principal Component Analysis (PCA) is a powerful technique that provides a quick, computationally inexpensive, and intuitive way for operators to detect defects that form in a manufacturing process without massive datasets. Recently, a combined index that is a weighted sum of the Hotelling's T 2 and squared residual error statistics has been proposed that can be monitored in one chart, improving interpretation accuracy and simplicity. However, the literature does not offer a formal method to optimise the weights. Here, we introduce two new approaches to the traditional weight selection approach using simulated and BAAM image data. Approach 1 uses a theoretically motivated optimum inspired by probabilistic principal component analysis. Approach 2 systematically varies the ratio of the weights to find the optimum. We show that approach 1 delivers optimal anomaly detection performance in select cases while approach 2 fares better in practice. Surprisingly, we also show that choosing a more complex PCA model has a minimal negative impact on anomaly detection performance compared to a more simplistic model.

3-dimensional printing↗
DOE OSTI2018

ScienceSearch: Enabling Search through Automatic Metadata Generation

© 2018 IEEE. Scientific facilities are increasingly generating and handling large amounts of data from experiments and simulations. Next-generation scientific discoveries rely on insights derived from data, especially across domain boundaries. Search capabilities are critical to enable scientists to discover datasets of interest. However, scientific datasets often lack the signals or metadata required for effective searches. Thus, we need formalized methods and systems to automatically annotate scientific datasets from the data and its surrounding context. Additionally, a search infrastructure needs to account for the scale and rate of application data volumes. In this paper, we present ScienceSearch, a system infrastructure that uses machine learning techniques to capture and learn the knowledge, context, and surrounding artifacts from data to generate metadata and enable search. Our current implementation is focused on a dataset from the National Center for Electron Microscopy (NCEM), an electron microscopy facility at Lawrence Berkeley National Laboratory sponsored by the Department of Energy which supports hundreds of users and stores millions of micrographs. In this paper, we describe a) our search infrastructure and model, b) methods for generating metadata using machine learning techniques, and c) optimizations to improve search latency, and deployment on an HPC system. We demonstrate that ScienceSearch is capable of producing valid metadata for NCEM's dataset and providing low-latency good quality search results over a scientific dataset.

Rodrigo, Gonzalo P.↗
DOE OSTI2017

Big Data Sanitization and Cyber Situational Awareness: A Network Telescope Perspective

This paper addresses the problems of data sanitization and cyber situational awareness by analyzing 910 GB of real Internet-scale traffic, which has been passively collected by monitoring close to 16.5 million darknet IP addresses from a /8 and a /13 network telescopes. First, the paper offers a novel probabilistic darknet preprocessing model, which aims at sanitizing darknet data to prepare it for effective use in the task of cyber threat intelligence generation. Such model has been engineered using a distributed multithreaded approach, rendering it highly effective on darknet big data. Second, the paper further contributes by presenting an innovative approach to infer large-scale orchestrated probing campaigns by leveraging darknet data, for Internet cyber situational awareness. The approach uniquely reduces the dimensionality of such big data by utilizing its artifacts, instead of processing the actual raw data. This is accomplished by extracting and analyzing probing time series using formal methods rooted in Fourier transform and Kalman filtering. Thorough empirical evaluations indeed validate the accuracy and the performance of the proposed methods. We assert that such approaches are of significant value, given their highly applicable nature to the field of Internet measurements for cyber security in the era of big data.

Bou-Harb, Elias↗
DOE OSTI2025

AR4IR (Automated Reasoning for Incident Response) [SWR-24-103]

A basic formal methods tool with the ability to aid and/or automate a utilities’ incidence response and instills confidence that the proposed action satisfies the system’s physical constraints, the organization’s cyber policies, and will not cause violations of technical standards.

Etigowni, Sriharsha [National Renewable Energy Lab↗