Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “pathfinding”

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 1,009 records · Page 56
All sourcesNASA NTRSDOE OSTI
NASA NTRS2002

An "Andestic" Component in Shergottites with Restored LREE Abundances?

The shergottite Martian meteorites present a variety of oft-confusing petrologic features. In particular, represented among this subgroup are basalts with very depleted LREE abundances, as well as those with nearly chondritic overall REE abundances. The LREE-depleted basalts appear to more closely record the REE and isotopic features of their mantle source regions. Those basalts with more nearly chondritic REE abundances appear to contain an extra component often referred to as a "crustal" component. The addition of the crustal component tends to restore the overall REE abundance pattern towards chondritic relative abundances. Here we suggest that the crustal component could derive from "andesitic" rocks observed remotely to occur on the Martian surface, and which were analysed at the Pathfinder site.

Nyquist, L. E.↗
NASA NTRS2002

Geolocation Assessment Algorithm for CALIPSO Using Coastline Detection

Cloud-Aerosol Lidar Infrared Pathfinder Satellite Observations (CALIPSO) is a joint satellite mission between NASA and the French space agency CNES. The investigation will gather long-term, global cloud and aerosol optical and physical properties to improve climate models. The CALIPSO spacecraft is scheduled to launch in 2004 into a 98.2 inclination, 705 km circular orbit approximately 3 minutes behind the Aqua spacecraft. The payload consists of a two-wavelength polarization-sensitive lidar, and two passive imagers operating in the visible (0.645 mm) and infrared (8.7 - 12.0 mm) spectral regions. The imagers are nadir viewing and co-aligned with the lidar. Earth viewing measurements are geolocated to the Earth fixed coordinate system using satellite ephemeris, Earth rotation and geoid, and instrument pointing data. The coastline detection algorithm will assess the accuracy of the CALIPSO geolocation process by analyzing Wide Field Camera (WFC) visible ocean land boundaries. Processing space-time coincident MODIS and WFC scenes with the coastline algorithm will help verify the co-registration requirement with Moderate Resolution Imaging Spectrometer (MODIS) data. This paper quantifies the accuracy of the coastline geolocation assessment algorithm.

Currey, J. Chris↗
NASA NTRS2002

EXIST (Energetic X-ray Imaging Survey Telescope): The Next Large GRB Observatory

Studies have begun on the EXIST (Energetic X-ray Imaging Survey Telescope) Mission. It is planned as a very wide-field, sensitive coded aperture telescope with a sensitive area of the order of 6-8 m^2 and having a positional accuracy for GRBs (Gamma ray bursts) better than one arc-minute. EXIST will use SWIFT as a pathfinder mission; the findings of SWIFT will refine the scientific objectives of EXIST and will help to determine many of its design parameters. It would study early star formation and early galaxy formation at very high redshifts through observations of thousands of GRBs, their afterglows and environments. It is intended that the international GRB community will play as large role in EXIST through direct participation as well as with complementary observational programs, both space-based and ground-based. Some preliminary design features and capabilities of the EXIST Mission will be presented.

Fishman, G. J.↗
NASA NTRS2002

GRACE: Gravity Recovery and Climate Experiment

While gravity is much weaker than other basic forces in nature, such as magnetism and electricity, its effects are ubiquitous and dramatic. Gravity controls everything from the motion of the ocean tides to the expansion of the entire Universe. To learn more about the mysteries of gravity, twin satellites named GRACE--short for the Gravity Recovery and Climate Experiment--are being launched to make detailed measurements of Earth's gravity field. This experiment could lead to discoveries about gravity and Earth's natural systems, which could have substantial benefits for society and the world's population. The GRACE mission will be the inaugural flight of NASA's Earth System Science Pathfinder Program (ESSP). A component of NASA's Earth Science Enterprise (ESE), the ESSP missions are intended to address unique, specific highly focused scientific issues and provide measurements required to support Earth science research.

Ward, A.↗
NASA NTRS2002

