Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Criticality Safety”

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 667 records · Page 37
All sourcesNASA NTRSDOE OSTI
DOE OSTI2021

On the Feynman-alpha method for reflected fissile assemblies

The Feynman-alpha method is a neutron noise technique that is used to estimate the prompt neutron period of fissile assemblies. The method and quantity are of widespread interest including in applications such as nuclear criticality safety, safeguards and nonproliferation, and stockpile stewardship; the prompt neutron period may also be used to infer the k eff multiplication factor. The Feynman-alpha method is predicated on time-correlated neutron detections that deviate from a Poisson random variable due to multiplication. Traditionally, such measurements are diagnosed with one-region point kinetics, but two-region models are required when the fissile assembly is reflected. This paper presents a derivation of the two-region point kinetics Feynman-alpha equations based on a double integration of the Rossi-alpha equations, develops novel propagation of measurement uncertainty, and validates the theory. Validation is achieved with organic scintillator measurements of weapons-grade plutonium reflected by various amounts of copper to achieve k eff values of 0.83–0.94 and prompt periods of 5–75 ns. The results demonstrate that Feynman-alpha measurements should use the two-region model instead of the one-region model. The simplified one-region model deviates from the validated two-region models by as much as 10% in the estimate of the prompt neutron period, and the two-region model reduces to the one-region model for small amounts of reflector. The Feynman-alpha estimates of the prompt neutron period are compared to those of the Rossi-alpha approach. The comparative results demonstrate that the Feynman-alpha method is more precise than the Rossi-alpha method and more accurate for k eff < 0.92, whereas the Rossi-alpha method is generally more accurate for higher multiplications. Here, the uncertainty propagation developed in this work should be used for all Feynman-alpha measurements and will therein improve fitting accuracy and appropriate precision estimates.

98 NUCLEAR DISARMAMENT, SAFEGUARDS, AND PHYSICAL P↗
DOE OSTI2023

The Case for and Against a Gadolinium Bias in SCALE: Round 2

The “Opening Arguments” for and against a gadolinium bias in SCALE were presented at the American Nuclear Society Annual Meeting in Philadelphia, Pennsylvania, in June, 2018. Some critical experiments included in the Oak Ridge National Laboratory Verified, Archived Library of Inputs and Data (VALID) indicate a significant bias as a function of gadolinium concentration. Other experiments indicate that no significant bias exists. The work presented here develops a larger suite of gadolinium-bearing benchmark models to further examine code, data, and benchmark performance. The new benchmark models have been reviewed for accuracy, but documentation and review for addition to the VALID library have not been completed. The problematic benchmarks included in VALID are HEU-SOL-THERM-014 and -016. These are two evaluations from a series of experiments from the Institute for Physics and Power Engineering (IPPE), Russia, documented in the International Criticality Safety Benchmark Evaluation Project (ICSBEP) Handbook. The entire set of evaluations also includes HEU-SOL-THERM-015, -017, -018, -019, and -025. Each evaluation contains a different uranium concentration, and different configurations within each evaluation include different gadolinium concentrations. These 7 evaluations contain a total of 52 configurations and form the largest subset of experiments considered, and they allow for a more complete assessment of the performance of these benchmarks than has historically been possible using just the HEU-SOL-THERM-014 and -016 results. Additional solution experiments are considered, including MIX-SOL-THERM-006 and -007 and PU-SOL-THERM-034. MIX-SOL-THERM-007 is in the VALID library, whereas MIX-SOL-THERM-006 and PU-SOL-THERM-034 are not. The results for MIX-SOL THERM-007 have not shown a gadolinium trend. These mixed- and plutonium-fueled solutions include 28 configurations. Some experiments including solid fuel and solid gadolinium are also included. These experiments include highly enriched uranium (HEU) foils moderated with polyethylene in HEU-MET-THERM-010, -016, and -034, and low enriched uranium (LEU) pin arrays with gadolinia absorber rods in LEU-COMP THERM-036 and -043. A total 32 cases with solid fuel are included. The IPPE solution benchmarks show a fairly high degree of variability, but no clear trend as a function of gadolinium concentration can be observed. The mixed- and plutonium-fueled solutions show less variability than the HEU solutions and also no trend relative to gadolinium concentration. The solid-fueled experiments also show no trend as a function of gadolinium content. The entire set of benchmarks shows no clear trend on gadolinium content or the energy of the average neutron lethargy causing fission.

