Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “divergence theorem”

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.

23 records · Page 2
All sourcesNASA NTRSDOE OSTI
NASA NTRS2011

Discretely Conservative Finite-Difference Formulations for Nonlinear Conservation Laws in Split Form: Theory and Boundary Conditions

Simulations of nonlinear conservation laws that admit discontinuous solutions are typically restricted to discretizations of equations that are explicitly written in divergence form. This restriction is, however, unnecessary. Herein, linear combinations of divergence and product rule forms that have been discretized using diagonal-norm skew-symmetric summation-by-parts (SBP) operators, are shown to satisfy the sufficient conditions of the Lax-Wendroff theorem and thus are appropriate for simulations of discontinuous physical phenomena. Furthermore, special treatments are not required at the points that are near physical boundaries (i.e., discrete conservation is achieved throughout the entire computational domain, including the boundaries). Examples are presented of a fourth-order, SBP finite-difference operator with second-order boundary closures. Sixth- and eighth-order constructions are derived, and included in E. Narrow-stencil difference operators for linear viscous terms are also derived; these guarantee the conservative form of the combined operator.

Fisher, Travis C.↗
NASA NTRSDate not supplied

A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts

The NASA DAIDALUS library provides formal definitions for Detect-and-Avoid avionics concepts such as when an aircraft is well-clear with respect to the surrounding air traffic, i.e., it does not operate in such proximity to create a collision hazard. While several properties are proven correct for DAIDALUS assuming ideal real number arithmetic, an actual implementation that uses floating-point numbers may behave unexpectedly because of round-off errors and run-time exceptions. This paper presents an experience report on the application of a formal methods toolchain to extract and verify floating-point C code from a real-valued specification of the well-clear module of DAIDALUS. This toolchain comprises the PVS theorem prover, the PRECiSA floating-point analyzer and code generator, and the Frama-C analysis suite. The generated code is automatically instrumented to detect when the control flow of the floating-point program may diverge from the ideal real number specification, and it is annotated with contracts that state the maximum accumulated round-off error. The absence of overflows is also formally verified for the generated code. In order to apply the toolchain to an industrial case study such as DAIDALUS, a formally verified pre-processing of the input specification is performed, which includes a program slicing and several semantic-preserving simplifications.

Program verification↗
NASA NTRS1997

On the Behavior of Velocity Fluctuations in Rapidly Rotating Flows

The behavior of velocity fluctuations subjected to rapid rotation is examined. The rapid rotation considered is any arbitrary combination of two basic forms of rotation, reference frame rotation and mean flow rotation. It is recognized that the two types of rotating flows differ in the manner in which the fluctuating fields are advected. The first category is comprised of flows in rotating systems of which synoptic scale geophysical flows are a good example. In this class of flows the fluctuating velocity field advects and rotates with the mean flow. In the rapid rotation limit, the Taylor-Proudman theorem describes the behavior of this class of fluctuations. Velocity fluctuations that are advected without rotation by the mean flow constitute the second category which includes vortical flows of aerodynamic interest. The Taylor-Proudman theorem is not pertinent to I his class flows and a new result appropriate to this second category of fluctuations is derived. The present development demonstrates that the fluctuating velocity fields are rendered two-dimensional and horizontally non-divergent in the limit of any large combination of reference frame rotation and mean-flow rotation. The concommitant 'geostrophic' balance of the momentum equation is, however, dependent upon the form of rapid rotation. It is also demonstrated that the evolution equations of a two-dimensional fluctuating velocity fields are frame-indifferent with any imposed mean-flow rotation. The analyses and results of this paper highlight many fundamental aspects of rotating flows and have important consequences for their turbulence closures in inertial and non-inertial frames.

Girimaji, S. S.↗
NASA NTRSDate not supplied

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↗
NASA NTRS2013

MHD Simulations of the Plasma Flow in the Magnetic Nozzle

The magnetohydrodynamic (MHD) flow of plasma through a magnetic nozzle is simulated by solving the governing equations for the plasma flow in the presence of an static magnetic field representing the applied nozzle. This work will numerically investigate the flow and behavior of the plasma as the inlet plasma conditions and magnetic nozzle field strength are varied. The MHD simulations are useful for addressing issues such as plasma detachment and to can be used to gain insight into the physical processes present in plasma flows found in thrusters that use magnetic nozzles. In the model, the MHD equations for a plasma, with separate temperatures calculated for the electrons and ions, are integrated over a finite cell volume with flux through each face computed for each of the conserved variables (mass, momentum, magnetic flux, energy) [1]. Stokes theorem is used to convert the area integrals over the faces of each cell into line integrals around the boundaries of each face. The state of the plasma is described using models of the ionization level, ratio of specific heats, thermal conductivity, and plasma resistivity. Anisotropies in current conduction due to Hall effect are included, and the system is closed using a real-gas equation of state to describe the relationship between the plasma density, temperature, and pressure.A separate magnetostatic solver is used to calculate the applied magnetic field, which is assumed constant for these calculations. The total magnetic field is obtained through superposition of the solution for the applied magnetic field and the self-consistently computed induced magnetic fields that arise as the flowing plasma reacts to the presence of the applied field. A solution for the applied magnetic field is represented in Fig. 1 (from Ref. [2]), exhibiting the classic converging-diverging field pattern. Previous research was able to demonstrate effects such as back-emf at a super-Alfvenic flow, which significantly alters the shape of the magnetic field in both the near- and far-field regions. However, in that work the downstream domain was constrained to a channel of constant cross-sectional area. In the present work we seek to address this issue by modeling the downstream region with a domain that permits free expansion of the plasma, permitting a better evaluation of the downstream effects the applied field has on the plasma. The inlet boundary conditions and applied magnetic field values will also be varied to determine the effect the initial plasma energy content and applied magnetic field energy density have on the near- and far-field plasma properties on the MHD code. This will determine the effect of inlet boundary conditions on the results downstream and address issues related to the restrictive numerical domain previously used.

Smith, T. E. R.↗