The IRIS-GUS Shuttle Borne Upper Stage System

This paper describes the Italian Research Interim Stage - Gyroscopic Upper Stage (IRIS-GUS) upper stage system that will be used to launch NASA's Triana Observatory from the Space Shuttle. Triana is a pathfinder earth science mission being executed on rapid schedule and small budget, therefore the mission's upper stage solution had to be a system that could be fielded quickly at relatively low cost and risk. The building of the IRIS-GUS system wa necessary because NASA lost the capability to launch moderately sized upper stage missions fro the Space Shuttle when the PAM-D system was retired. The IRIS-GUS system restores this capability. The resulting system is a hybrid which mates the existing, flight proven IRIS (Italian Research Interim Stage) airborne support equipment to a new upper stage, the Gyroscopic Upper Stage (GUS) built by the GSFC for Triana. Although a new system, the GUS exploits flight proven hardware and design approaches in most subsystems, in some cases implementing proven design approaches with state-of-the-art electronics. This paper describes the IRIS-GUS upper stage system elements, performance capabilities, and payload interfaces.

Tooley, Craig↗
NASA NTRS2002

CALIPSO: Global Aerosol and Cloud Observations from Lidar and Passive Instruments

CALIPSO (Cloud-Aerosol Lidar and Infrared Pathfinder Spaceborne Observations) is an approved satellite mission being developed through collaboration between NASA and the French space agency CNES. The mission is scheduled for launch in 2004 and will operate for 3 years as part of a five-satellite formation called the Aqua constellation. This constellation will provide a unique data set on aerosol and cloud optical and physical properties and aerosol-cloud interactions that will substantially increase our understanding of the climate system and the potential for climate change.

Poole, L. R.↗
NASA NTRS2002

Program Instrumentation and Trace Analysis

Several attempts have been made recently to apply techniques such as model checking and theorem proving to the analysis of programs. This shall be seen as a current trend to analyze real software systems instead of just their designs. This includes our own effort to develop a model checker for Java, the Java PathFinder 1, one of the very first of its kind in 1998. However, model checking cannot handle very large programs without some kind of abstraction of the program. This paper describes a complementary scalable technique to handle such large programs. Our interest is turned on the observation part of the equation: How much information can be extracted about a program from observing a single execution trace? It is our intention to develop a technology that can be applied automatically and to large full-size applications, with minimal modification to the code. We present a tool, Java PathExplorer (JPaX), for exploring execution traces of Java programs. The tool prioritizes scalability for completeness, and is directed towards detecting errors in programs, not to prove correctness. One core element in JPaX is an instrumentation package that allows to instrument Java byte code files to log various events when executed. The instrumentation is driven by a user provided script that specifies what information to log. Examples of instructions that such a script can contain are: 'report name and arguments of all called methods defined in class C, together with a timestamp'; 'report all updates to all variables'; and 'report all acquisitions and releases of locks'. In more complex instructions one can specify that certain expressions should be evaluated and even that certain code should be executed under various conditions. The instrumentation package can hence be seen as implementing Aspect Oriented Programming for Java in the sense that one can add functionality to a Java program without explicitly changing the code of the original program, but one rather writes an aspect and compiles it into the original program using the instrumentation. Another core element of JPaX is an observation package that supports the analysis of the generated event stream. Two kinds of analysis are currently supported. In temporal analysis the execution trace is evaluated against formulae written in temporal logic. We have implemented a temporal logic evaluator on finite traces using the Maude rewriting system from SRI International, USA. Temporal logic is defined in Maude by giving its syntax as a signature and its semantics as rewrite equations. The resulting semantics is extremely efficient and can handle event streams of hundreds of millions events in few minutes. Furthermore, the implementation is very succinct. The second form of even stream analysis supported is error pattern analysis where an execution trace is analyzed using various error detection algorithms that can identify error-prone programming practices that may potentially lead to errors in some different executions. Two such algorithms focusing on concurrency errors have been implemented in JPaX, one for deadlocks and the other for data races. It is important to note, that a deadlock or data race potential does not need to occur in order for its potential to be detected with these algorithms. This is what makes them very scalable in practice. The data race algorithm implemented is the Eraser algorithm from Compaq, however adopted to Java. The tool is currently being applied to a code base for controlling a spacecraft by the developers of that software in order to evaluate its applicability.