11 NUCLEAR FUEL CYCLE AND FUEL MATERIALS↗
DOE OSTI2023

Lost and Found Opportunities Around the Chlorine Worth Study

Los Alamos National Laboratory performed a series of critical experiments in 2021 to examine the worth of chlorine in plutonium-fueled systems. This series of experiments has been dubbed the “Chlorine Worth Study,” and the evaluation of the experiments was presented to the International Criticality Safety Benchmark Evaluation Project (ICSBEP) Technical Review Group in April, 2023. The primary purpose of these experiments was to enable validation of aqueous solutions crediting neutron absorption in 35 Cl. An external, independent view of the events leading up to the design and execution of these experiments indicates a missed opportunity to leverage sensitivity/uncertainty (S/U) analysis to assert validation without the experiments by taking an additional margin for the lack of direct validation of chlorine. On the other hand, the execution of these experiments also presents a rare opportunity to examine the efficacy of the S/U approach and extract useful information about the evaluated chlorine covariance data. TSUNAMI-1D models of representative application solutions were created and used to generate sensitivity data. Varying plutonium and chlorine concentrations were considered to examine the impact of these differences on the chlorine sensitivities and uncertainties. The data-induced uncertainty in k eff resulting from chlorine was calculated directly from uncertainty information calculated in the TSUNAMI-1D sequence. In all cases, this uncertainty was less than 0.1 %Δk. This result could potentially be used to justify a reactivity margin to account for the validation gap related to chlorine in the validation set. On the other hand, given that the experiments were performed, the community should endeavor to extract as much value from them and their results as possible. The results can be used to examine the actual bias associated with chlorine in these systems once the evaluations have been released. These data can be compared with the data-induced uncertainty margin discussed above to test the sufficiency of the validation gap penalty. This result will provide an indication of the performance of the chlorine covariance data specifically and the S/U validation approach generally. More advanced S/U techniques may also be employed to determine reactivity sensitivities associated with the chlorine in the experiments, potentially generating a more robust test of the chlorine covariance data.

11 NUCLEAR FUEL CYCLE AND FUEL MATERIALS↗
DOE OSTI2020

Sulfur Pellets Responses to a Bare and Steel Reflected Pulse of the Oak Ridge National Laboratory Health Physics Research Reactor

The experiments analyzed in this report were conducted at the Health Physics Research Reactor (HPRR), also known as the $\textit{Fast Burst Reactor}$. The reactor was designed and built at Oak Ridge National Laboratory (ORNL) in 1961. The HPRR was an unmoderated, unshielded fast reactor that used highly enriched uranium and molybdenum alloy as fuel. The reactor was initially sent to the Nevada Test Site in 1962, where it was used to evaluate radiation doses received as a result of the Hiroshima and Nagasaki bombings during World War II. A few years later, the reactor was sent back to ORNL to be part of the Dosimetry Application Research (DOSAR) facility shown in Figure 1, which included a reactor building shown on the left (west) of the picture and a control and laboratory building in the upper right corner (northeast). The critical assembly was used for numerous technical studies, including systems calibration, dosimetry, radiobiology of plants and animals, testing of radiation alarms, as well as teaching and training in radiation dosimetry and nuclear engineering. Between 1963 and 1987, the HPRR was operated for thousands of hours, achieving criticality close to 10,000 times and motivating many publications. The HPRR was decommissioned in 1987. The goal of this effort was to use historical data from operation of the HPRR to create a criticality accident alarm system (CAAS) benchmark to be included in the $\textit{International Handbook of Evaluated Criticality Safety Benchmark Experiments}$ (ICSBEP Handbook). A thorough inspection was performed of all available documentation and information available. The most promising experiments that were selected for evaluation were those described in the 1987 ORNL report entitled $\textit{Health Physics Research Reactor Reference Dosimetry}$, ORNL-6240. The report includes reference dosimetry results of the shielded and unshielded configurations of the HPRR after burst operations. Because of changes to the reactor positioning and storage systems that were made in 1985, the previous dosimetry reports became obsolete, and the newly designed experiments were needed to create the HPRR’s adjusted dosimetry data. The various results reported in ORNL-6240 include reference doses and dose equivalents from different conventions at different distances and elevations as determined using the detected neutron fluence and conversion factors. The HPRR neutron fluence was obtained through different methods, including sulfur pellet analysis and threshold detector unit data. Information about the HPRR spectrum was also obtained through Bonner sphere measurements. This benchmark is focused on a part of the measured sulfur fluences reported in Appendix H of ORNL-6240. Standard commercial sulfur pellets were placed at different distances from the HPRR centerline during burst operation and were activated due to the 32 S(n,p) 32 P reaction. The resulting 32 P activity was then measured and the information about the corresponding sulfur fluence and/or neutron dose could be extracted. Many of those measurements have 7 been performed with the HPRR in its bare configuration or with different shields (combinations of Lucite, concrete, steel). All the necessary, precise information about material and/or dimensions of the different shields was not found, so it was decided to focus only on the unshielded and steel-shielded configurations to minimize the benchmark uncertainty. A total of 31 cases (24 unshielded and 7 shielded cases at different positions) of sulfur fluence were selected before evaluation to develop the benchmark.

