SEARCH · Engineering Papers

Results for “formal”

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.

SourceResearch connectionFrom yearThrough year

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

At least 271 records · Page 15

All sources NASA NTRS DOE OSTI

NASA NTRS1993

Using Penelope to assess the correctness of NASA Ada software: A demonstration of formal methods as a counterpart to testing

Life-critical applications warrant a higher level of software reliability than has yet been achieved. Since it is not certain that traditional methods alone can provide the required ultra reliability, new methods should be examined as supplements or replacements. This paper describes a mathematical counterpart to the traditional process of empirical testing. ORA's Penelope verification system is demonstrated as a tool for evaluating the correctness of Ada software. Grady Booch's Ada calendar utility package, obtained through NASA, was specified in the Larch/Ada language. Formal verification in the Penelope environment established that many of the package's subprograms met their specifications. In other subprograms, failed attempts at verification revealed several errors that had escaped detection by testing.

Eichenlaub, Carl T.↗

NASA NTRS1992

On Vasyliunas's equivalent conductivity formalism

The Vasyliunas's (1972) equivalent conductivity formalism (ECF) for representing the coupling of the ionosphere and the magnetosphere is discussed, and a new, simpler, derivation is presented of the ECF, in which certain of the underlying assumptions and their implications are made transparent. The derivation presented indicates that the only role of the ions in the ECF is to insure quasi-neutrality. It is shown that the ECF is not as robust as usually assumed and that caution must be used to insure that reasonable results are obtained.

Pontius, D. H., Jr.↗

NASA NTRS1993

A theory of nonlocal mixing-length convection. I - The moment formalism

A flexible and potentially powerful theory of convection, based on the mixing length picture, is developed to make unbiased self-consistent predictions about overshooting and other complicated phenomena in convection. The basic formalism is set up, and the method's power is demonstrated by showing that a simplified version of the theory reproduces all the standard results of local convection. The second-order equations of the theory are considered in the limit of a steady state and vanishing third moments, and it is shown that they reproduce all the standard results of local mixing-length convection. There is a particular value of the superadiabatic gradient, below which the only possible steady state of a fluid is nonconvecting. Above this critical value, a fluid is convectively unstable. Two distinct regimes of convection, which are identified as efficient and inefficient convection, are determined.

Grossman, Scott A.↗

NASA NTRS1992

A new nonlinear diffusion formalism in a magnetized plasma - Application to space physics and astrophysics

A novel diffusion formalism that takes into account the finite width of resonances is presented. The resonance diagram technique is shown to reproduce the details of the particle orbits very accurately, and can be used to determine the acceleration/scattering in the presence of a given wave spectrum. Ways in which the nonlinear orbits can be incorporated into the diffusion equation are shown. The resulting diffusion equation is an extension of the Q-L theory to cases where the waves have large amplitudes and/or are coherent. This new equation does not have a gap at 90 deg in cases where the individual orbits can cross the gap. The conditions under which the resonance gap at 90-deg pitch angle exits are also examined.

Karimbadi, H.↗

NASA NTRS1993

On a Lagrange-Hamilton formalism describing position and momentum uncertainties

According to Heisenberg's uncertainty relation, in quantum mechanics it is not possible to determine, simultaneously, exact values for the position and the momentum of a material system. Calculating the mean value of the Hamiltonian operator with the aid of exact analytic Gaussian wave packet solutions, these uncertainties cause an energy contribution additional to the classical energy of the system. For the harmonic oscillator, e.g., this nonclassical energy represents the ground state energy. It will be shown that this additional energy contribution can be considered as a Hamiltonian function, if it is written in appropriate variables. With the help of the usual Lagrange-Hamilton formalism known from classical particle mechanics, but now considering this new Hamiltonian function, it is possible to obtain the equations of motion for position and momentum uncertainties.

Schuch, Dieter↗

NASA NTRS1992

Formally biorthogonal polynomials and a look-ahead Levinson algorithm for general Toeplitz systems

