Engineering Papers⌕ Search

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.

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

At least 397 records · Page 22
All sourcesNASA NTRSDOE OSTI
NASA NTRS1991

A Variational Formalism for the Radiative Transfer Equation: Prelude to Model 3

The MODEL III variational data assimilation model is the third of four general assimilation models designed to blend weather data measured from space based platforms in the meteorological data mainstream in a way that maximizes the information content of the satellite data. Because there are many different observation locations and there are many instruments with different measurement error characteristics, it is also necessary to require that the blending be done to maximize the information content of the data and simultaneously to retain a dynamically consistent and reasonably accurate description of the state of the atmosphere. This is ideally a variational problem for which the data receive relative weights that are inversely proportional to measurement error and are adjusted to satisfy a set of dynamical equations that govern atmospheric processes. The advantage of MODEL III over the previous two models is that radiance, the atmospheric variable measured by satellite, becomes a dependent variable. In the previous versions, mean layer temperatures that had been retrieved from the radiances by some method, were included in the assimilation by substituting them in place of the rawinsonde temperatures. Now both rawinsonde temperatures and satellite radiances are included independently in the assimilation.

Achtemeier, Gary L.↗
NASA NTRS1991

A Variational Formalism for the Radiative Transfer Equation and a Geostrophic, Hydrostatic Atmosphere: Prelude to Model 3

The second step in development of MODEL III is summarized. It combines the four radiative transfer equations of the first step with the equations for a geostrophic and hydrostatic atmosphere. This step is intended to bring radiance into a three dimensional balance with wind, height, and temperature. The use of the geostrophic approximation in place of the full set of primitive equations allows for an easier evaluation of how the inclusion of the radiative transfer equation increases the complexity of the variational equations. Seven different variational formulations were developed for geostrophic, hydrostatic, and radiative transfer equations. The first derivation was too complex to yield solutions that were physically meaningful. For the remaining six derivations, the variational method gave the same physical interpretation (the observed brightness temperatures could provide no meaningful input to a geostrophic, hydrostatic balance) at least through the problem solving methodology used in these studies. The variational method is presented and the Euler-Lagrange equations rederived for the geostrophic, hydrostatic, and radiative transfer equations.

Achtemeier, Gary L.↗
NASA NTRS1992

Formal verification of a set of memory management units

This document describes the verification of a set of memory management units (MMU). The verification effort demonstrates the use of hierarchical decomposition and abstract theories. The MMUs can be organized into a complexity hierarchy. Each new level in the hierarchy adds a few significant features or modifications to the lower level MMU. The units described include: (1) a page check translation look-aside module (TLM); (2) a page check TLM with supervisor line; (3) a base bounds MMU; (4) a virtual address translation MMU; and (5) a virtual address translation MMU with memory resident segment table.

Schubert, E. Thomas↗
NASA NTRS1991

IDEF3 formalization report

The Process Description Capture Method (IDEF3) is one of several Integrated Computer-Aided Manufacturing (ICAM) DEFinition methods developed by the Air Force to support systems engineering activities, and in particular, to support information systems development. These methods have evolved as a distillation of 'good practice' experience by information system developers and are designed to raise the performance level of the novice practitioner to one comparable with that of an expert. IDEF3 is meant to serve as a knowledge acquisition and requirements definition tool that structures the user's understanding of how a given process, event, or system works around process descriptions. A special purpose graphical language accompanying the method serves to highlight temporal precedence and causality relationships relative to the process or event being described.

Menzel, Christopher↗
NASA NTRS1990

Formal mathematical solutions of the force-free equations, spontaneous discontinuities, and dissipation in large-scale magnetic fields

Direct integration of the force-free field equation del x B = alpha B, in the simple case of the local deformation of a laminar field, produces field configurations containing tangential discontinuities (current sheets). Whereas continuous solutions allow only restricted field topologies, the discontinuities provide the necessary release from those restrictions in more general topologies. Magnetic fields in nature are strongly deformed by convection, so as to contain significant internal discontinuities. The bipolar magnetic fields containing the active X-ray corona of the sun are a case in point. It appears that the dissipation caused by the discontinuities may be the primary heat source producing the X-ray corona.

Parker, E. N.↗
NASA NTRS1993

Curvature-Squared Cosmology In The First-Order Formalism

Paper presents theoretical study of some of general-relativistic ramifications of gravitational-field energy density proportional to R - alpha R(exp 2) (where R is local scalar curvature of space-time and alpha is a constant).

Shahid-Saless, Bahman↗
NASA NTRS1992

Formalization and visualization of domain-specific software architectures