Havelund, Klaus↗
NASA NTRS2003

Generalized Symbolic Execution for Model Checking and Testing

Modern software systems, which often are concurrent and manipulate complex data structures must be extremely reliable. We present a novel framework based on symbolic execution, for automated checking of such systems. We provide a two-fold generalization of traditional symbolic execution based approaches: one, we define a program instrumentation, which enables standard model checkers to perform symbolic execution; two, we give a novel symbolic execution algorithm that handles dynamically allocated structures (e.g., lists and trees), method preconditions (e.g., acyclicity of lists), data (e.g., integers and strings) and concurrency. The program instrumentation enables a model checker to automatically explore program heap configurations (using a systematic treatment of aliasing) and manipulate logical formulae on program data values (using a decision procedure). We illustrate two applications of our framework: checking correctness of multi-threaded programs that take inputs from unbounded domains with complex structure and generation of non-isomorphic test inputs that satisfy a testing criterion. Our implementation for Java uses the Java PathFinder model checker.

Khurshid, Sarfraz↗
NASA NTRS2002

Formal Verification for a Next-Generation Space Shuttle

This paper discusses the verification and validation (V&2) of advanced software used for integrated vehicle health monitoring (IVHM), in the context of NASA's next-generation space shuttle. We survey the current VBCV practice and standards used in selected NASA projects, review applicable formal verification techniques, and discuss their integration info existing development practice and standards. We also describe two verification tools, JMPL2SMV and Livingstone PathFinder, that can be used to thoroughly verify diagnosis applications that use model-based reasoning, such as the Livingstone system.

Nelson, Stacy D.↗
NASA NTRS2003

Test-Case Generation using an Explicit State Model Checker Final Report

In the project 'Test-Case Generation using an Explicit State Model Checker' we have extended an existing tools infrastructure for formal modeling to export Java code so that we can use the NASA Ames tool Java Pathfinder (JPF) for test case generation. We have completed a translator from our source language RSML(exp -e) to Java and conducted initial studies of how JPF can be used as a testing tool. In this final report, we provide a detailed description of the translation approach as implemented in our tools.

Heimdahl, Mats P. E.↗
NASA NTRS2002

Evaluation of Methods to Estimate the Surface Downwelling Longwave Flux during Arctic Winter

Surface longwave radiation fluxes dominate the energy budget of nighttime polar regions, yet little is known about the relative accuracy of existing satellite-based techniques to estimate this parameter. We compare eight methods to estimate the downwelling longwave radiation flux and to validate their performance with measurements from two field programs in thc Arctic: the Coordinated Eastern Arctic Experiment (CEAREX ) conducted in the Barents Sea during the autumn and winter of 1988, and the Lead Experiment performed in the Beaufort Sea in the spring of 1992. Five of the eight methods were developed for satellite-derived quantities, and three are simple parameterizations based on surface observations. All of the algorithms require information about cloud fraction, which is provided from the NASA-NOAA Television and Infrared Observation Satellite (TIROS) Operational Vertical Sounder (TOVS) polar pathfinder dataset (Path-P): some techniques ingest temperature and moisture profiles (also from Path-P): one-half of the methods assume that clouds are opaque and have a constant geometric thickness of 50 hPa, and three include no thickness information whatsoever. With a somewhat limited validation dataset, the following primary conclusions result: (1) all methods exhibit approximately the same correlations with measurements and rms differences, but the biases range from -34 W sq m (16% of the mean) to nearly 0; (2) the error analysis described here indicates that the assumption of a 50-hPa cloud thickness is too thin by a factor of 2 on average in polar nighttime conditions; (3) cloud-overlap techniques. which effectively increase mean cloud thickness, significantly improve the results; (4) simple Arctic-specific parameterizations performed poorly, probably because they were developed with surface-observed cloud fractions; and (5) the single algorithm that includes an estimate of cloud thickness exhibits the smallest differences from observations.