Systems of linear equations with Toeplitz coefficient matrices arise in many important applications. The classical Levinson algorithm computes solutions of Toeplitz systems with only O(n(sub 2)) arithmetic operations, as compared to O(n(sub 3)) operations that are needed for solving general linear systems. However, the Levinson algorithm in its original form requires that all leading principal submatrices are nonsingular. An extension of the Levinson algorithm to general Toeplitz systems is presented. The algorithm uses look-ahead to skip over exactly singular, as well as ill-conditioned leading submatrices, and, at the same time, it still fully exploits the Toeplitz structure. In our derivation of this algorithm, we make use of the intimate connection of Toeplitz matrices with formally biorthogonal polynomials.

Freund, Roland W.↗

NASA NTRS1993

A formal language for the specification and verification of synchronous and asynchronous circuits

A formal hardware description language for the intended application of verifiable asynchronous communication is described. The language is developed within the logical framework of the Nqthm system of Boyer and Moore and is based on the event-driven behavioral model of VHDL, including the basic VHDL signal propagation mechanisms, the notion of simulation deltas, and the VHDL simulation cycle. A core subset of the language corresponds closely with a subset of VHDL and is adequate for the realistic gate-level modeling of both combinational and sequential circuits. Various extensions to this subset provide means for convenient expression of behavioral circuit specifications.

Russinoff, David M.↗

NASA NTRS1991

Formal verification of an MMU and MMU cache

We describe the formal verification of a hardware subsystem consisting of a memory management unit and a cache. These devices are verified independently and then shown to interact correctly when composed. The MMU authorizes memory requests and translates virtual addresses to real addresses. The cache improves performance by maintaining a LRU (least recently used) list from the memory resident segment table.

Schubert, E. T.↗

NASA NTRS1991

Formal specification of a high speed CMOS correlator

The formal specification of a high speed CMOS correlator is presented. The specification gives the high-level behavior of the correlator and provides a clear, unambiguous description of the high-level architecture of the device.

Windley, P. J.↗

NASA NTRS1994

Interpreter composition issues in the formal verification of a processor-memory module

This report describes interpreter composition techniques suitable for the formal specification and verification of a processor-memory module using the HOL theorem proving system. The processor-memory module is a multichip subsystem within a fault-tolerant embedded system under development within the Boeing Defense and Space Group. Modeling and verification methods were developed that permit provably secure composition at the transaction-level of specification, significantly reducing the complexity of the hierarchical verification of the system.

Fura, David A.↗

NASA NTRS1994

A robot control formalism based on an information quality concept

A relevance measure based on Jaynes maximum entropy principle is introduced. Information quality is the conjunction of accuracy and relevance. The formalism based on information quality is developed for one-agent applications. The robot requires a well defined working environment where properties of each object must be accurately specified.

Ekman, A.↗

NASA NTRS1994

Open architectures for formal reasoning and deductive technologies for software development

The objective of this project is to develop an open architecture for formal reasoning systems. One goal is to provide a framework with a clear semantic basis for specification and instantiation of generic components; construction of complex systems by interconnecting components; and for making incremental improvements and tailoring to specific applications. Another goal is to develop methods for specifying component interfaces and interactions to facilitate use of existing and newly built systems as 'off the shelf' components, thus helping bridge the gap between producers and consumers of reasoning systems. In this report we summarize results in several areas: our data base of reasoning systems; a theory of binding structures; a theory of components of open systems; a framework for specifying components of open reasoning system; and an analysis of the integration of rewriting and linear arithmetic modules in Boyer-Moore using the above framework.

Mccarthy, John↗

NASA NTRS1994

Two space scatterer formalism calculation of bulk parameters of thunderclouds

