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 first-order analog to Martian fretted terrain has been recognized on enhanced, ERTS-1 (Earth Resources Technology Satellite) imagery of Alaskan Arctic thermokarst terrain. The Alaskan analog displays flat-floored valleys and intervalley uplands characteristic of fretted terrain. The thermokarst terrain has formed in a manner similar to one of the processes postulated for the development of the Martian fretted terrain.
The present examination of the west Deuteronilus Mensae region of Mars notes the changes in fretted terrain across the gradational boundary from uplands to lowlands to include a reduction of canyon wall slopes and depths, so that the fretted terrain north of the gradational boundary appears matted, but not obscured. The two process-classes that may account for the lateral overlap are the erosion of stratified upland terrain, and the deposition of plains materials onto the sloping upland margin and fretted terrain. A variety of plains-emplacement mechanisms is considered.
The Termoskan instrument on board the Phobos '88 spacecraft acquired the highest spatial resolution thermal infrared emission data ever obtained for Mars. Included in the thermal images 2 km/pixel, midday observations of several major channel and valley systems including significant portions of Shalbatana, Ravi, Al-Qahira, and Ma'adim Valles, the channel connecting Valles Marineris with Hydraotes Chaos, and channel material in Eos Chasma. Termoskan also observed small portions of the southern beginnings of Simud, Tiu, and Ares Valles and some channel material in Gangis Chasma. Simultaneous broadband visible reflectance data were obtained for all but Ma'adim Vallis. We find that most of the channels and valleys have higher thermal inertias than their surroundings, consistent with previous thermal studies. We show for the first time that the thermal inertia boundaries closely match flat channel floor boundaries. Also, buttes within channels have inertias similiar to the plains surrounding the channels, suggesting the buttes are remnants of a contiguous plains surface. Lower bounds on typical channel thermal inertias range from 8.4 to 12.5 (10(exp -3) cal cm(exp -2) s(exp -1/2)/K) (352 to 523 in SI units of J m(exp -2) s(exp -1/2)/K). Lower bounds on inertia differences with the surrounding heavily cratered plains range from 1.1 to 3.5 (46 to 147 SI). Atmospheric and geometric effects are not sufficient to cause the observed channel inertia enhancements. We favor nonaeolian explanations of the overall channel inertia enhancements based primarily upon the channel floors' thermal homogeneity and the strong correlation of thermal boundaries with floor boundaries. However, localized, dark regions within some channels are likely aeolian in nature as reported previously. Most channels with increased inertias have fretted morphologies such as flat floors with steep walls. Eastern Ravi and southern Ares Valles, the only major channel sections observed that have obvious catastrophic flood bedforms, do not have enhanced inertias. Therefore, we favor fretting processes over catastrophic flooding for explaining the inertia enhancements. We postulate that the inertia enhancements were caused either by the original fretting process or by a process involving the bonding of fines due to an increased availability of water, either initially or secondarily.
A geologic map of the Ismenius Lacus (MC-5) Southwestern subquadrangle of Mars is described, using the 1:2,000,000 photomosaic as a base. The mapping, and a limited study of the surrounding areas, was done to determine the nature and origin of fretted terrain, fretted channels, and the northern highland scarp. Some highlights resulting from the mapping and accompanying topical investigations are included.
Various landforms possibly related to formation (growth), movement, or decay of ground ice have been identified on Mars, including fretted terrain (ft) and associated lobate debris aprons (lda), the chaotic terrain, concentric crater fills (ccf), polygonal ground, softened terrain, small domes that are possibly pingos, and curvilinear (fingerprint) features (cuf). Glaciers may also have been present. Some of these may involve ice derived from artesian groundwater. Topical areas of discussion are: Mars groundwater and the location of permafrost features; the ft, lda, ccf, and cuf; role of artesian groundwater in formation of fretted terrain, lobate debris blankets, and concentric crater fills; sources of glacial ice; and pingos and other pseudovolcanic structures.
The northwest Isidis Basin offers a unique opportunity to land near a fretted terrain lowland/upland boundary that meets both the latitudinal and elevation requirements imposed on the spacecraft. The landing site lies east of erosional scarps and among remnant massif inselbergs of the Syrtis Major volcanic plains. The plains surface throughout Isidis exhibits abundant, low-relief mounds that are the local expression of the 'thumbprint terrain' that is common within a few hundred kilometers of the lowland/upland boundary. The massif inselbergs are not as numerous nor as massive as those fretted terrains to the northwest, so local slopes are not expected to be steep. Neither feature should pose a serious threat to the lander. Landing on or adjacent to one of these features would enhance the science return and would help to pinpoint the landing site in Viking and subsequent orbiter images by offering views of landmarks beyond the local horizon.
Using Viking Orbiter images, detailed photoclinometric profiles were obtained across 10 irregular depressions, 32 fretted fractures, 40 troughs and pits, 124 solitary scarps, and 370 simple grabens in the north Tharsis region of Mars. These data allow inferences to be made on the shallow crustal structure of this region. The frequency modes of measured scarp heights correspond with previous general thickness estimates of the heavily cratered and rigded plains units. The depths of the flat-floored irregular depressions (55-175 m), fretted fractures (85-890 m), and troughs and pits (60-1620 m) are also similar to scarp heights (thicknesses) of the geologic units in which these depressions occur, which suggests that the depths of these flat-floored features were controlled by erosional base levels created by lithologic contacts. Although the features have a similar age, both their depths and their observed local structural control increase in the order listed above, which suggests that the more advanced stages of associated fracturing facilitated the development of these depressions by increasing permeability. If a ground-ice zone is a factor in development of these features, as has been suggested, our observation that the depths of these features decrease with increasing latitude suggests that either the thickness of the ground-ice zone does not increase poleward or the depths of the depressions were controlled by the top of the ground-ice zone whose depth may decrease with latitude.
We are investigating protein-protein interactions in under- and over-saturated crystallization solution conditions using fluorescence methods. The use of fluorescence requires fluorescent derivatives where the probe does not markedly affect the crystal packing. A number of chicken egg white lysozyme (CEWL) derivatives have been prepared, with the probes covalently attached to one of two different sites on the protein molecule; the side chain carboxyl of ASP 101, within the active site cleft, and the N-terminal amine. The ASP 101 derivatives crystallize while the N-terminal amine derivatives do not. However, the N-terminal amine is part of the contact region between adjacent 43 helix chains, and blocking this site does would not interfere with formation of these structures in solution. Preliminary FRET data have been obtained at pH 4.6, 0.1M NaAc buffer, at 5 and 7% NaCl, 4 C, using the N-terminal bound pyrene acetic acid (PAA, Ex 340 nm, Em 376 nm) and ASP 101 bound Lucifer Yellow (LY, Ex 425 nm, Em 525 nm) probe combination. The corresponding Csat values are 0.471 and 0.362 mg/ml (approximately 3.3 and approximately 2.5 x 10 (exp 5) M respectively), and all experiments were carried out at approximately Csat or lower total protein concentration. The data at both salt concentrations show a consistent trend of decreasing fluorescence yield of the donor species (PAA) with increasing total protein concentration. This decrease is apparently more pronounced at 7% NaCl, consistent with the expected increased intermolecular interactions at higher salt concentrations (reflected in the lower solubility). The estimated average distance between protein molecules at 5 x 10 (exp 6) M is approximately 70 nm, well beyond the range where any FRET can be expected. The calculated RO, where 50% of the donor energy is transferred to the acceptor, for the PAA-CEWL * LY-CEWL system is 3.28 nm, based upon a PAA-CEWL quantum efficiency of 0.41.
One of the most powerful and versatile methods for studying molecules in solution is fluorescence. Crystallization typically takes place in a concentrated solution environment, whereas fluorescence typically has an upper concentration limit of approximately 1 x 10(exp -5)M, thus intrinsic fluorescence cannot be employed, but a fluorescent probe must be added to a sub population of the molecules. However the fluorescent species cannot interfere with the self-assembly process. This can be achieved with macromolecules, where fluorescent probes can be covalently attached to a sub population of molecules that are subsequently used to track the system as a whole. We are using fluorescence resonance energy transfer (FRET) to study the initial solution phase self-assembly process of tetragonal lysozyme crystal nucleation, using covalent fluorescent derivatives which crystallize in the characteristic P432121 space group. FRET studies are being carried out between cascade blue (CB-lys, donor, Ex 376 nm, Em 420 nm) and lucifer yellow (LY-lys, acceptor, Ex 425 nm, Em 520 nm) asp101 derivatives. The estimated R0 for this probe pair, the distance where 50% of the donor energy is transferred to the acceptor, is approximately 1.2 nm, compared to 2.2 nm between the side chain carboxyls of adjacent asp101's in the crystalline 43 helix. The short CB-lys lifetime (approximately 5 ns), coupled with the large average distances between the molecules ((sup 3) 50 nm) in solution, ensure that any energy transfer observed is not due to random diffusive interactions. Addition of LY-lys to CB-lys results in the appearance of a second, shorter lifetime (approximately 0.2 ns). Results from these and other ongoing studies will be discussed in conjunction with a model for how tetragonal lysozyme crystals nucleate and grow, and the relevance of that model to microgravity protein crystal growth
Increasingly, millimeter waves are being employed for telecomm, radar, and imaging applications. To date in the U.S, however, very few investigations on the impact of this radiation on biological systems at the cellular level have been undertaken. In the beginning, to examine the impact of millimeter waves on cellular processes, researchers discovered that cell membrane depolarization may be triggered by low levels of integrated power at these high frequencies. Such a situation could be used to advantage in the direct stimulation of neuronal cells for applications in neuroprosthetics and diagnosing or treating neurological disorders. An experimental system was set up to directly monitor cell response on exposure to continuous-wave, fixed-frequency, millimeter-wave radiation at low and modest power levels (0.1 to 100 safe exposure standards) between 50 and 100 GHz. Two immortalized cell lines derived from lung and neuronal tissue were transfected with green fluorescent protein (GFP) that locates on the inside of the cell membrane lipid bi-layer. Oxonol dye was added to the cell medium. When membrane depolarization occurs, the oxonal bound to the outer wall of the lipid bi-layer can penetrate close to the inner wall where the GFP resides. Under fluorescent excitation (488 nm), the normally green GFP (520 nm) optical signal quenches and gives rise to a red output when the oxonol comes close enough to the GFP to excite a fluorescence resonance energy transfer (FRET) with an output at 620 nm. The presence of a strong FRET signature upon exposures of 30 seconds to 2 minutes at 5-10 milliwatts per square centimeter RF power at 50 GHz, followed by a return to the normal 520-nm GFP signal after a few minutes indicating repolarization of the membrane, indicates that low levels of RF energy may be able to trigger non-destructive membrane depolarization without direct cell contact. Such a mechanism could be used to stimulate neuronal cells in the cortex without the need for invasive electrodes as millimeter waves penetrate skin and bone on the order of 15 mm in depth. Although 50 GHz could not readily penetrate from the outer skull to the center of the cortex, implants on the outer skull or even on the scalp could reach the outer layer of the cerebral cortex where substantial benefit could be realized from such non-contact type excitation.
Formal verfication and simulation are powerful tools to validate requirements against complex systems. [Problem] Requirements are developed in early stages of the software lifecycle and are typically written in ambiguous natural language. There is a gap between such requirements and formal notations that can be used by verification tools, and lack of support for proper association of requirements with software artifacts for verification. [Principal idea] We propose to write requirements in an intuitive, structured natural language with formal semantics, and to support formalization and model/code verification as a smooth, well-integrated process. [Contribution] We have developed an end-to-end, open source requirements analysis framework that checks Simulink models against requirements written in structured natural language. Our framework is built in the Formal Requirements Elicitation Tool (fret); we use fret's requirements language named fretish, and formalization of fretish requirements in temporal logics. Our proposed framework contributes the following features: 1) automatic extraction of Simulink model information and association of fretish requirements with target model signals and components; 2) translation of temporal logic formulas into synchronous dataflow cocospec specifications as well as Simulink monitors, to be used by verification tools; we establish correctness of our translation through extensive automated testing; 3) interpretation of counterexamples produced by verification tools back at requirements level. These features support a tight integration and feedback loop between high level requirements and their analysis. We demonstrate our approach on a major case study: the Ten Lockheed Martin Cyber-Physical, aerospace-inspired challenge problems.
Capturing and analyzing requirements of Cyber-Physical Systems (CPS) can be challenging, since CPS models typically involve time-varying and real-valued variables, physical system dynamics, or even adaptive behavior. MATLAB/Simulinkis a development and simulation framework that is widely used in industry to capture such systems. In this paper, we report on the application of NASA Ames tools to perform end-to-end analysis of the Ten Lockheed Martin Challenge Problems (LMCPS). LMCPS is a set of industrial Simulink model benchmarks and natural language requirements developed by domain experts. Our framework, which integrates the tools FRET and COCOSIM, is used to: 1) elicit, explain, and formalize the semantics of the given natural language requirements; 2) generate verification code and monitors that can be automatically attached to the Simulink models; 3) perform verification by using SMT-based model checkers. FRET and COCOSIM are open source, and can be used by other researchers and practitioners to replicate our case study. We provide a categorization of recurring patterns in the formalization of the requirements and discuss the strengths and weaknesses of our automated verification approach.
The Independent Configurable Architecture for Reliable Operations of Unmanned Systems(ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.
The Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.
In this technical report, we provide requirements for a wildfire-fighting use-case, towards the Safety Demonstrator 1. The use case will incorporate ground and airborne assets operating in a coordinated fashion, and will comprise five activities, from detection to the execution of the initial attack. Depending on the activity and the data involved, the requirements identified may be non-probabilistic or probabilistic. In both cases, we first identify some of the requirements we wish to monitor, and then present a formalization using the language of requirements of the NASA requirements elicitation tool FRET. To formalize probabilistic requirements, we use a novel extension to FRET’s requirements language that incorporates notions of probability, and discuss how requirements can be translated into existing probabilistic temporal logics like PCTL. We exemplify how some of the requirements presented can be monitored using the existing tools Ogma and Copilot. We close with a summary and future directions.
Formal veri fication and simulation are powerful tools for the veri fication of requirements against complex systems. Requirements are developed in early stages of the software lifecycle and are typically expressed in natural language. There is a gap between such requirements and their software implementations. We present a framework that bridges this gap by supporting a tight integration and feedback loop between high-level requirements and their analysis against software artifacts. Our framework implements an analysis portal within the fret requirements elicitation tool, thus forming an end-to-end, open-source environment where requirements are written in an intuitive, structured natural language, and are veri fied automatically against Simulink models.
Developing critical software requires adherence to rigorous software development practices, such as formal requirement specification and verification. Despite their importance, such practices are often considered as complex and challenging tasks that require a strong formal methods background. In this paper, we present our work on simplifying the formal requirements specification experience for resource-constrained mission critical software through the use of structured natural language. To this end, we connect NASA’s FRET, a formal requirement elicitation and authoring tool with the Shelley model checking framework for MicroPython code. We report our experience on using these tools to specify requirements and analyze code from the NASA Ames PHALANX exploration concept.
The development of autonomous systems requires a rigorous process that can guarantee a system’s reliability in critical applications. At its core, an autonomous system bases its behavior on a well-defined decision making system. In this paper, we present a methodological basis for the design, formalization and formal verification of Decision Making systems for autonomous agents. The approach is generally applicable to operational objectives that can be functionally decomposed and subsequently represented as Hierarchical Finite State Machines. As a case study, we present the application of this method to implement a Decision Making model in Simulink. Furthermore, we present how we use NASA’s FRET tool to write requirements in structured natural language and generate formal specifications that can be automatically digested by NASA’s CoCoSim tool. Finally, we present how, by leveraging CoCoSim, we perform formal verification against the Simulink model and present analysis results.