Chiacchio, Marc↗
NASA NTRS2002

Evaluation of GEOSAT Follow-On Precise Orbit Ephemeris

The GEOSAT Follow-On spacecraft (GFO-l), launched in 1998, began continuous radar altimeter coverage of the oceans in 2000, and after an extensive series of calibration campaigns in 1999 and 2000 was finally accepted by the US Navy on November 29, 2000. By providing high quality altimeter data, GFO can supplement TOPEX/POSEIDON(T/P), ERS-1, and ERS-2 data, providing a different synoptic sampling of the oceans with its 17-day ground track repeat cycle. Altimeter analysis suggests GFO is capable of POSEIDON class altimetry, with orbit error the largest contributor to the GFO altimeter error budget. Satellite laser ranging (SLR), especially in combination with altimeter crossover data, offer the only means of determining high-quality precise orbits. SLR tracking is also augmented by Doppler (Tranet style) beacons. These data were used to tune the gravity field and macromodel (3D representation of the spacecraft geometry and surface properties). Beginning with January 2000 GSFC has produced a 2.5 year span of the Precision Orbit Ephemeris (POE) intended for use on the GFO GDR and for the Pathfinder Project. Using GFO GDR and IGDR altimeter data from NOAA, a two year span of POE orbits are evaluated with respect to the TOPEX orbits by adjusting the GFO data into the TOPEX frame with the help of TOPEX/GFO altimeter crossovers. A 2.5 year span of orbits are also evaluated using tracking data residual analysis, GFO altimeter crossover residual analysis, and direct orbit comparison. In an effort to improve the current POE orbit several ideas are considered, including using recent gravity models which include CHAMP data, the reduced-dynamic approach, and including TOPEX/GFO altimeter crossover data in the orbit solution.

Lemoine, Frank G.↗
NASA NTRS1999

Vertical Structure in Outer Planet Atmospheres

The period covered by this cooperative agreement included: 1) the analysis of data acquired by both Voyager spacecraft during their encounters with Saturn in 1979 and 1980; 2) work on Uranus' seasonal variability and transient albedo features on both Uranus and Neptune using observations made by the Hubble Space Telescope beginning in 2000; 3) a search for lightning on Jupiter using HST; and 4) the analysis of Pathfinder images of Martian surface features.

Rages, Kathy A.↗
NASA NTRS2003

Far-IR/Submillimeter Interferometry Missions in NASA's Roadmap: SPIRIT and SPECS

Information vital to the attainment of the major scientific objectives of NASA's Origins and Structure and Evolution of the Universe themes is uniquely available in the far-IR and submillimeter (FIR/SMM). NASA is studying concepts and investing in technologies for FIR/SMM observatories that could fly in the period 2010 - 2025 and provide enormous increases in measurement capabilities to extend the legacy of the next-generation missions SIRTF and Herschel. Future FIR/SMM space observatories will have the sensitivity needed to reach back in time to the formation epoch of the first luminous objects, the angular resolution needed to image proto-planetary systems and distinguish the emissions of individual galaxies, and the spectral resolution needed to probe the physical conditions and measure the flows of interstellar gas in young galaxies, nascent stars, and the dust-enshrouded nuclei of galaxies that harbor massive black holes. NASA's roadmap includes the JWST-class Single Aperture Far-IR (SAFIR) telescope and 1 km maximum-baseline FIR/SMM interferometer. This talk will focus on the niche for FIR/SMM interferometry and describe two missions: SPECS, the Submillimeter Probe of the Evolution of Cosmic Structure, and the pathfinder mission SPIRIT, the Space Infrared interferometric Telescope. I will give the scientific motivation for these missions, describe mission concepts and telescope measurement capabilities, and compare these capabilities with those of the next-generation IR telescopes, and with the complementary JWST and ALMA.