In a previous study, we used a modified two-space scatterer formalism of Twersky to establish for a cloud modeled as a statistically homogeneous distribution of spherical water droplets, the dispersion relations that determine its bulk propagation numbers and bulk indexes of refraction in terms of the vector equivalent scattering amplitude and the dyadic scattering amplitude of the single water droplet in isolation. The results were specialized to the forward direction of scattering while demanding that the scatterers preserve the incident polarization. We apply this approach to obtain specific numerical values for the macroscopic parameters of the cloud. We work with a cloud of density rho = 100 cm(exp -3), a wavelength lambda = 0.7774 microns, and with spherical water droplets of common radius alpha = 10 microns. In addition, the scattering medium is divided into three parts, the medium outside the cloud, moist air (the medium inside the cloud but outside the droplets), and the medium inside the spherical water droplets. The results of this report are applicable to a cloud of any geometry since the boundary does not interfere with the calculations. Also, it is important to notice the plane wave nature of the incidence wave in the moist atmosphere.

Phanord, Dieudonne D.↗

NASA NTRS1995

Towards a formal semantics for Ada 9X

The Ada 9X language precision team was formed during the revisions of Ada 83, with the goal of analyzing the proposed design, identifying problems, and suggesting improvements, through the use of mathematical models. This report defines a framework for formally describing Ada 9X, based on Kahn's 'natural semantics', and applies the framework to portions of the language. The proposals for exceptions and optimization freedoms are also analyzed, using a different technique.

Guaspari, David↗

NASA NTRS1996

A Formal Algorithm for Routing Traces on a Printed Circuit Board

This paper addresses the classical problem of printed circuit board routing: that is, the problem of automatic routing by a computer other than by brute force that causes the execution time to grow exponentially as a function of the complexity. Most of the present solutions are either inexpensive but not efficient and fast, or efficient and fast but very costly. Many solutions are proprietary, so not much is written or known about the actual algorithms upon which these solutions are based. This paper presents a formal algorithm for routing traces on a print- ed circuit board. The solution presented is very fast and efficient and for the first time speaks to the question eloquently by way of symbolic statements.

Hedgley, David R., Jr.↗

NASA NTRS1997

Fourth NASA Langley Formal Methods Workshop

This publication consists of papers presented at NASA Langley Research Center's fourth workshop on the application of formal methods to the design and verification of life-critical systems. Topic considered include: Proving properties of accident; modeling and validating SAFER in VDM-SL; requirement analysis of real-time control systems using PVS; a tabular language for system design; automated deductive verification of parallel systems. Also included is a fundamental hardware design in PVS.

Holloway, C. Michael↗

NASA NTRS1999

Detecting Mode Confusion Through Formal Modeling and Analysis

Aircraft safety has improved steadily over the last few decades. While much of this improvement can be attributed to the introduction of advanced automation in the cockpit, the growing complexity of these systems also increases the potential for the pilots to become confused about what the automation is doing. This phenomenon, often referred to as mode confusion, has been involved in several accidents involving modern aircraft. This report describes an effort by Rockwell Collins and NASA Langley to identify potential sources of mode confusion through two complementary strategies. The first is to create a clear, executable model of the automation, connect it to a simulation of the flight deck, and use this combination to review of the behavior of the automation and the man-machine interface with the designers, pilots, and experts in human factors. The second strategy is to conduct mathematical analyses of the model by translating it into a formal specification suitable for analysis with automated tools. The approach is illustrated by applying it to a hypothetical, but still realistic, example of the mode logic of a Flight Guidance System.

Miller, Steven P.↗

NASA NTRS1998

An Integrated Environment for Efficient Formal Design and Verification

The general goal of this project was to improve the practicality of formal methods by combining techniques from model checking and theorem proving. At the time the project was proposed, the model checking and theorem proving communities were applying different tools to similar problems, but there was not much cross-fertilization. This project involved a group from SRI that had substantial experience in the development and application of theorem-proving technology, and a group at Stanford that specialized in model checking techniques. Now, over five years after the proposal was submitted, there are many research groups working on combining theorem-proving and model checking techniques, and much more communication between the model checking and theorem proving research communities. This project contributed significantly to this research trend. The research work under this project covered a variety of topics: new theory and algorithms; prototype tools; verification methodology; and applications to problems in particular domains.

Source record↗