SEARCH · Engineering Papers
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.
A parameterized definition of subtractive floating point division algorithms is presented and verified using PVS. The general algorithm is proven to satisfy a formal definition of an IEEE standard for floating point arithmetic. The utility of the general specification is illustrated using a number of different instances of the general algorithm.
We describe a recent NASA-sponsored pilot project intended to gauge the effectiveness of using formal methods in Space Shuttle software requirements analysis. Several Change Requests (CRs) were selected as promising targets to demonstrate the utility of formal methods in this demanding application domain. A CR to add new navigation capabilities to the Shuttle, based on Global Positioning System (GPS) technology, is the focus of this industrial usage report. Portions of the GPS CR were modeled using the language of SRI's Prototype Verification System (PVS). During a limited analysis conducted on the formal specifications, numerous requirements issues were discovered. We present a summary of these encouraging results and conclusions we have drawn from the pilot project.
This paper presents the formal verification of a new protocol for online distributed diagnosis for the SPIDER family of architectures. An instance of the Scalable Processor-Independent Design for Electromagnetic Resilience (SPIDER) architecture consists of a collection of processing elements communicating over a Reliable Optical Bus (ROBUS). The ROBUS is a specialized fault-tolerant device that guarantees Interactive Consistency, Distributed Diagnosis (Group Membership), and Synchronization in the presence of a bounded number of physical faults. Formal verification of the original SPIDER diagnosis protocol provided a detailed understanding that led to the discovery of a significantly more efficient protocol. The original protocol was adapted from the formally verified protocol used in the MAFT architecture. It required O(N) message exchanges per defendant to correctly diagnose failures in a system with N nodes. The new protocol achieves the same diagnostic fidelity, but only requires O(1) exchanges per defendant. This paper presents this new diagnosis protocol and a formal proof of its correctness using PVS.
Crack formation in the space shuttle's heat shield during flight poses a major safety concern to everyone on board. Cracking weakens the structure of the shield and lessens the protection it offers against the high temperatures and forces encountered during re-entry. Astronauts need a way to mend these cracks while in space. This is GRABER s function; it can be spackled into the cracks by an astronaut. The material then hardens, or cures, due to being in a vacuum and the heat encountered when it faces the sun. A great deal of work and testing is necessary to create a material that will be workable in a vacuum over a wide range of temperatures, will cure without cracking, will adhere to the sides of the crack, and that can withstand the extreme temperatures of re-entry. A Brookfield PVS Rheometer is being used to characterize GRABER's viscosity at various temperatures and stirring rates. Various compositions of GRABER are being heat treated in a vacuum to determine probably curing times in space. The microstructures of cured samples of each composition are being examined using both optical and electron microscopy. Jupiter s Icy Moon Orbiter (JIMO) will be lifting off sometime around 2013. JIMO will have more power than its predecessor, Galileo, allowing it to change orbits to circle three of Jupiter s moons. Both of the engine types being considered require large heat dissipation systems. These systems will be comprised of heat conductive tubing and plates with a liquid flowing through them. In order to maximize the speed of heat transfer between the tubes and the panels, the in-between areas will be filled with heat conductive silicon carbide foam. Two different foam systems are being considered for this foam. Currently, experimentation is underway with adding Sic, carbon, and carbon fibers to a two part fuel retardant foam. The foam is them pyrolized and its mass and dimensional changes are measured. The structure of the foam will be examined using optical and electron microscopy as well. Work is also planned with a foam system developed by an Italian team.
A critical factor in the adoption of any new aeronautical technology or concept of operation is safety. Traditionally, safety is accomplished through a rigorous process that involves human factors, low and high fidelity simulations, and flight experiments. As this process is usually performed on final products or functional prototypes, concept modifications resulting from this process are very expensive to implement. This paper describe an approach to system safety that can take place at early stages of a concept design. It is based on a set of mathematical techniques and tools known as formal methods. In contrast to testing and simulation, formal methods provide the capability of exhaustive state exploration analysis. We present the safety analysis and verification performed for the Small Aircraft Transportation System (SATS) Concept of Operations (ConOps). The concept of operations is modeled using discrete and hybrid mathematical models. These models are then analyzed using formal methods. The objective of the analysis is to show, in a mathematical framework, that the concept of operation complies with a set of safety requirements. It is also shown that the ConOps has some desirable characteristic such as liveness and absence of dead-lock. The analysis and verification is performed in the Prototype Verification System (PVS), which is a computer based specification language and a theorem proving assistant.
This paper proposes a challenge problem in disproving. We describe a fault-tolerant distributed protocol designed at NASA for use in a fly-by-wire system for next-generation commercial aircraft. An early design of the protocol contains a subtle bug that is highly unlikely to be caught in fault injection testing. We describe a failed proof of the protocol's correctness in a mechanical theorem prover (PVS) with a complex unfinished proof conjecture. We use a model checking suite (SAL) to generate a concrete counterexample to the unproven conjecture to demonstrate the existence of a bug. However, we argue that the effort required in our approach is too high and propose what conditions a better solution would satisfy. We carefully describe the protocol and bug to provide a challenging but feasible case study for disproving research.
We present a mathematical framework for the specification and verification of state-based conflict resolution algorithms that recover from loss of separation. In particular, we propose rigorous definitions of horizontal and vertical maneuver correctness that yield horizontal and vertical separation, respectively, in a bounded amount of time. We also provide sufficient conditions for independent correctness, i.e., separation under the assumption that only one aircraft maneuvers, and for implicitly coordinated correctness, i.e., separation under the assumption that both aircraft maneuver. An important benefit of this approach is that different aircraft can execute different algorithms and implicit coordination will still be achieved, as long as they all meet the explicit criteria of the framework. Towards this end we have sought to make the criteria as general as possible. The framework presented in this paper has been formalized and mechanically verified in the Prototype Verification System (PVS).
The purpose of this project is to characterize and correlate Electrostatic Discharge (ESD) sensitivity levels of an Integrated Circuit (IC) package using Transmission Line Pulse (TLP) and Human Body Model (HBM) methods. This characterization will be used as a baseline ESD sensitivity level to demonstrate improvement to the ESD sensitivity of the IC package through the use of EPI-FLO(Trade Mark) Polymer Voltage Suppression (PVS) protection devices developed and manufactured by Electronic Polymers, Inc. (EPI).
A concept of operations for air traffic management consists of a set of flight rules and procedures aimed to keep aircraft safely separated. This paper reports on the formal verification of separation properties of the NASA's Small Aircraft Transportation System, Higher Volume Operations (SATS HVO) concept for non-towered, non-radar airports. Based on a geometric description of the SATS HVO air space, we derive analytical formulas to compute spacing requirements on nominal approaches. Then, we model the operational concept by a hybrid non-deterministic asynchronous state transition system. Using an explicit state exploration technique, we show that the spacing requirements are always satisfied on nominal approaches. All the mathematical development presented in this paper has been formally verified in the Prototype Verification System (PVS). Keywords. Formal verification, hybrid systems, air traffic management, theorem proving
An important goal of NASA's Internal Vehicle Health Management program (IVHM) is to develop and verify methods and technologies for fault detection in critical airframe structures. A particularly promising new technology under development at NASA Langley Research Center is distributed Bragg fiber optic strain sensors. These sensors can be embedded in, for instance, aircraft wings to continuously monitor surface strain during flight. Strain information can then be used in conjunction with well-known vibrational techniques to detect faults due to changes in the wing's physical parameters or to the presence of incipient cracks. To verify the benefits of this technology, the Formal Methods Group at NASA LaRC has proposed the use of formal verification tools such as PVS. The verification process, however, requires knowledge of the physics and mathematics of the vibrational techniques and a clear understanding of the particular fault detection methodology. This report presents a succinct review of the physical principles behind the modeling of vibrating structures such as cantilever beams (the natural model of a wing). It also reviews two different classes of fault detection techniques and proposes a particular detection method for cracks in wings, which is amenable to formal verification. A prototype implementation of these methods using Matlab scripts is also described and is related to the fundamental theoretical concepts.
In this paper, we develop and formally verify practical algorithms for recovery from loss of separation. The formal verification is performed in the context of a criteria-based framework. This framework provides rigorous definitions of horizontal and vertical maneuver correctness that guarantee divergence and achieve horizontal and vertical separation. The algorithms are shown to be independently correct, that is, separation is achieved when only one aircraft maneuvers, and implicitly coordinated, that is, separation is also achieved when both aircraft maneuver. In this paper we improve the horizontal criteria over our previous work. An important benefit of the criteria approach is that different aircraft can execute different algorithms and implicit coordination will still be achieved, as long as they all meet the explicit criteria of the framework. Towards this end we have sought to make the criteria as general as possible. The framework presented in this paper has been formalized and mechanically verified in the Prototype Verification System (PVS).
This paper presents the specification and verification in the Prototype Verification System (PVS) of a protocol intended to facilitate communication in an experimental remotely operated vehicle used by NASA researchers. The protocol is defined as a stack-layered com- position of simpler protocols. It can be seen as the vertical composition of protocol layers, where each layer performs input and output message processing, and the horizontal composition of different processes concurrently inhabiting the same layer, where each process satisfies a distinct requirement. It is formally proven that the protocol components satisfy certain delivery guarantees. Compositional techniques are used to prove these guarantees also hold in the composed system. Although the protocol itself is not novel, the methodology employed in its verification extends existing techniques by automating the tedious and usually cumbersome part of the proof, thereby making the iterative design process of protocols feasible.
A technique based on the use of a quantifier elimination decision procedure for real closed fields and simple theorem proving to construct a series of successively finer qualitative abstractions of hybrid automata is taught. The resulting abstractions are always discrete transition systems which can then be used by any traditional analysis tool. The constructed abstractions are conservative and can be used to establish safety properties of the original system. The technique works on linear and non-linear polynomial hybrid systems: the guards on discrete transitions and the continuous flows in all modes can be specified using arbitrary polynomial expressions over the continuous variables. An exemplar tool in the SAL environment built over the theorem prover PVS is detailed. The technique scales well to large and complex hybrid systems.
In this paper we describe a process of algorithmic discovery that was driven by our goal of achieving complete, mechanically verified algorithms that compute conflict prevention bands for use in en route air traffic management. The algorithms were originally defined in the PVS specification language and subsequently have been implemented in Java and C++. We do not present the proofs in this paper: instead, we describe the process of discovery and the key ideas that enabled the final formal proof of correctness
This paper presents the correctness proof of Saturation, an algorithm for generating state spaces of concurrent systems, implemented in the SMART tool. Unlike the Breadth First Search exploration algorithm, which is easy to understand and formalise, Saturation is a complex algorithm, employing a mutually-recursive pair of procedures that compute a series of non-trivial, nested local fixed points, corresponding to a chaotic fixed point strategy. A pencil-and-paper proof of Saturation exists, but a machine checked proof had never been attempted. The key element of the proof is the characterisation theorem of saturated nodes in decision diagrams, stating that a saturated node represents a set of states encoding a local fixed-point with respect to firing all events affecting only the node s level and levels below. For our purpose, we have employed the Prototype Verification System (PVS) for formalising the Saturation algorithm, its data structures, and for conducting the proofs.
In air traffic management, a pairwise conflict is a predicted loss of separation between two aircraft, referred to as the ownship and the intruder. A conflict prevention bands system computes ranges of maneuvers for the ownship that characterize regions in the airspace that are either conflict-free or 'don't go' zones that the ownship has to avoid. Conflict prevention bands are surprisingly difficult to define and analyze. Errors in the calculation of prevention bands may result in incorrect separation assurance information being displayed to pilots or air traffic controllers. This paper presents provably correct 3-dimensional prevention bands algorithms for ranges of track angle; ground speed, and vertical speed maneuvers. The algorithms have been mechanically verified in the Prototype Verification System (PVS). The verification presented in this paper extends in a non-trivial way that of previously published 2-dimensional algorithms.
We provide a framework to bound the probability that accumulated errors were never above a given threshold on numerical algorithms. Such algorithms are used for example in aircraft and nuclear power plants. This report contains simple formulas based on Levy's and Markov's inequalities and it presents a formal theory of random variables with a special focus on producing concrete results. We selected four very common applications that fit in our framework and cover the common practices of systems that evolve for a long time. We compute the number of bits that remain continuously significant in the first two applications with a probability of failure around one out of a billion, where worst case analysis considers that no significant bit remains. We are using PVS as such formal tools force explicit statement of all hypotheses and prevent incorrect uses of theorems.
This new utility patent is an active design that relies on the lung's role as an organic heat exchanger for providing deep body core heating of air. It is based on the fact that the greatest heat loss mechanism for an insulated human body immersed in a cold water environment is due to heat loss through respiration. This innovation successfully merges two existing technologies (cold immersion suit and existing valve technologies) to produce a new product that helps prevent against the onset of hypothermia at sea. During normal operations, a human maintains an approximate body temperature of [98.6 F (37 C)]. A mechanism was developed to recover the warm temperature from the body and reticulate it in a survival suit. The primary intention is to develop an encompassing systems design that can both easily and cost effectively be integrated in all existing currently manufactured cold water survival suits, and as such, it should be noted that the cold water immersion suit is only used as a framework or tool for laying out the required design elements. At the heart of the suit is the Warm Air Recovery (WAR) system, which relies on a single, large Main Purge Valve (MPV) and secondary Purge Valves (PV) to operate. The main purge valve has a thin membrane, which is normally closed, and acts as a one-way check valve. When warm air is expelled from the lungs, it causes the main purge valve to open. Air forced from the MPV is dumped directly into the suit, thereby providing warmth to the torso, legs, and arms. A slight positive over-pressure in the suit causes warm waste air (or water if the suit is punctured) to be safely vented into the sea through large PVs located at the bottom of each arm and leg. The secondary purge valves act to prevent the buildup of large concentrations of CO2 gas and help guard against asphyxia. It is noted that the MPV causes the inhalation and exhalation cycles to be completely isolated from one another in the current suit design.