Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Correctness proofs”

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 91 records · Page 5
All sourcesNASA NTRSDOE OSTI
NASA NTRS1973

Research in mathematical theory of computation

Research progress in the following areas is reviewed: (1) new version of computer program LCF (logic for computable functions) including a facility to search for proofs automatically; (2) the description of the language PASCAL in terms of both LCF and in first order logic; (3) discussion of LISP semantics in LCF and attempt to prove the correctness of the London compilers in a formal way; (4) design of both special purpose and domain independent proving procedures specifically program correctness in mind; (5) design of languages for describing such proof procedures; and (6) the embedding of ideas in the first order checker.

Mccarthy, J.↗
NASA NTRSDate not supplied

Space-borne Doppler Weather Radar Modeling for Radar Design Evaluation

A model has been developed to predict the reflectivity and Doppler performance of a spaceborne weather radar for atmospheric aerosol and cloud monitoring. The goal is to predict radar sensitivity, resolution, uncertainties and other key performance metrics vs. radar design parameters and hardware nonidealities. Analytical formulas are readily available to predict key performance metrics of a space-borne radar system as a function of design parameters such as antenna size, spacecraft velocity, transmit power, and receive noise figure. Effects of some system nonidealities such as antenna pointing errors, power amplifier nonlinearity and phase noise can be estimated using idealized methods. These analytical formulas use idealized forms of the antenna radiation pattern and weather statistics to predict system performance. However, it is desirable to have a more physical model based on discretized weather volumes in which the particle size distribution, Doppler distribution, and other parameters can be varied to study how the radar hardware design parameters and nonidealities affect the measurement of the weather reflectivity and Doppler characteristics. This would allow the radar designers to have more insight into what is being measured and the hardware parameters and errors that need to be carefully controlled to achieve best radar performance, as well as potential methods to calibrate the system or correct errors. This presentation will demonstrate some proof-of-concept Ka-band simulations where the discretized model agrees with the analytical formulas for a simple case where the elements in the discretized weather volume are defined by a constant reflectivity and simple velocity vectors. In particular, the system sensitivity and Doppler uncertainty are evaluated by analytical formulas as well as the discretized model. Future work will expand on this to include more complex weather scenarios and the addition of system nonidealities.

Sara Tucker↗
NASA NTRS1977

Proving the correctness of the flight director program EADIFD, volume 1

EADIFD is written in symbolic assembly language for execution on the C4000 airborne computer. It is a subprogram of an aircraft navigation and guidance program and is used to generate pitch and roll command signals for use in terminal airspace. The proof of EADIFD was carried out by an inductive assertion method consisting of two parts, a verification condition generator and a source language independent proof checker. With the specifications provided by NASA, EADIFD was proved correct. The termination of the program is guaranteed and the program contains no instructions that can modify it under any conditions.

Lee, F. J.↗
NASA NTRS1993

A nonconforming multigrid method using conforming subspaces

For second-order elliptic boundary value problems, we develop a nonconforming multigrid method using the coarser-grid correction on the conforming finite element subspaces. The convergence proof with an arbitrary number of smoothing steps for nu-cycle is presented.

Lee, Chang Ock↗
NASA NTRS2017

Development of Gridded Innovations and Observations Supplement to MERRA-2

Atmospheric reanalysis have become an important source of data for weather and climate research, owing to the continuity of the data, but especially because of the multitude of observational data included (radiosondes, commercial aircraft, retrieved data products and radiances). However, the presence of assimilated observations can vary based on numerous factors, and so it is difficult or impossible for a researcher to say with any degree of certainty how many and what type of observations contributed to the reanalysis data they are using at any give point in time or space. For example, quality control, transmission interruptions, and station outages can occasionally affect data availability. While orbital paths can be known, drift in certain instruments and the large number of available instruments makes it challenging to know which satellite is observing any region at any point in the diurnal cycle. Furthermore, there is information from the statistics generated by the data assimilation that can help understand the model and the quality of the reanalysis. Typically, the assimilated observations and their innovations are in observation-space data formats and have not been made easily available to reanalysis users.A test data set has been developed to make the MERRA-2 assimilated observations available for rapid and general use, by simplifying the data format. The observations are binned to a grid similar as MERRA-2 and saved as netCDF. This data collection includes the mean and number of observations in the bin as well as its variance. The data will also include the innovations from the data assimilation, the forecast departure and the analysis increment, as well as bias correction (for satellite radiances). We refer to this proof-of-concept data as the MERRA-2 Gridded Innovations and Observations (GIO). In this paper, we present the data format and its strengths and limitations with some initial testing and validation of the methodology.

SSMI↗
NASA NTRS2001

Dual-mass vibratory rate gyroscope with suppressed translational acceleration response and quadrature-error correction capability

