Engineering PapersSearch

SEARCH · Engineering Papers

Results for “MOSCATO”

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 19 records

MOSCATO Development and Integration in Fiscal Year 2025: Implementation of Multiphase, Multiphysics Modeling Capabilities for Molten Salt Systems

MOSCATO (Molten Salt Chemistry and Transport) is a multiphysics code that provides high-fidelity, coupled simulations of fluid flow, heat transfer, mass transfer, chemistry, electrochemical phenomena, and alloy corrosion for molten salt systems. In FY25, significant developments were made to the code package, enhancing its capabilities for modeling all relevant phenomena within operating moltens salt reactors (MSRs). The developments and activities in FY25 included: 1. Implementation of Level-Set methods to enable modeling of single-bubble behavior in molten salts. In FY25, the Level-Set two-phase flow modeling implementation was improved to simulate single bubble behavior with molten salt media. The large density and viscosity ratios between typical gases and molten salt liquids present challenges for these types of numerical solvers. With enhancements to the pressure projection method, MOSCATO’s Level-Set solver was able to be successfully validated to experiments related to helium bubble rise in stagnant molten salt. The simulated bubble rising velocity showed reasonable good agreement with experimental measurements. The bubble shape and dynamics were also visually compared with experimental snapshots, demonstrating a good qualitative match. 2. Generation of mass transfer correlations for multiphase flow systems. To enable calculations of the tritium transport across the interface between gas bubbles and salt, we modeled high- Schmidt-number mass transfer around a sphere across a broad range of Reynolds numbers. The mesh near the sphere surface was highly refined to resolve steep concentration gradients caused by the low diffusion coefficient. Literature-based mass transfer correlations were compared with the numerical results, and modifications were proposed to improve agreement, particularly at higher Schmidt numbers. These mass transfer correlations were subsequently provided to other national laboratories to help enable high quality mass transfer simulations using lower-order solvers under development within the NEAMS program. 3. Preliminary implementation of a bubbly flow solver. To model bubbly flow in molten salt, we implemented a bubbly flow solver for void fractions less than 5%. To do so, an algebraic relative velocity model that assumes small bubbles with rapid momentum equilibration was added to MOSCATO to compute bubble velocities. Preliminary comparisons with experimental data showed reasonable agreement, and further improvements are underway. 4. Generation of mass transfer correlations for MSRE subchannel The Molten-Salt Reactor Experiment (MSRE) was a landmark historical project that demonstrated the feasibility of molten-salt reactor technology. The MSRE campaign also generated a significant body of experimental data and reports that continue to support molten-salt–related research. In this report, the MSRE core subchannel was used as the reference geometry for a mass transfer study performed with MOSCATO. The geometry and computational mesh were adapted from a previous study, providing adequate resolution for the relatively low Reynolds number in this case. Additional mesh refinement was applied to reach higher Schmidt numbers, enabling the derivation of a reliable mass-transfer correlation for the present scenario. 5. Simulations of oxygen ingressions into molten salt. In the previous fiscal year, we initiated a study to simulate oxygen ingression in stagnant salt. As oxygen enters the salt through its surface, it reacts with Ce 3+ to form solid CeO 2 and other reaction products. To more fully capture the complex diffusion-convection-reaction mechanisms, capabilities for modeling natural convection in the salt vessel were added. These were needed as the flow of the ingressed gas induced flow in the salt caused by surface shear and non-isothermal effects. With these updated physics in place, we were able to successfully reproduce the experimental results for the rate of change of CeCl 3 concentrations versus time. 6. Flow corrosion model validation. In FY24, MOSCATO’s corrosion model was validated against static corrosion experiments. In FY25, this work was extended to a flow corrosion experiment, where FLiNaK salt was driven by natural convection, with initial salt impurities to initiate corrosion. Despite uncertainties in parameters such as elemental diffusion coefficients in the alloy and unknown H + concentrations, the simulations achieved good agreement with experimental results, especially in predicting sample mass losses.

22 GENERAL STUDIES OF NUCLEAR REACTORS

Development of MOSCATO: A CFD-Level Electrochemistry and Corrosion Simulator for Molten Salt Systems

