Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “verifications”

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 181 records · Page 10

Code and Solution Verification Assessment of the CTF Thermal Hydraulic Subchannel Code

CTF is a thermal-hydraulics subchannel code jointly developed by Oak Ridge National Laboratory and North Carolina State University. Over the past seven years, the Consortium for Advanced Simulation of Light Water Reactors (CASL) has made a significant investment in developing CTF so it can be used to model light water reactors, including nominal operating conditions, departure from nucleate boiling analysis, and transients ranging from loss of flow to reactivity insertion accidents. In addition to implementing new modeling capabilities and developing the user input and output interface, extensive work has been performed to improve the code’s quality assurance program, resulting in a development process that conforms with NQA-1 requirements. The CASL program follows the Predictive Capability Maturity Model (PCMM) approach for assessing code quality, which emphasizes performing code verification(ensuring the code converges to the correct answer) and solution verification (ensuring the code converges for the intended application). Code and solution verification are used to identify uncertainty errors introduced by numerical approximations in the code and are important for demonstrating that the model is coded without error, which is an important aspect of the Best Estimate plus Uncertainty method. This paper presents a comprehensive overview of the code and solution verification testing that has been performed on CTF. A top-down approach is taken in which the intended CTF applications are presented, followed by the code features required for their modeling. These features are then linked to the applicable code and solution verification tests that demonstrate proper functioning. Past testing efforts are summarized, and new tests are added to help close gaps in the presented test matrix. Rather than performing “one-off” exercises, these tests are added to the automated CTF regression test suite to ensure continual code quality.

21 SPECIFIC NUCLEAR REACTORS AND ASSOCIATED PLANTS↗

Verification and Validation of the PLTEMP/ANL Code for Thermal-Hydraulic Analysis of Experimental and Test Reactors (Code Version 4.3)

The document compiles in a single volume the verification and validation works done for the PLTEMP/ANL code during the years of its development and improvement. The verification of sixteen capabilities of the PLTEMP/ANL Version 4.3 code that were identified by research reactor analysts as frequently used in their thermal-hydraulic analysis are described and documented. Each chapter of the document deals with the verification or validation of a specific part of the software that calculates a specific phenomenon, e.g., channel flow calculation, coolant property calculation, heat transfer calculation, and flow instability calculation. The software verification work is usually done by comparing the code with hand calculation, Microsoft spreadsheet calculation, or Mathematica calculation. The software validation is done by comparing the code with experimental data or a widely tested code like the RELAP5 code. In addition, some PLTEMP/ANL verification works that are available in the open literature are simply referenced and not included in the document. PLTEMP/ANL has been used in conversion safety analysis reports of several US and foreign research reactors that have been licensed and converted. A list of such reactors is given.

22 GENERAL STUDIES OF NUCLEAR REACTORS↗

Verification Testing For Solid-Element Material Models 11-19 in DYNA3D/ParaDyn

This technical report documents the creation and implementation of verification tests for solid-element material models 11 through 19 available in DYNA3D/ParaDyn. The verification tests covered all aspects of each material model, except for the Weibull distribution functionality in material models 15 and 19. General test cases were created to verify the elastic and plastic behavior of the material models. Other additional tests were developed to examine the intricacies of each material model. Each test involved the use a kinematic load case and specification of material parameters necessary to activate corresponding features of the material model. The load cases prescribed the full time history of the kinematic motion for the solid elements, and these loads are independent of the material model or element formulation. When possible, closed form solutions were then derived for each verification test in a continuum setting. The DYNA3D simulations for each test were carried out over a unit time interval, t ϵ [0, 1], and the as implemented DYNA3D response was compared to the closed form solutions evaluated at discrete points in time. A relative error measure was determined for each test to justify the proper implementation of the material model. The relative errors comparing the DYNA3D solution to the analytical solution were, in general, on the order of machine precision except where noted. This signifies the proper implementation of solid-element material models 11-19. In the development of these verification tests, six bugs were found and fixed in the source code. Additionally, this work generated eighteen DYNA3D input decks and answer extraction scripts in the DYNA3D/ParaDyn Software Quality Assurance test suite, which are comprised of a total of 285 solid-element tests. Testing for each material model utilizes two input decks and answer extraction scripts, where one focuses on the linear elastic response and the other examines the inelastic and remaining functionalities of the material model. In total, this work added 285 individual verification test problems in the DYNA3D/ParaDyn test suite.