This paper describes a domain-specific software design system based on the concepts of software architectures engineering and domain-specific models and languages. In this system, software architectures are used as high level abstractions to formulate a domain-specific software design. The software architecture serves as a framework for composing architectural fragments (e.g., domain objects, system components, and hardware interfaces) that make up the knowledge (or model) base for solving a problem in a particular application area. A corresponding software design is generated by analyzing and describing a system in the context of the software architecture. While the software architecture serves as the framework for the design, this concept is insufficient by itself for supplying the additional details required for a specific design. Additional domain knowledge is still needed to instantiate components of the architecture and develop optimized algorithms for the problem domain. One possible way to obtain the additional details is through the use of domain-specific languages. Thus, the general concept of a software architecture and the specific design details provided by domain-specific languages are combined to create what can be termed a domain-specific software architecture (DSSA).

Bailor, Paul D.↗
NASA NTRS1993

Formal verification of a microcoded VIPER microprocessor using HOL

The Royal Signals and Radar Establishment (RSRE) and members of the Hardware Verification Group at Cambridge University conducted a joint effort to prove the correspondence between the electronic block model and the top level specification of Viper. Unfortunately, the proof became too complex and unmanageable within the given time and funding constraints, and is thus incomplete as of the date of this report. This report describes an independent attempt to use the HOL (Cambridge Higher Order Logic) mechanical verifier to verify Viper. Deriving from recent results in hardware verification research at UC Davis, the approach has been to redesign the electronic block model to make it microcoded and to structure the proof in a series of decreasingly abstract interpreter levels, the lowest being the electronic block level. The highest level is the RSRE Viper instruction set. Owing to the new approach and some results on the proof of generic interpreters as applied to simple microprocessors, this attempt required an effort approximately an order of magnitude less than the previous one.

Levitt, Karl↗
NASA NTRS1993

Towards the formal verification of the requirements and design of a processor interface unit: HOL listings

This technical report contains the Higher-Order Logic (HOL) listings of the partial verification of the requirements and design for a commercially developed processor interface unit (PIU). The PIU is an interface chip performing memory interface, bus interface, and additional support services for a commercial microprocessor within a fault tolerant computer system. This system, the Fault Tolerant Embedded Processor (FTEP), is targeted towards applications in avionics and space requiring extremely high levels of mission reliability, extended maintenance-free operation, or both. This report contains the actual HOL listings of the PIU verification as it currently exists. Section two of this report contains general-purpose HOL theories and definitions that support the PIU verification. These include arithmetic theories dealing with inequalities and associativity, and a collection of tactics used in the PIU proofs. Section three contains the HOL listings for the completed PIU design verification. Section 4 contains the HOL listings for the partial requirements verification of the P-Port.

Fura, David A.↗
NASA NTRS1993

Towards the formal specification of the requirements and design of a processor interface unit: HOL listings

This technical report contains the HOL listings of the specification of the design and major portions of the requirements for a commercially developed processor interface unit (or PIU). The PIU is an interface chip performing memory interface, bus interface, and additional support services for a commercial microprocessor within a fault-tolerant computer system. This system, the Fault-Tolerant Embedded Processor (FTEP), is targeted towards applications in avionics and space requiring extremely high levels of mission reliability, extended maintenance-free operation, or both. This report contains the actual HOL listings of the PIU specification as it currently exists. Section two of this report contains general-purpose HOL theories that support the PIU specification. These theories include definitions for the hardware components used in the PIU, our implementation of bit words, and our implementation of temporal logic. Section three contains the HOL listings for the PIU design specification. Aside from the PIU internal bus (I-Bus), this specification is complete. Section four contains the HOL listings for a major portion of the PIU requirements specification. Specifically, it contains most of the definition for the PIU behavior associated with memory accesses initiated by the local processor.

Fura, David A.↗
NASA NTRS1994

Formal semantics for a subset of VHDL and its use in analysis of the FTPP scoreboard circuit

In the first part of the report, we give a detailed description of an operational semantics for a large subset of VHDL, the VHSIC Hardware Description Language. The semantics is written in the functional language Caliban, similar to Haskell, used by the theorem prover Clio. We also describe a translator from VHDL into Caliban semantics and give some examples of its use. In the second part of the report, we describe our experience in using the VHDL semantics to try to verify a large VHDL design. We were not able to complete the verification due to certain complexities of VHDL which we discuss. We propose a VHDL verification method that addresses the problems we encountered but which builds on the operational semantics described in the first part of the report.

Bickford, Mark↗
NASA NTRS1994

Epistemology, software engineering and formal methods

One of the most basic questions anyone can ask is, 'How do I know that what I think I know is true?' The study of this question is called epistemology. Traditionally, epistemology has been considered to be of legitimate interest only to philosophers, theologians, and three year old children who respond to every statement by asking, 'Why?' Software engineers need to be interested in the subject, however, because a lack of sufficient understanding of epistemology contributes to many of the current problems in the field.