21 SPECIFIC NUCLEAR REACTORS AND ASSOCIATED PLANTS↗
DOE OSTI2022

Estimating List-Mode Data Sensitivities to Nuclear Data with MCNP6

Nuclear data are a vital component of predictive simulations used in applications like experiment design, stockpile stewardship, nuclear nonproliferation/safeguards, health physics, and criticality safety. A singular simulation requires the coalescence of different areas of nuclear data such as cross sections, angular distributions, and energy distributions of emitted neutrons for different materials and energy ranges. Improving nuclear data and thus reducing the uncertainty in simulated parameters could enable smaller, better-informed safety factors and ultimately reduce operational and procedural costs. There is a constant effort to garner a better understanding of the physical quantities represented by nuclear data through experiments. Integral experiment benchmarks use simulated and measured results to validate current nuclear data values. In the past, benchmarks primarily focused on the effective multiplication factor (k eff ); however, this limited scope has caused compensating errors and areas of nuclear data that lack validation. Compensating errors are inaccuracies in nuclear data that are obfuscated by cancellation when observing integrated values such as k eff . Diverse integral benchmark experiments that look for quantities of interest other than k eff and include multiple responses minimize the possibility of compensating errors and provides validation to areas of nuclear data previously lacking experimental validation. Benchmark experiments can be optimized during the design process to be highly dependent on specific areas of nuclear data. The dependence of a response in an experiment to a specific area/type of nuclear data is defined as sensitivity. A larger sensitivity means that nuclear data uncertainties will play a larger role in the response(s) resulting in larger bias. Currently, the sensitivity capabilities of the Monte Carlo N-Particle (MCNP ®1 ) transport code are limited to responses of k eff and tallied values (e.g., flux, surface current). As a part of the EUCLID project, this work explores estimating list-mode nuclear data sensitivities that can be used to design experiments aimed to constrain and reduce compensating errors in nuclear data by focusing on responses other than k eff . Tallied values are ideal quantities that are estimated with detectors during experiments. List-mode data (a list of neutron collection times) are the direct output of detector systems in subcritical neutron noise experiments. Expanding MCNP sensitivity capabilities to include the sensitivity of responses estimated from list-mode data, such as the prompt neutron decay constant (α) and multiplicity estimates (S and D), enables more direct comparison of simulated and measured experimental quantities. Additionally, deterministic tools such as SENSMG are capable of obtaining sensitivities to a wide variety of responses; however, these tools cannot handle complex geometries due to the assumptions made in discretizing the phase-space variables of the Boltzman transport equation.

73 NUCLEAR PHYSICS AND RADIATION PHYSICS↗
DOE OSTI2021

A Verification of Flux Sensitivity Estimates Using the MCNP Tally Perturbation Tool