Leisawitz, David T.↗
NASA NTRS2003

Propel: Tools and Methods for Practical Source Code Model Checking

The work reported here is an overview and snapshot of a project to develop practical model checking tools for in-the-loop verification of NASA s mission-critical, multithreaded programs in Java and C++. Our strategy is to develop and evaluate both a design concept that enables the application of model checking technology to C++ and Java, and a model checking toolset for C++ and Java. The design concept and the associated model checking toolset is called Propel. It builds upon the Java PathFinder (JPF) tool, an explicit state model checker for Java applications developed by the Automated Software Engineering group at NASA Ames Research Center. The design concept that we are developing is Design for Verification (D4V). This is an adaption of existing best design practices that has the desired side-effect of enhancing verifiability by improving modularity and decreasing accidental complexity. D4V, we believe, enhances the applicability of a variety of V&V approaches; we are developing the concept in the context of model checking. The model checking toolset, Propel, is based on extending JPF to handle C++. Our principal tasks in developing the toolset are to build a translator from C++ to Java, productize JPF, and evaluate the toolset in the context of D4V. Through all these tasks we are testing Propel capabilities on customer applications.

Mansouri-Samani, Massoud↗
NASA NTRS2003

EXIST: The Next Large GRB Observatory

Studies have begun on the EXIST (Energetic X-ray Imaging Survey Telescope) Mission as a Black Hole Survey 'Einstein Probe', a major element in the new NASA Beyond Einstein Program in the Office of Space Science. This program was approved by the US Congress, in February 2003 as part of the NASA FY2004 NASA budget. EXIST is planned as a very wide-field coded aperture telescope and a positional accuracy for GRBs better than one arc-minute. The baseline detectors are Cadmium-Zinc-Telluride (CZT), with a total sensitive area of approximately 8 m2. EXIST will use SWIFT as a pathfinder mission; the findings of SWIFT will refine the scientific objectives of EXIST and will help to determine many of its design parameters. EXIST will study early star and galaxy formation at high redshifts through observations of thousands of GRBs, their afterglows and host galaxies. It is intended that the international GRB community will play a large role in EXIST through direct participation as well as with complementary observational programs, both space-based and ground-based. Some preliminary design features and capabilities of the EXIST Mission will be presented.

Fishman, Gerald J.↗
NASA NTRS2001

Addressing Dynamic Issues of Program Model Checking

Model checking real programs has recently become an active research area. Programs however exhibit two characteristics that make model checking difficult: the complexity of their state and the dynamic nature of many programs. Here we address both these issues within the context of the Java PathFinder (JPF) model checker. Firstly, we will show how the state of a Java program can be encoded efficiently and how this encoding can be exploited to improve model checking. Next we show how to use symmetry reductions to alleviate some of the problems introduced by the dynamic nature of Java programs. Lastly, we show how distributed model checking of a dynamic program can be achieved, and furthermore, how dynamic partitions of the state space can improve model checking. We support all our findings with results from applying these techniques within the JPF model checker.

Lerda, Flavio↗
NASA NTRS2001

Efficient Translation of LTL Formulae into Buchi Automata

Model checking is a fully automated technique for checking that a system satisfies a set of required properties. With explicit-state model checkers, properties are typically defined in linear-time temporal logic (LTL), and are translated into B chi automata in order to be checked. This report presents how we have combined and improved existing techniques to obtain an efficient LTL to B chi automata translator. In particular, we optimize the core of existing tableau-based approaches to generate significantly smaller automata. Our approach has been implemented and is being released as part of the Java PathFinder software (JPF), an explicit state model checker under development at the NASA Ames Research Center.

Giannakopoulou, Dimitra↗