42 ENGINEERING↗

Verification Testing of OLI Systems Mixed Solvent Electrolyte Model for the Na-K-Mg-Ca-H-Cl-SO 4 -OH-HCO 3 -CO 3 -CO 2 -H 2 ) System to High Ionic Strength at 25°C

This technical report summarizes model verification results and summary statistics for 41 evaporite mineral solubility cases evaluated by Savannah River National Laboratory using OLI Systems’ aqueous electrolyte thermodynamic modeling software. The 41 verification cases containing a total of 60 solubility curves comprise mineral solubility data from low to high ionic strength at 25°C for the eight-component system Na-K-Mg-Ca-H-Cl-SO 4 -OH-HCO 3 -CO 3 -CO 2 -H 2 O as reported by Harvie et al. (1984). Thermodynamic calculations were executed using OLI Systems’ Stream Analyzer computation module within the OLI Studio software platform (Ver. 11.0, Rev. 11.0.1.9). The Mixed Solvent Electrolyte (MSE) thermodynamic framework was chosen for this investigation because of its superiority in modeling high ionic-strength inorganic salt solutions and actinide redox chemistry and solubility, both of which are relevant to the geological repository conditions at the Waste Isolation Pilot Plant in Carlsbad, New Mexico. Mineral solubility data in various inorganic salt solutions were digitized and extracted from figures generated by Harvie et al. (1984). For each of the 60 solubility curves, a case-specific chemistry model and input file were generated in OLI Studio using OLI Stream Analyzer and the MSE (H 3 O + ion) public databank provided by OLI Systems. Model simulation results were exported to Microsoft Excel to calculate summary statistics and to generate graphs comparing the OLI model predictions to the solubility data. Summary statistics include residuals (model – data) and concordance (accuracy × precision, where precision is indicated by the Pearson correlation coefficient and accuracy accounts for bias and scale differential). Private databanks were not developed, and activity coefficient model regressions were not performed to improve OLI model fits to the data. Of the 41 model verification plots, 83% have a mean of the percent residuals less than or equal to 25%. Similarly, 75% display a concordance greater than or equal to 0.75. Only seven of the 41 verification plots fail to show good agreement between the model and data. Of these seven, three are relevant to the WIPP repository because they involve the Mg-OH-Cl-SO 4 -CO 3 aqueous system. The remaining four address salt solubilities at the pH extremes (strong acid and strong base). It should be noted that in two of the three Mg-OH-Cl-SO 4 -CO 3 system cases, the regressed Harvie et al. (1984) solubility curve also deviated from the data. Lack of agreement between the OLI model-predicted solubility curves and the data is attributable to one or more of the following: specific solid species are not included in the OLI MSE databank; there is significant variation among the different solubility datasets chosen by Harvie et al. (1984); the OLI MSE model’s thermodynamic parameters were determined using different solubility datasets; and the activity coefficient parameters for certain relevant ion-ion and ion-molecule pairs have not been optimized via data regression. Two recommendations for future work are to (1) evaluate solubility data for the Mg-OH-Cl-SO 4 -CO 3 system at high ionic strength and, if necessary, develop a private OLI MSE database that includes missing species and, where necessary, regressed standard state properties and interaction parameters; (2) perform similar verification testing of the OLI model for actinide solubility data.

12 MANAGEMENT OF RADIOACTIVE AND NON-RADIOACTIVE W↗