Nuclear data is commonly used in applications such as nuclear nonproliferation, safeguards, and criticality safety. More specifically, nuclear data is used in predictive simulation codes like the Monte-Carlo N-Particle (MCNP ® ) transport code, Serpent, and similar radiation transport codes. The improvement of nuclear data enables more precise and accurate simulations, which result in higher fidelity designs and reduced operational/procedural costs. Therefore, the improvement of nuclear data is of paramount importance across the nuclear community. Nuclear data is improved and validated through integral benchmark experiments. The design of benchmark experiments is an extensive process; therefore, these experiments are often optimized on multiple characteristics, including sensitivity to the nuclear data, during the design process. Sensitivity is a measure of how much a quantity changes due to changes in independent variables such as experimental configuration. An experimental design that has a larger sensitivity to the nuclear data of interest will have a larger impact on the accuracy and precision of the validated data. Past integral benchmark experiments have primarily used the effective multiplication factor ($k_{eff}$) as the predominant measured quantity; however, experiments designed with other quantities in mind would be able to optimize on validating different areas of the nuclear data. A primary goal of the EUCLID project is to design, constrain, and reduce compensating errors in experiments focused on quantities other than $k_{eff}$ to better validate nuclear data across the board. Currently, there is a capability in MCNP to easily calculate the sensitivity of $k_{eff}$ to specific nuclear data of numerous reactions types and isotopes (KSEN card); however, the sensitivity of other quantities must be estimated in more strenuous manners. For example, the perturbation feature (PERT card) of MCNP can be used to estimate first-order sensitivities of some response in fixed source simulations. A recent announcement revealed that the first- and second-order perturbation features in previous releases of MCNP contained a bug. It was identified that particles were being scored into the wrong energy bin. The bug is in the most recent public release (MCNP6.2); however, a patch has been added to the most up to date version (MCNP6.2.2) that has not been released publicly. A direct comparison of the PERT card results for an F4 (neutron flux averaged over a cell) tally before and after the patch are shown in figure 1. All simulations used in the sensitivity estimates in this report were performed with MCNP6.2.2. This work verifies the patched MCNP perturbation tool by comparing first order sensitivities made using the PERT card to estimates made using manual perturbation of the compact ENDF (ACE) files.

73 NUCLEAR PHYSICS AND RADIATION PHYSICS↗
DOE OSTI2022

Preliminary Design of a New Pulsed-Neutron Die--Away Experiments with Absorbers (IER-552 CED-1)

This report presents the preliminary design (CED-1) of IER-552, pulsed-neutron die-away (PNDA) experiments with absorbers, to be conducted by Lawrence Livermore National Laboratory (LLNL). The goal of the PNDA experiments with absorbing materials is to produce high-quality, low-cost integral benchmarks that can be used to validate cross sections that are high priority nuclear data for the Department of Energy’s Nuclear Criticality Safety Program (NCSP). PNDA experiments can be used to generate nuclear data validation benchmarks quickly and cheaply, as they do not require fissile material or a nuclear facility to conduct them. The original PNDA experiments were set up at LLNL under IER-501. Extending the PNDA experiments to include absorbing materials leverages existing facilities and resources at LLNL to validate cross sections, with a basic experiment design that uses a neutron generator to impinge a short, mono-energetic neutron pulse on a poisoned, moderating target sample. The neutron pulse lasts 100 µs, after which the neutron population in the sample reaches thermal equilibrium and later spatial equilibrium. In this fully equilibrized state, the neutron population has a characteristic decay-time eigenvalue. The eigenvalue can be used as an integral parameter to validate nuclear data involved with neutron scattering and absorption. Two observables can be measured: the neutron population and the population of secondary γ-rays produced by inelastic and capture reactions. This report explores the feasibility of both approaches. For γ-ray measurements, this allows for direct measurement of reactions of interest for validation. During the neutron burst time, inelastic (prompt) γ-rays dominate, and these data can be isolated for validation of neutron inelastic scattering data. After the pulse ends, neutron capture (delayed) γ-rays dominate and are produced by many reaction channels as neutrons slow down to thermal energies. Two sets of γ-ray spectra (inelastic, capture) can be produced for validation. Additionally, the time-dependent decay of the capture γ-ray population when the neutron population is thermalized and in its fundamental mode can be used for validation. Two experiments can be imagined where pulsed neutrons are used to validate the nuclear data of absorbing materials. The first integrates well into the existing PNDA testbed at LLNL. The absorber material would be introduced into a moderating target and the same neutron generator, neutron detectors, electronics, and shielding box used for IER-501 would be employed. From the same experimental setup, many absorbing materials can be validated by simply changing the neutron poison in the moderator. The only significant modification would be the introduction of a γ-ray detector. Such an experiment would primarily serve to validate nuclear data in the thermal energy range. The second kind of experiment would validate the fast and epithermal energy range. It would involve pulsing neutron into a bare assembly of the absorber material and measuring the die-away of neutrons. The fast leakage of such an assembly requires nanosecond neutron-generator pulse widths and fast detectors/electronics that could measure ~200 ns die-away curves. This kind of experiment would ideally be performed at a cyclotron, like that available at Lawrence Berkeley National Laboratory.