A microfabricated vibratory rate gyroscope to measure rotation includes two proof-masses mounted in a suspension system anchored to a substrate. The suspension has two principal modes of compliance, one of which is driven into oscillation. The driven oscillation combined with rotation of the substrate about an axis perpendicular to the substrate results in Coriolis acceleration along the other mode of compliance, the sense-mode. The sense-mode is designed to respond to Coriolis accelerationwhile suppressing the response to translational acceleration. This is accomplished using one or more rigid levers connecting the two proof-masses. The lever allows the proof-masses to move in opposite directions in response to Coriolis acceleration. The invention includes a means for canceling errors, termed quadrature error, due to imperfections in implementation of the sensor. Quadrature-error cancellation utilizes electrostatic forces to cancel out undesired sense-axis motion in phase with drive-mode position.

Clark, William A.↗
NASA NTRS1996

Verification and Validation of KBS with Neural Network Components

Artificial Neural Network (ANN) play an important role in developing robust Knowledge Based Systems (KBS). The ANN based components used in these systems learn to give appropriate predictions through training with correct input-output data patterns. Unlike traditional KBS that depends on a rule database and a production engine, the ANN based system mimics the decisions of an expert without specifically formulating the if-than type of rules. In fact, the ANNs demonstrate their superiority when such if-then type of rules are hard to generate by human expert. Verification of traditional knowledge based system is based on the proof of consistency and completeness of the rule knowledge base and correctness of the production engine.These techniques, however, can not be directly applied to ANN based components.In this position paper, we propose a verification and validation procedure for KBS with ANN based components. The essence of the procedure is to obtain an accurate system specification through incremental modification of the specifications using an ANN rule extraction algorithm.

Wen, Wu↗
NASA NTRS1982

Formal specification and mechanical verification of SIFT - A fault-tolerant flight control system

The paper describes the methodology being employed to demonstrate rigorously that the SIFT (software-implemented fault-tolerant) computer meets its requirements. The methodology uses a hierarchy of design specifications, expressed in the mathematical domain of multisorted first-order predicate calculus. The most abstract of these, from which almost all details of mechanization have been removed, represents the requirements on the system for reliability and intended functionality. Successive specifications in the hierarchy add design and implementation detail until the PASCAL programs implementing the SIFT executive are reached. A formal proof that a SIFT system in a 'safe' state operates correctly despite the presence of arbitrary faults has been completed all the way from the most abstract specifications to the PASCAL program.

Melliar-Smith, P. M.↗
NASA NTRS1978

A uniqueness proof for a transonic flow problem

The uniqueness of the first-order lifting-line correction to the two-dimensional transonic small disturbance potential for the flow past a lifting, three-dimensional, large-aspect-ratio wing is proved. The correction is the solution of a linear equation of mixed type in the plane slit along the positive x-axis. The boundary data consist of Neumann data, continuity restrictions, the Kutta condition, and the form of the asymptotic behavior at infinity. The zeroth-order flow is assumed to be shock-free, and hence the correction is shock-free.

Cook, L. P.↗
NASA NTRS1990

Machine-checked proofs of the design and implementation of a fault-tolerant circuit

A formally verified implementation of the 'oral messages' algorithm of Pease, Shostak, and Lamport is described. An abstract implementation of the algorithm is verified to achieve interactive consistency in the presence of faults. This abstract characterization is then mapped down to a hardware level implementation which inherits the fault-tolerant characteristics of the abstract version. All steps in the proof were checked with the Boyer-Moore theorem prover. A significant results is the demonstration of a fault-tolerant device that is formally specified and whose implementation is proved correct with respect to this specification. A significant simplifying assumption is that the redundant processors behave synchronously. A mechanically checked proof that the oral messages algorithm is 'optimal' in the sense that no algorithm which achieves agreement via similar message passing can tolerate a larger proportion of faulty processor is also described.

Bevier, William R.↗
NASA NTRS2001

Theory Interpretations in PVS

The purpose of this task was to provide a mechanism for theory interpretations in a prototype verification system (PVS) so that it is possible to demonstrate the consistency of a theory by exhibiting an interpretation that validates the axioms. The mechanization makes it possible to show that one collection of theories is correctly interpreted by another collection of theories under a user-specified interpretation for the uninterpreted types and constants. A theory instance is generated and imported, while the axiom instances are generated as proof obligations to ensure that the interpretation is valid. Interpretations can be used to show that an implementation is a correct refinement of a specification, that an axiomatically defined specification is consistent, or that a axiomatically defined specification captures its intended models. In addition, the theory parameter mechanism has been extended with a notion of theory as parameter so that a theory instance can be given as an actual parameter to an imported theory. Theory interpretations can thus be used to refine an abstract specification or to demonstrate the consistency of an axiomatic theory. In this report we describe the mechanism in detail. This extension is a part of PVS version 3.0, which will be publicly released in mid-2001.

Owre, Sam↗
NASA NTRS1997

Automated Reuse of Scientific Subroutine Libraries through Deductive Synthesis