Gamma Source Verification for GAMSRC and GAMSOR

Nuclear reactors that rely upon the fission reaction have two modes of thermal energy deposition in the reactor system: neutron absorption and gamma absorption. The gamma rays are typically generated by neutron capture reactions or during the fission process which means the primary driver of energy production is of course the neutron interactions. The GAMSOR program was first built in the mid 1980s to properly account for the gamma heating in an operating reactor core on core internals. The GAMSOR code is sequence of DIF3D calculations to compute the neutron and gamma flux and combine them to define both the neutron and gamma heating throughout the modeled domain. The goal of this manuscript is to present the software verification of GAMSOR. The first step of the GAMSOR sequence of calculations involves of a modified version of DIF3D (called DIF3D-GAMSOR) which generates a gamma source distribution for the follow-on DIF3D gamma transport calculation (step 2). This modified version of DIF3D increases the burden of maintenance and verification work on GAMSOR as one must reverify the DIF3D capabilities which is undesirable. Because the calculation of the gamma source is the only unique aspect of GAMSOR beyond the regular DIF3D capabilities, that part was put in a standalone code called GAMSRC such that one can use the verified DIF3D code in step 1 followed by GAMSRC to carry out the same GAMSOR calculation step. As a consequence, this manuscript is focused on verification of the gamma source files generated by GAMSRC. The verification of the modified version of DIF3D (DIF3D-GAMSOR) will be done less rigorously in that it will be verified that it produces the same output that GAMSRC does and thus GAMSRC is equivalent to GAMSOR on the problems studied here. Hand calculations and independent numerical calculations of the gamma source generation are used for the verification work. This work follows the same methodology of GAMSRC. As expected, the results agree well with those calculated by GAMSRC as will be shown.

22 GENERAL STUDIES OF NUCLEAR REACTORS↗

Verification and Benchmarking of High Fidelity Physics Peat Smoldering Model

Peat fires are a major contributor to greenhouse gas emissions. The estimates of these emissions currently contain major uncertainties, due to the difficulty of determining the mass of peat burned in a fire. To address these uncertainties, we develop a computational physics-based peat smoldering model, which will be leveraged for high-fidelity quantitative estimates of peat fire emissions relevant to climate change. We present the verification of the 2-D axisymmetric model, a first step towards developing a full 3-D model. Verification includes the solution verification against a literature model for the 0-D smoldering case and verification of the heat transfer problem in 1-D and 2-D. Also presented is the effect of reaction mechanism on the smoldering model, for which we found a relatively simple three-step reaction mechanism is able to capture key behavior. These verification results provide the foundation for moving forward with validation against experimental data of the 2-D model.

71 CLASSICAL AND QUANTUM MECHANICS, GENERAL PHYSIC↗

Multi-Rigor Agile Verification and Rapid Prototyping for Formally Verified Software

We propose a novel approach to developing formally verified systems through Multi-rigor Agile Verification. Multi-rigor Agile Verification is rooted in the hypothesis of Rigor Independence, that a system’s specification and verification architecture depend primarily on the system requirements to be verified, and they depend very little on the rigor level of the methods used to verify those requirements. Due to its iterative nature, Multi-rigor Agile Verification promises to mitigate many of the high upfront design costs experienced by formally verified systems and to deliver a better-architected, and thus better-trusted, system in the end. We then discuss the tooling needed to perform Multi-rigor Agile Verification and go in depth to build one of those tools, which directly generates executable prototype code from declarative formal specifications using the Maude rewrite-logic framework.

97 MATHEMATICS AND COMPUTING↗

Gamma Source Verification for GAMSRC and GAMSOR