73 NUCLEAR PHYSICS AND RADIATION PHYSICS↗
NASA NTRS2017

Interpretable Categorization of Heterogeneous Time Series Data

We analyze data from simulated aircraft encounters to validate and inform the development of a prototype aircraft collision avoidance system. The high-dimensional and heterogeneous time series dataset is analyzed to discover properties of near mid-air collisions (NMACs) and categorize the NMAC encounters. Domain experts use these properties to better organize and understand NMAC occurrences. Existing solutions either are not capable of handling high-dimensional and heterogeneous time series datasets or do not provide explanations that are interpretable by a domain expert. The latter is critical to the acceptance and deployment of safety-critical systems. To address this gap, we propose grammar-based decision trees along with a learning algorithm. Our approach extends decision trees with a grammar framework for classifying heterogeneous time series data. A context-free grammar is used to derive decision expressions that are interpretable, application-specific, and support heterogeneous data types. In addition to classification, we show how grammar-based decision trees can also be used for categorization, which is a combination of clustering and generating interpretable explanations for each cluster. We apply grammar-based decision trees to a simulated aircraft encounter dataset and evaluate the performance of four variants of our learning algorithm. The best algorithm is used to analyze and categorize near mid-air collisions in the aircraft encounter dataset. We describe each discovered category in detail and discuss its relevance to aircraft collision avoidance.

Drones↗
DOE OSTI2020

Pitch Variation Experiments in Water-Moderated Square-Pitched U(6.90)O 2 Fuel Rod Lattices with Fuel to Water Volume Ratios Spanning 0.08 to 0.67

The US Department of Energy (DOE) Nuclear Energy Research Initiative funded the design and construction of the Seven Percent Critical Experiment (7uPCX) at Sandia National Laboratories. The start-up of the experiment facility and the execution of the experiments described here were funded by the DOE Nuclear Criticality Safety Program. The 7uPCX is designed to investigate critical systems with fuel for light water reactors in the enrichment range above 5 % 235 U. The 7uPCX assembly is a water-moderated and -reflected array of aluminum-clad square-pitched U(6.90 %)O 2 fuel rods. Other critical experiments performed in the 7uPCX assembly are documented in LEU-COMP-THERM-078, LEU-COMP-THERM-080, LEU-COMPTHERM- 096, LEU-COMP-THERM-097, and LEU-COMP-THERM-101. The fuel used in these experiments was fabricated using unirradiated 6.90 % enriched UO 2 fuel pellets from fuel elements designed to be used in the internal nuclear superheater section of the Pathfinder boiling water reactor operated in South Dakota by the Northern States Power Company in the 1960s. The fuel elements were obtained from The Pennsylvania State University where they had been stored for many years. The fuel pellets in those fuel elements were removed from the original Incoloy cladding and reclad in 3003 aluminum tubes and end caps for use in the experiments reported here. The purpose of these experiments was to measure the effects of decreasing the fuel-to-water volume ratio on the critical array size. This was accomplished by removing fuel rods from fully fueled configurations, effectively increasing the pitch of the fuel arrays in the assembly. The fuel rod pitch variations provided assembly configurations that ranged from strongly undermoderated to slightly overmoderated.

11 NUCLEAR FUEL CYCLE AND FUEL MATERIALS↗
DOE OSTI2020

Partially-Reflected Water-Moderated Square-Pitched U(6.90)O 2 Fuel Rod Lattices with 0.52 Fuel to Water Volume Ratio (0.855 CM Pitch)