Holloway, C. Michael↗
NASA NTRS1994

A spectral formalism for computing three-dimensional deformations due to surface loads. 2: Present-day glacial isostatic adjustment

Using a spherically symmetric, self-gravitating, linear viscoelastic Earth model, we predict present-day three-dimensional surface deformation rates and baseline evolutions arising as a consequence of the late Pleistocene glacial cycles. In general, we use realistic models for the space-time geometry of the final late Pleistocene deglaciation event and incorporate a gravitationally self-consistent ocean meltwater redistribution. The predictions of horizontal velocity presented differ significantly, in both their amplitude and their spatial variation, from those presented in earlier analysis of others which adopted simplified models of both the late Pleistocene ice history and the Earth rheology. An important characteristic of our predicted velocity fields is that the melting of the Laurentide ice sheet over Canada is capable of contributing appreciably to the adjustment in Europe. The sensitivity of the predictions to variations in mantle rheology is investigated by considering a number of different Earth models, and by computing appropriate Frechet kernels. These calculations suggest that the sensitivity of the deformations to the Earth's rheology is significant and strongly dependent on the location of the site relative to the ancient ice sheet. The effects on the predictions of three-dimensional deformation rates of altering the ice history or adopting approximate models for the ocean meltwater redistribution have also been considered and found to be important (the former especially so). Finally, for a suite of Earth models we provide predictions of the velocity of a number of baselines in North America and Europe. We find that, in general, both radial and tangential motions contribute significantly to baseline length changes, and that these contributions are a strong function of the Earth model. We have, furthermore, found a set of Earth models which, together with the ICE-3G deglaciation chronology, produce predictions of baseline length changes that are consistent with very long baseline interferometry measurements of baselines within Europe.

Mitrovica, J. X.↗
NASA NTRS1999

Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL

A real-time system for power-down control in audio/video components is modeled and verified using the real-time model checker UPPAAL. The system is supposed to reside in an audio/video component and control (read from and write to) links to neighbor audio/video components such as TV, VCR and remote-control. In particular, the system is responsible for the powering up and down of the component in between the arrival of data, and in order to do so in a safe way without loss of data, it is essential that no link interrupts are lost. Hence, a component system is a multitasking system with hard real-time requirements, and we present techniques for modeling time consumption in such a multitasked, prioritized system. The work has been carried out in a collaboration between Aalborg University and the audio/video company B&O. By modeling the system, 3 design errors were identified and corrected, and the following verification confirmed the validity of the design but also revealed the necessity for an upper limit of the interrupt frequency. The resulting design has been implemented and it is going to be incorporated as part of a new product line.

Havelund, Klaus↗
NASA NTRS2002

The Role of Formal Experiment Design in Hypersonic Flight System Technology Development

Hypersonic airbreathing engine (scramjet) powered vehicles are being considered to replace conventional rocket-powered launch systems. Effective utilization of scramjet engines requires careful integration with the air vehicle. This integration synergistically combines aerodynamic forces with propulsive cycle functions of the engine. Due to the highly integrated nature of the hypersonic vehicle design problem, the large flight envelope, and the large number of design variables, the use of a statistical design approach in design is effective. Modern Design-of-Experiments (MDOE) has been used throughout the Hyper-X program, for both systems analysis and experimental testing. Application of MDOE fall into four categories: (1) experimental testing; (2) studies of unit phenomena; (3) refining engine design; and (4) full vehicle system optimization. The MDOE process also provides analytical models, which are also used to document lessons learned, supplement low-level design tools, and accelerate future studies. This paper will discuss the design considerations for scramjet-powered vehicles, specifics of MDOE utilized for Hyper-X, and present highlights from the use of these MDOE methods within the Hyper-X Program.

McClinton, Charles R.↗
NASA NTRS1999

Formal Models of Blur Detection

This paper presents a review and comparison of the engineering and physiological optics literature on defocus detection. The equivalence of spatial frequency based detectors and the edge-based hypothesis, and variance-based detectors and the contrast- difference hypothesis is argued. Finally, variance-invariant transforms are introduced as a means of experimentally differentiating the hypotheses.

Neveu, Charles F.↗
NASA NTRS1998

Formal Analysis of Human Automation Interaction: The Problem of Display Correctness

This presentation attempted to develop a quantitative method for evaluating the effectiveness of autoflight displays. Researchers sought to develop a methodology for evaluation of display correctness and develop a methodology for display synthesis. Topics covered included: mode awareness, industry/research contributions, human-machine interface analysis, research objectives, modeling, flight guidance project and evaluation.

Degani, Asaf↗