Systematic software construction offers the potential of elevating software engineering from an art-form to an engineering discipline. The desired result is more predictable software development leading to better quality and more maintainable software. However, the overhead costs associated with the formalisms, mathematics, and methods of systematic software construction have largely precluded their adoption in real-world software development. In fact, many mainstream software development organizations, such as Microsoft, still maintain a predominantly oral culture for software development projects; which is far removed from a formalism-based culture for software development. An exception is the limited domain of safety-critical software, where the high-assuiance inherent in systematic software construction justifies the additional cost. We believe that systematic software construction will only be adopted by mainstream software development organization when the overhead costs have been greatly reduced. Two approaches to cost mitigation are reuse (amortizing costs over many applications) and automation. For the last four years, NASA Ames has funded the Amphion project, whose objective is to automate software reuse through techniques from systematic software construction. In particular, deductive program synthesis (i.e., program extraction from proofs) is used to derive a composition of software components (e.g., subroutines) that correctly implements a specification. The construction of reuse libraries of software components is the standard software engineering solution for improving software development productivity and quality.

Lowry, Michael R.↗
NASA NTRS2020

Very High Resolution, Altitude-Corrected, TMPA-Based Monthly Satellite Precipitation Product Over the CONUS

The Tropical Rainfall Measuring Mission (TRMM) Multisatellite Precipitation Analysis (TMPA) product provided over 17 years of gridded precipitation datasets. However, the accuracy and spatial resolution of TMPA limits the applicability in hydrometeorological applications. We present a dataset that enhances the accuracy and spatial resolution of the TMPA monthly product (3B43). We resample the TMPA data to a 1 km grid and apply a correction function derived from the Parameter-elevation Regressions on Independent Slopes Model (PRISM) to reduce bias in the data. We confirm a linear relationship between bias and elevation above 1,500 meters where TMPA underestimates measured precipitation, providing a proof-of-concept of how simple linear scaling can be used to augment existing satellite datasets. The result of the correction is the High-Resolution Altitude-Corrected Precipitation product (HRAC-Precip) for the CONUS. Using 9,200 precipitation stations from the Global Historical Climatology Network (GHCN), we compare the accuracy of TMPA 3B43 versus the new HRAC-Precip product. The results show an improvement of the mean absolute error of 12.98% on average.

Hossein Hashemi↗
NASA NTRSDate not supplied

Phase-change Reconfigurable Optical WavEfront Synthesis System (PROWESS)

We report the design, fabrication, and testing of electrically tunable metasurface k-space filters based on the low-loss, high-contrast phase-change material GSST and a transparent Si electrode heating architecture. A 10x10 array of PCM elements integrated with Si heaters was fabricated via foundry processes, and used to actively control the crystallinity of a metasurface consisting of GSST nano antennae. By selectively varying the structural state of individual PCM elements, specific k-vectors of transmitted light can effectively be filtered out, resulting in improved imaging quality by reducing the scattered light that reaches a detector. Optimized doping profiles in the Si heaters allow for uniform, low power, reliable and repeatable switching of the GSST state. Compared to other k-space filters, this new architecture is completely transparent to the wavelength of interest and can be actively reconfigured in real time with high performance, low power consumption and a small footprint. The 10x10 array device is a proof-of-concept demonstration that can enable high-resolution arbitrary wavefront synthesis and correction in the future, with key applications in optical communications, beam steering, remote sensing, and adaptive optics.

phase change material↗
NASA NTRS1991

High Level Design Proof of a Reliable Computing Platform

An architecture for fault-tolerant computing is formalized and shown to satisfy a key correctness property. The reliable computing platform uses replicated processors and majority voting to achieve fault tolerance. Under the assumption of a majority of processors working in each frame, we show that the replicated system computes the same results as a single processor system not subject to failures. Sufficient conditions are obtained to establish that the replicated system recovers from transient faults within a bounded amount of time. Three different voting schemes are examined and proved to satisfy the bounded recovery time conditions.

DiVito, Ben L.↗
NASA NTRS2008

Large-Scale Simulations and Detailed Flow Field Measurements for Turbomachinery Aeroacoustics

The presentation is a review of recent work in highly loaded compressors, turbine aeroacoustics and cooling fan noise. The specific topics are: the importance of correct numerical modeling to capture blade row interactions in the Ultra Efficient Engine Technology Proof-of-Concept Compressor, the attenuation of a detonation pressure wave by an aircraft axial turbine stage, current work on noise sources and acoustic attenuation in turbines, and technology development work on cooling fans for spaceflight applications. The topic areas were related to each other by certain themes such as the advantage of an experimentalist s viewpoint when analyzing numerical simulations and the need to improve analysis methods for very large numerical datasets.

VanZante, Dale↗
NASA NTRS2019

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.↗
NASA NTRS1983

Verification of Numerical Algorithms

The following strategy is suggested for specification and proof: (1) Defer the construction of a formal program specification with respect to I/O assertions unit the correctness of the program with respect to an abstract mathematical model of program intent is demonstrated. (2) Prove that an abstract machine (using infinite precision arithmetic) would compute that object exactly. (3) Prove that the computational sequences of arithmetic operations that occur in the abstract machine must be precisely the same at every step as those occurring on an actual machine (with finite precision arithmetic), executing the same program. (4) Use a Verification Conditions VC-generator that knows about the semantics of arithmetic operations to annotate the program with assertions that bound (or in some circumstances estimate) the difference between the actual machine state variables and the corresponding ones of the abstract machine. Construct the formal program specification by combining the verification conditions into theorems about computational error that can be proved with mechanical assistance.

Source record↗