For both coolant and fueled variants of molten salt reactors (MSRs), the corrosion of structural materials is a significant challenge. The corrosion stems from chemical and electrochemical reactions initiated by fissile material, fission products, and impurities in the salt. Lower-fidelity models rely on empirical correlations for mass transfer, simplified lumped temperature profiles, and similar assumptions. They do not capture detailed spatial variations in complex geometries, creating the need for high-fidelity modeling to bridge this gap.As we approach the demonstration and possible deployment of MSRs in this decade, the development of a high-fidelity, high-performance simulator becomes imperative. To simulate the complex electrochemical environment and corrosion within molten salt systems, we have developed the Molten Salt Chemistry And TranspOrt (MOSCATO) code. This endeavor is comprised of three essential components. First, mass transfer equations are coupled with the Navier-Stokes equations in order to account for the transport of species in the salt. Second, the diffusion of alloy constituents, such as Cr, Fe, Ni, etc. is simulated within the structural metals. Third, the alloy and salt domains are coupled to account for the heterogeneous chemical and electrochemical reactions that occur at the salt-alloy interface.MOSCATO manages all three components within the framework of the highly scalable, open-source spectral element method computational fluid dynamics code Nek5000/NekRS. This integration enables MOSCATO to harness the immense computational power of modern high-performance computing resources, ensuring both high fidelity and computational speed.In addition to code development, we have initiated a comprehensive verification and validation campaign, utilizing data from diverse sources. First, MOSCATO's electrochemical solver was verified with reference numerical data. Then validation occurred against experiments: one of a thermal galvanic cell and the other for corrosion in flowing molten salt of FLiNaK (LiF-NaF-KF). This campaign verified and validated MOSCATO as a reliable tool for simulating electrochemical environments and corrosion in molten salt systems.

22 GENERAL STUDIES OF NUCLEAR REACTORS

Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis

This paper introduces a static analysis technique for computing formally verified round-off error bounds of floating-point functional expressions. The technique is based on a denotational semantics that computes a symbolic estimation of floating-point round-o errors along with a proof certificate that ensures its correctness. The symbolic estimation can be evaluated on concrete inputs using rigorous enclosure methods to produce formally verified numerical error bounds. The proposed technique is implemented in the prototype research tool PRECiSA (Program Round-o Error Certifier via Static Analysis) and used in the verification of floating-point programs of interest to NASA.

Moscato, Mariano

An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs

This paper presents an abstract interpretation framework for the round-off error analysis of floating-point programs. This framework defines a parametric abstract analysis that computes, for each combination of ideal and floating-point execution path of the program, a sound over-approximation of the accumulated floating-point round-off error that may occur. In addition, a Boolean expression that characterizes the input values leading to the computed error approximation is also computed. An abstraction on the control flow of the program is proposed to mitigate the explosion of the number of elements generated by the analysis. Additionally, a widening operator is defined to ensure the convergence of recursive functions and loops. An instantiation of this framework is implemented in the prototype tool PRECiSA that generates formal proof certificates stating the correctness of the computed round-off errors.

Titolo, Laura

A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm

The Automatic Dependent Surveillance-Broadcast (ADS-B) system allows aircraft to communicate their current state, including position and velocity information, to other aircraft in their vicinity and to ground stations. The Compact Position Reporting (CPR) algorithm is the ADS-B module responsible for the encoding and decoding of aircraft positions. CPR is highly sensitive to computer arithmetic since it heavily relies on functions that are intrinsically unstable such as floor and modulo. In this paper, a formally-verified double-precision floating-point implementation of the CPR algorithm is presented. The verification proceeds in three steps. First, an alternative version of CPR, which reduces the floating-point rounding error is proposed. Then, the Prototype Verification System (PVS) is used to formally prove that the ideal real-number counterpart of the improved algorithm is mathematically equivalent to the standard CPR definition. Finally, the static analyzer Frama-C is used to verify that the double-precision implementation of the improved algorithm is correct with respect to its operational requirement. The alternative algorithm is currently being considered for inclusion in the revised version of the ADS-B standards document as the reference implementation of the CPR algorithm.

Laura Titolo

A Mixed Real and Floating-Point Solver

Reasoning about mixed real and floating-point constraints is essential for developing accurate analysis tools for floating-point pro- grams. This paper presents FPRoCK, a prototype tool for solving mixed real and floating-point formulas. FPRoCK transforms a mixed formula into an equisatisfiable one over the reals. This formula is then solved using an off-the-shelf SMT solver. FPRoCK is also integrated with the PRECiSA static analyzer, which computes a sound estimation of the round-off error of a floating-point program. It is used to detect infeasible computational paths, thereby improving the accuracy of PRECiSA.

Salvia, Rocco

Provably Correct Floating-Point Implementation of a Point-In-Polygon Algorithm