The US Department of Energy (DOE) Nuclear Energy Research Initiative funded the design and construction of the Seven Percent Critical Experiment (7uPCX) at Sandia National Laboratories. The start-up of the experiment facility and the execution of the experiments described here were funded by the DOE Nuclear Criticality Safety Program. The 7uPCX is designed to investigate critical systems with fuel for light water reactors in the enrichment range above 5 % 235 U. The 7uPCX assembly is a water-moderated and -reflected array of aluminum-clad square-pitched U(6.90 %)0 2 fuel rods. Other critical experiments performed in the 7uPCX assembly are documented in LEU-COMP-THERM-078, LEU-COMP-THERM-080, LEU-COMP-THERM-096, and LEU-COMP-THERM-097.

11 NUCLEAR FUEL CYCLE AND FUEL MATERIALS↗
DOE OSTI2023

Molybdenum Sleeve Experiments in Fully-Reflected Water-Moderated Triangular-Pitched U(6.90)O 2 Fuel Rod Lattices (1.55 cm Pitch)

The US Department of Energy (DOE) Nuclear Energy Research Initiative funded the design and construction of the Seven Percent Critical Experiment (7uPCX) at Sandia National Laboratories. The start-up of the experiment facility and the execution of the experiments described here were funded by the DOE Nuclear Criticality Safety Program. The 7uPCX is designed to investigate critical systems with fuel for light water reactors in the enrichment range above 5 % 235 U. The 7uPCX assembly is a water-moderated and -reflected array of aluminum-clad U(6.90 %)O 2 fuel rods. Other critical experiments performed in the 7uPCX assembly are documented in LEU-COMP-THERM-078, LEU-COMP-THERM-080, LEU-COMP-THERM-096, LEUCOMP-THERM-097, LEU-COMP-THERM-101, and LEU-COMP-THERM-102. The purpose of these experiments was to measure the effects of molybdenum in nearly-critical systems. The molybdenum was introduced into the fuel arrays as tubular sleeves that surrounded some of the fuel rods in the fuel arrays measured. Four hundred molybdenum tubes nominally 12.7 mm outside diameter, 498 mm long, with 0.762 mm wall thickness were provided for the experiments by the Institut de Radioprotection et de Sûreté Nucléaire (IRSN). Small polyethylene adapters at each end of the tubes were used to center each tube on a fuel rod in the assembly. The critical experiments were done using a set of triangular-pitched grid plates fabricated for these experiments. The grid plate set accommodated a fuel array of a total of 1261 fuel rod positions on a pitch of 0.610 in (1.5494 cm) in a series of 20 hexagonal rings surrounding the central fuel rod. The fuel used in these experiments was fabricated using unirradiated 6.90 % enriched UO 2 fuel pellets from fuel elements designed to be used in the internal nuclear superheater section of the Pathfinder boiling water reactor operated in South Dakota by the Northern States Power Company in the 1960s. The fuel elements were obtained from The Pennsylvania State University where they had been stored for many years. The fuel pellets in those fuel elements were removed from the original Incoloy cladding and reclad in 3003 aluminum tubes and end caps for use in the experiments reported here. The five critical experiments in this series were performed in August through December 2022, in the Sandia Critical Experiments (SCX) at the Sandia Pulsed Reactor Facility. Case 1 had no molybdenum sleeves, Case 2 had 208 molybdenum sleeves clustered at the center of the array, Case 3 had 397 molybdenum sleeves clustered at the center of the array, Case 4 had 175 molybdenum sleeves in the central position and in five alternating hexagonal rings, and Case 5 had 331 molybdenum sleeves in the central position and in seven alternating hexagonal rings. All five critical experiments are judged to be acceptable as benchmark experiments.

11 NUCLEAR FUEL CYCLE AND FUEL MATERIALS↗
NASA NTRSDate not supplied

A Formal Verification Framework for Runtime Assurance

The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality, allowing for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

Runtime assurance↗
NASA NTRSDate not supplied

A Formal Verification Framework for Runtime Assurance

The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality, allowing for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

Runtime assurance↗
NASA NTRS2011