Nuclear reactors that rely upon the fission reaction have two modes of thermal energy deposition in the reactor system: neutron absorption and gamma absorption. The gamma rays are typically generated by neutron capture reactions or during the fission process which means the primary driver of energy production is of course the neutron interactions. The GAMSOR program was first built in the mid 1980s to properly account for the gamma heating in an operating reactor core on core internals. The GAMSOR code is sequence of DIF3D calculations to compute the neutron and gamma flux and combine them to define both the neutron and gamma heating throughout the modeled domain. The goal of this manuscript is to present the software verification of GAMSOR. The first step of the GAMSOR sequence of calculations involves of a modified version of DIF3D (called DIF3D-GAMSOR) which generates a gamma source distribution for the follow-on DIF3D gamma transport calculation (step 2). This modified version of DIF3D increases the burden of maintenance and verification work on GAMSOR as one must reverify the DIF3D capabilities which is undesirable. Because the calculation of the gamma source is the only unique aspect of GAMSOR beyond the regular DIF3D capabilities, that part was put in a standalone code called GAMSRC such that one can use the verified DIF3D code in step 1 followed by GAMSRC to carry out the same GAMSOR calculation step. As a consequence, this manuscript is focused on verification of the gamma source files generated by GAMSRC. The verification of the modified version of DIF3D (DIF3D-GAMSOR) will be done less rigorously in that it will be verified that it produces the same output that GAMSRC does and thus GAMSRC is equivalent to GAMSOR on the problems studied here. Hand calculations and independent numerical calculations of the gamma source generation are used for the verification work. This work follows the same methodology of GAMSRC. As expected, the results agree well with those calculated by GAMSRC as will be shown.

22 GENERAL STUDIES OF NUCLEAR REACTORS↗

FY20 Improvements to CTF Code Verification and Unit Testing

In 2010, the U.S. Department of Energy created its first Energy Innovation Hub, which focuses on improving Light Water Reactors (LWRs) through Modeling and Simulation. This hub, named the Consortium for the Advanced Simulation of LWRs (CASL), attempts to characterize and understand LWR behavior under normal operating conditions and use any gained insights to improve their efficiency. In collaboration with North Carolina State University (NCSU), CASL has worked extensively on the thermal-hydraulic subchannel code Coolant Boiling in Rod Arrays–Three Field (COBRA-TF). The NCSU/CASL version of COBRA-TF has been rebranded as CTF. This document focuses on code verification test problems that ensure CTF converges to the correct answer for the intended application. The suite of code verification tests are mapped to the underlying conservation equations of CTF, and significant gaps are addressed. Convergence behavior and numerical errors are quantified for each of the tests. Tests that converge at the correct rate to the corresponding analytic solution are incorporated into the CTF automated regression suite. A new verification utility is created for this purpose, which enables code verification by generalizing the process. For problems that do not behave correctly, the results are reported but the problem is not included in the regression suite. In addition to verification studies, this document also quantifies the existing tests of constitutive models. A few existing gaps are addressed by adding new unit tests.

22 GENERAL STUDIES OF NUCLEAR REACTORS↗

MPACT Verification and Validation Manual (rev 6)

The MPACT code provides the capability to calculate the steady-state and transient reactor core neutron distribution for operating nuclear power plant (PWR) conditions across multiple fuel cycles. As required in the CASL SQA plan, it is the responsibility of UM and ORNL as joint owners of MPACT to ensure that verification and validation activities are performed and documented in a V&V manual with supporting publications and CASL technical reports which can be distributed for reference and distribution within VERA. This document provides the fifth revision of the MPACT verification and validation (V&V) manual and describes the current state of MPACT V&V and updates the framework for future MPACT V&V activities. During FY19 MPACT V&V activities in the areas of code / solution verification and code validation have continued to mature. Several specific tasks have also been completed to include the Ganapol and IPEN Benchmarks which have provided significant improvements in MPACT verification and validation, respectively. Based on the results of V&V efforts this past year, the confidence level has increased in the ability of MPACT to model an operational Pressurized Water Reactor. Specific areas in both verification and validation were identified which require increased emphasis during FY20.