The problem of determining whether or not a point lies inside a given polygon occurs in many applications. In air traffic management concepts, a correct solution to the point-in-polygon problem is critical to geofencing systems for Unmanned Aerial Vehicles and in weather avoidance applications. Many mathematical methods can be used to solve the point-in-polygon problem. Unfortunately, a straightforward floating- point implementation of these methods can lead to incorrect results due to round-off errors. In particular, these errors may cause the control flow of the program to diverge with respect to the ideal real-number algorithm. This divergence potentially results in an incorrect point-in- polygon determination even when the point is far from the edges of the polygon. This paper presents a provably correct implementation of a point-in-polygon method that is based on the computation of the winding number. This implementation is mechanically generated from a source- to-source transformation of the ideal real-number specification of the algorithm. The correctness of this implementation is formally verified within the Frama-C analyzer, where the proof obligations are discharged using the Prototype Verification System (PVS).

Moscato, Mariano M.

Automatic Generation of Guard-Stable Floating-Point Code

In floating-point programs, test instability occurs when the control flow of a conditional statement diverges from its ideal execution under real arithmetic. This phenomenon is caused by the presence of round-off errors in floating-point computations. Writing programs that correctly handle test instability often require expertise on finite precision computations and rounding errors. This paper presents a fully automatic tool chain that generates and formally verifies a test-stable floating-point C program from its functional specification in real arithmetic. The generated program is instrumented to soundly detect when unstable tests may occur and, in these cases, to issue a warning. The proposed approach combines the PRECiSA floating-point static analyzer, the Frama-C software verification suite, and the PVS theorem prover.

Floating-Point Arithmetic

Intelligent Lemma Selection for Formal Methods Proofs

To help in formally verifying the correctness of various systems, NASA constructs mathematical proofs using the proof assistant PVS (Prototype Verification System). Throughout this effort, NASA has amassed a library of tens of thousands of proven lemmas. While these lemmas can often be applied to new problems, their abundance can make lemma selection a non-trivial task. This project focuses on creating a lemma selector for use in PVS based on existing systems MePo, MaSh, and MeSh, which were written for other proof assistants. An initial benchmark system makes selections based on symbol-level similarity while the final lemma selector is a hybrid system, combining the classical approach used in the benchmark with a machine learning approach which leverages the lemmas' past usage.

Connor T Baumler

Formal Verification of Termination Criteria for First-Order Recursive Functions

This paper presents a formalization of several termination criteria for first-order recursive functions. The formalization, which is developed in the Prototype Verification System (PVS), includes the specification and proof of equivalence of semantic termination, Turing termination, size change principle, calling context graphs, and matrix-weighted graphs. These termination criteria are defined on a computational model that consists of a basic functional language called PVS0, which is an embedding of recursive first-order functions. Through this embedding, the native mechanism for checking termination of recursive functions in PVS could be soundly extended with semi-automatic termination criteria such as calling contexts graphs. As a proof of concept, this paper illustrates how such an extension can be implemented using proof strategies based on computational reflection.

Formal Verification

Formal Verification of Termination Criteria for​ First-Order Recursive Functions

This talk presents a formalization of several termination criteria for first-order recursive functions. The formalization, which is developed in the Prototype Verification System (PVS), includes the specification and proof of equivalence of semantic termination, Turing termination, size change principle, calling context graphs, and matrix-weighted graphs. These termination criteria are defined on a computational model that consists of a basic functional language called PVS0, which is an embedding of recursive first-order functions. Through this embedding, the native mechanism for checking termination of recursive functions in PVS could be soundly extended with semi-automatic termination criteria such as calling contexts graphs.

Termination

Towards an Implementation of Differential Dynamic Logic in PVS

This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, which employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification process. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties.

Differential Dynamic Logic

PRECiSA: a static analysis tool for floating-point programs

This presentation introduces PRECiSA, a static analysis framework for analyzing floating-point programs. PRECiSA computes round-off error bounds for a class of floating-point programs, and produces a formal proof certificate of the correctness of these bounds. PRECiSA also has the capability of generating C code which is instrumented to detect unstable branching conditions from a real-number algorithm specification.

Floating-point

Interpretation and Formalization of the Right-of-Way Rules

This paper presents an interpretation and mathematical definition of the right-of-way rules as stated in USA, Title 14 of the Code of Federal Regulations, Part 91, Section 91.113 (14 CFR 91.113). In an encounter between two aircraft, the right-of-way rules in 14 CFR 91.113 defines which aircraft, if any, has the right-of-way and which aircraft must maneuver to stay well clear of the other aircraft. The objective of the work presented in this paper is to give an unambiguous interpretation of the rules. From the interpretation, a precise mathematical formulation is created that can be used for analysis and proof of properties. The mathematical formulation has been defined in the Prototype Verification System (PVS) and properties of well formedness and core properties of the formalization have been mechanically proved. Additional objectives are to use the mathematical formulation to code a rule compliant virtual pilot that can be used in simulation experiments and to possibly use the rule compliant virtual pilot in autonomous operations.

right-of-way