Reliability and Maintainability Engineering - A Major Driver for Safety and Affordability

The United States National Aeronautics and Space Administration (NASA) is in the midst of an effort to design and build a safe and affordable heavy lift vehicle to go to the moon and beyond. To achieve that, NASA is seeking more innovative and efficient approaches to reduce cost while maintaining an acceptable level of safety and mission success. One area that has the potential to contribute significantly to achieving NASA safety and affordability goals is Reliability and Maintainability (R&M) engineering. Inadequate reliability or failure of critical safety items may directly jeopardize the safety of the user(s) and result in a loss of life. Inadequate reliability of equipment may directly jeopardize mission success. Systems designed to be more reliable (fewer failures) and maintainable (fewer resources needed) can lower the total life cycle cost. The Department of Defense (DOD) and industry experience has shown that optimized and adequate levels of R&M are critical for achieving a high level of safety and mission success, and low sustainment cost. Also, lessons learned from the Space Shuttle program clearly demonstrated the importance of R&M engineering in designing and operating safe and affordable launch systems. The Challenger and Columbia accidents are examples of the severe impact of design unreliability and process induced failures on system safety and mission success. These accidents demonstrated the criticality of reliability engineering in understanding component failure mechanisms and integrated system failures across the system elements interfaces. Experience from the shuttle program also shows that insufficient Reliability, Maintainability, and Supportability (RMS) engineering analyses upfront in the design phase can significantly increase the sustainment cost and, thereby, the total life cycle cost. Emphasis on RMS during the design phase is critical for identifying the design features and characteristics needed for time efficient processing, improved operational availability, and optimized maintenance and logistic support infrastructure. This paper discusses the role of R&M in a program acquisition phase and the potential impact of R&M on safety, mission success, operational availability, and affordability. This includes discussion of the R&M elements that need to be addressed and the R&M analyses that need to be performed in order to support a safe and affordable system design. The paper also provides some lessons learned from the Space Shuttle program on the impact of R&M on safety and affordability.

Safie, Fayssal M.↗
NASA NTRS2009

Deriving Safety Cases from Automatically Constructed Proofs

Formal proofs provide detailed justification for the validity of claims and are widely used in formal software development methods. However, they are often complex and difficult to understand, because the formalism in which they are constructed and encoded is usually machine-oriented, and they may also be based on assumptions that are not justified. This causes concerns about the trustworthiness of using formal proofs as arguments in safety-critical applications. Here, we present an approach to develop safety cases that correspond to formal proofs found by automated theorem provers and reveal the underlying argumentation structure and top-level assumptions. We concentrate on natural deduction style proofs, which are closer to human reasoning than resolution proofs, and show how to construct the safety cases by covering the natural deduction proof tree with corresponding safety case fragments. We also abstract away logical book-keeping steps, which reduces the size of the constructed safety cases. We show how the approach can be applied to the proofs found by the Muscadet prover.

Basir, Nurlida↗
NASA NTRS2009

Deriving Safety Cases from Machine-Generated Proofs

Proofs provide detailed justification for the validity of claims and are widely used in formal software development methods. However, they are often complex and difficult to understand, because they use machine-oriented formalisms; they may also be based on assumptions that are not justified. This causes concerns about the trustworthiness of using formal proofs as arguments in safety-critical applications. Here, we present an approach to develop safety cases that correspond to formal proofs found by automated theorem provers and reveal the underlying argumentation structure and top-level assumptions. We concentrate on natural deduction proofs and show how to construct the safety cases by covering the proof tree with corresponding safety case fragments.

Basir, Nurlida↗
NASA NTRS2009

Deriving Safety Cases from Machine-Generated Proofs

Proofs provide detailed justification for the validity of claims and are widely used in formal software development methods. However, they are often complex and difficult to understand, because they use machine-oriented formalisms; they may also be based on assumptions that are not justified. This causes concerns about the trustworthiness of using formal proofs as arguments in safety-critical applications. Here, we present an approach to develop safety cases that correspond to formal proofs found by automated theorem provers and reveal the underlying argumentation structure and top-level assumptions. We concentrate on natural deduction proofs and show how to construct the safety cases by covering the proof tree with corresponding safety case fragments.

Basir, Nurlida↗