22 GENERAL STUDIES OF NUCLEAR REACTORS↗

Space transportation system payload interface verification

The paper considers STS payload-interface verification requirements and the capability provided by STS to support verification. The intent is to standardize as many interfaces as possible, not only through the design, development, test and evaluation (DDT and E) phase of the major payload carriers but also into the operational phase. The verification process is discussed in terms of its various elements, such as the Space Shuttle DDT and E (including the orbital flight test program) and the major payload carriers DDT and E (including the first flights). Five tools derived from the Space Shuttle DDT and E are available to support the verification process: mathematical (structural and thermal) models, the Shuttle Avionics Integration Laboratory, the Shuttle Manipulator Development Facility, and interface-verification equipment (cargo-integration test equipment).

Everline, R. T.↗

Hierarchical Design and Verification for VLSI

The specification and verification work is described in detail, and some of the problems and issues to be resolved in their application to Very Large Scale Integration VLSI systems are examined. The hierarchical design methodologies enable a system architect or design team to decompose a complex design into a formal hierarchy of levels of abstraction. The first step inprogram verification is tree formation. The next step after tree formation is the generation from the trees of the verification conditions themselves. The approach taken here is similar in spirit to the corresponding step in program verification but requires modeling of the semantics of circuit elements rather than program statements. The last step is that of proving the verification conditions using a mechanical theorem-prover.

Shostak, R. E.↗

Multibody modeling and verification

A summary of a ten week project on flexible multibody modeling, verification and control is presented. Emphasis was on the need for experimental verification. A literature survey was conducted for gathering information on the existence of experimental work related to flexible multibody systems. The first portion of the assigned task encompassed the modeling aspects of flexible multibodies that can undergo large angular displacements. Research in the area of modeling aspects were also surveyed, with special attention given to the component mode approach. Resulting from this is a research plan on various modeling aspects to be investigated over the next year. The relationship between the large angular displacements, boundary conditions, mode selection, and system modes is of particular interest. The other portion of the assigned task was the generation of a test plan for experimental verification of analytical and/or computer analysis techniques used for flexible multibody systems. Based on current and expected frequency ranges of flexible multibody systems to be used in space applications, an initial test article was selected and designed. A preliminary TREETOPS computer analysis was run to ensure frequency content in the low frequency range, 0.1 to 50 Hz. The initial specifications of experimental measurement and instrumentation components were also generated. Resulting from this effort is the initial multi-phase plan for a Ground Test Facility of Flexible Multibody Systems for Modeling Verification and Control. The plan focusses on the Multibody Modeling and Verification (MMV) Laboratory. General requirements of the Unobtrusive Sensor and Effector (USE) and the Robot Enhancement (RE) laboratories were considered during the laboratory development.

Wiens, Gloria J.↗

Formal verification of an oral messages algorithm for interactive consistency

The formal specification and verification of an algorithm for Interactive Consistency based on the Oral Messages algorithm for Byzantine Agreement is described. We compare our treatment with that of Bevier and Young, who presented a formal specification and verification for a very similar algorithm. Unlike Bevier and Young, who observed that 'the invariant maintained in the recursive subcases of the algorithm is significantly more complicated than is suggested by the published proof' and who found its formal verification 'a fairly difficult exercise in mechanical theorem proving,' our treatment is very close to the previously published analysis of the algorithm, and our formal specification and verification are straightforward. This example illustrates how delicate choices in the formulation of the problem can have significant impact on the readability of its formal specification and on the tractability of its formal verification.

Rushby, John↗

Towards the formal verification of the requirements and design of a processor interface unit: HOL listings

This technical report contains the Higher-Order Logic (HOL) listings of the partial verification of the requirements and design for a commercially developed processor interface unit (PIU). The PIU is an interface chip performing memory interface, bus interface, and additional support services for a commercial microprocessor within a fault tolerant computer system. This system, the Fault Tolerant Embedded Processor (FTEP), is targeted towards applications in avionics and space requiring extremely high levels of mission reliability, extended maintenance-free operation, or both. This report contains the actual HOL listings of the PIU verification as it currently exists. Section two of this report contains general-purpose HOL theories and definitions that support the PIU verification. These include arithmetic theories dealing with inequalities and associativity, and a collection of tactics used in the PIU proofs. Section three contains the HOL listings for the completed PIU design verification. Section 4 contains the HOL listings for the partial requirements verification of the P-Port.

Fura, David A.↗

Evaluation of HCFC AK 225 Alternatives for Precision Cleaning and Verification

Maintaining qualified cleaning and verification processes are essential in an production environment. Environmental regulations have and are continuing to impact cleaning and verification processing in component and large structures, both at the Michoud Assembly Facility and component suppliers. The goal of the effort was to assure that the cleaning and verification proceeds unimpeded and that qualified, environmentally compliant material and process replacements are implemented and perform to specifications. The approach consisted of (1) selection of a Supersonic Gas-Liquid Cleaning System; (2) selection and evaluation of three cleaning and verification solvents as candidate alternatives to HCFC 225 (Vertrel 423 (HCFC), Vertrel MCA (HFC/1,2-Dichloroethylene), and HFE 7100DE (HFE/1,2 Dichloroethylene)); and evaluation of an analytical instrumental post cleaning verification technique. This document is presented in viewgraph format.

Melton, D. M.↗

Improved Detection Technique for Solvent Rinse Cleanliness Verification

The NASA White Sands Test Facility (WSTF) has an ongoing effort to reduce or eliminate usage of cleaning solvents such as CFC-113 and its replacements. These solvents are used in the final clean and cleanliness verification processes for flight and ground support hardware, especially for oxygen systems where organic contaminants can pose an ignition hazard. For the final cleanliness verification in the standard process, the equivalent of one square foot of surface area of parts is rinsed with the solvent, and the final 100 mL of the rinse is captured. The amount of nonvolatile residue (NVR) in the solvent is determined by weight after the evaporation of the solvent. An improved process of sampling this rinse, developed at WSTF, requires evaporation of less than 2 mL of the solvent to make the cleanliness verification. Small amounts of the solvent are evaporated in a clean stainless steel cup, and the cleanliness of the stainless steel cup is measured using a commercially available surface quality monitor. The effectiveness of this new cleanliness verification technique was compared to the accepted NVR sampling procedures. Testing with known contaminants in solution, such as hydraulic fluid, fluorinated lubricants, and cutting and lubricating oils, was performed to establish a correlation between amount in solution and the process response. This report presents the approach and results and discusses the issues in establishing the surface quality monitor-based cleanliness verification.

Hornung, S. D.↗

Towards a Theory for Integration of Mathematical Verification and Empirical Testing

From the viewpoint of a project manager responsible for the V&V (verification and validation) of a software system, mathematical verification techniques provide a possibly useful orthogonal dimension to otherwise standard empirical testing. However, the value they add to an empirical testing regime both in terms of coverage and in fault detection has been difficult to quantify. Furthermore, potential cost savings from replacing testing with mathematical verification techniques cannot be realized until the tradeoffs and synergies can be formulated. Integration of formal verification with empirical testing is also difficult because the idealized view of mathematical verification providing a correctness proof with total coverage is unrealistic and does not reflect the limitations imposed by computational complexity of mathematical techniques. This paper first describes a framework based on software reliability and formalized fault models for a theory of software design fault detection - and hence the utility of various tools for debugging. It then describes a utility model for integrating mathematical and empirical techniques with respect to fault detection and coverage analysis. It then considers the optimal combination of black-box testing, white-box (structural) testing, and formal methods in V&V of a software system. Using case studies from NASA software systems, it then demonstrates how this utility model can be used in practice.

Lowry, Michael↗