Engineering PapersSearch

Engineering topics

Clancy, Daniel

Publications and source records attributed to Clancy, Daniel.

At least 19 records

Combining Static Analysis and Model Checking for Software Analysis

We present an iterative technique in which model checking and static analysis are combined to verify large software systems. The role of the static analysis is to compute partial order information which the model checker uses to reduce the state space. During exploration, the model checker also computes aliasing information that it gives to the static analyzer which can then refine its analysis. The result of this refined analysis is then fed back to the model checker which updates its partial order reduction. At each step of this iterative process, the static analysis computes optimistic information which results in an unsafe reduction of the state space. However we show that the process converges to a fired point at which time the partial order information is safe and the whole state space is explored.

Brat, Guillaume

Hierarchies of Models: Toward Understanding Planetary Nebulae

Stars like our sun (initial masses between 0.8 to 8 solar masses) end their lives as swollen red giants surrounded by cool extended atmospheres. The nuclear reactions in their cores create carbon, nitrogen and oxygen, which are transported by convection to the outer envelope of the stellar atmosphere. As the star finally collapses to become a white dwarf, this envelope is expelled from the star to form a planetary nebula (PN) rich in organic molecules. The physics, dynamics, and chemistry of these nebulae are poorly understood and have implications not only for our understanding of the stellar life cycle but also for organic astrochemistry and the creation of prebiotic molecules in interstellar space. We are working toward generating three-dimensional models of planetary nebulae (PNe), which include the size, orientation, shape, expansion rate and mass distribution of the nebula. Such a reconstruction of a PN is a challenging problem for several reasons. First, the data consist of images obtained over time from the Hubble Space Telescope (HST) and spectra obtained from Kitt Peak National Observatory (KPNO) and Cerro Tololo Inter-American Observatory (CTIO). These images are of course taken from a single viewpoint in space, which amounts to a very challenging tomographic reconstruction. Second, the fact that we have two disparate and orthogonal data types requires that we utilize a method that allows these data to be used together to obtain a solution. To address these first two challenges we employ Bayesian model estimation using a parameterized physical model that incorporates much prior information about the known physics of the PN. In our previous works we have found that the forward problem of the comprehensive model is extremely time consuming. To address this challenge, we explore the use of a set of hierarchical models, which allow us to estimate increasingly more detailed sets of model parameters. These hierarchical models of increasing complexity are akin to scientific theories of increasing sophistication, with each new model/theory being a refinement of a previous one by either incorporating additional prior information or by introducing a new set of parameters to model an entirely new phenomenon. We apply these models to both a simulated and a real ellipsoidal PN to initially estimate the position, angular size, and orientation of the nebula as a two-dimensional object and use these estimates to later examine its three-dimensional properties. The efficiency/accuracy tradeoffs of the techniques are studied to determine the advantages and disadvantages of employing a set of hierarchical models over a single comprehensive model.

Knuth, Kevin H.

Two Paths from the Same Place: Task Driven and Human Centered Evolution of a Group Information Surface

This is the tale of two different implementations of a collaborative information tool, that started from the same design source. The Blueboard, developed at IBM Research, is a tool for groups to use in exchanging information in a lightweight, informal collaborative way. It began as a large display surface for walk-by use in a corporate setting and has evolved in response to task demands and user needs. At NASA, the MERBoard is being designed to support surface operations for the upcoming Mars Exploration Rover Missions. The MERBoard is a tool that was inspired by the Blueboard design, extending this design to support the collaboration requirements for viewing, annotating, linking and distributing information for the science and engineering teams that will operate two rovers on the surface of Mars. The ways in which each group transformed the system reflects not only technical requirements, but also the needs of users in each setting and embedding of the system within the larger socio-technical environment. Lessons about how task requirements, information flow requirements and work practice drive the evolution of a system are illustrated.

Russell, Daniel M.

Prediction of Aerodynamic Coefficients using Neural Networks for Sparse Data

Basic aerodynamic coefficients are modeled as functions of angles of attack and sideslip with vehicle lateral symmetry and compressibility effects. Most of the aerodynamic parameters can be well-fitted using polynomial functions. In this paper a fast, reliable way of predicting aerodynamic coefficients is produced using a neural network. The training data for the neural network is derived from wind tunnel test and numerical simulations. The coefficients of lift, drag, pitching moment are expressed as a function of alpha (angle of attack) and Mach number. The results produced from preliminary neural network analysis are very good.

Rajkumar, T.

Learning Assumptions for Compositional Verification

Compositional verification is a promising approach to addressing the state explosion problem associated with model checking. One compositional technique advocates proving properties of a system by checking properties of its components in an assume-guarantee style. However, the application of this technique is difficult because it involves non-trivial human input. This paper presents a novel framework for performing assume-guarantee reasoning in an incremental and fully automated fashion. To check a component against a property, our approach generates assumptions that the environment needs to satisfy for the property to hold. These assumptions are then discharged on the rest of the system. Assumptions are computed by a learning algorithm. They are initially approximate, but become gradually more precise by means of counterexamples obtained by model checking the component and its environment, alternately. This iterative process may at any stage conclude that the property is either true or false in the system. We have implemented our approach in the LTSA tool and applied it to the analysis of a NASA system.

Cobleigh, Jamieson M.

Science Target Assessment for Mars Rover Instrument Deployment

This paper introduces the system being developed at NASA Ames Research Center, intended for the Mars '09 Smart Lander, to robustly place sensors or tools against rocks in a single communications cycle. Science targets must be assessed prior to instrument placement in order to segment them from the background and determine where, if possible, to position the instrument. An initial result of this research effort is a novel Bayesian based method for segmenting rocks from the ground using 3D data.

Pedersen, Liam

Instrument Deployment for Mars Rovers

Future Mars rovers, such as the planned 2009 MSL rover, require sufficient autonomy to robustly approach rock targets and place an instrument in contact with them. It took the 1997 Sojourner Mars rover between 3 and 5 communications cycles to accomplish this. This paper describes the technologies being developed and integrated onto the NASA Ames K9 prototype Mars rover to both accomplish this in one cycle, and to extend the complexity and duration of operations that a Mars rover can accomplish without intervention from mission control.

Pedersen, Liam

Dynamics of Quantum Adiabatic Evolution Algorithm for Number Partitioning

We have developed a general technique to study the dynamics of the quantum adiabatic evolution algorithm applied to random combinatorial optimization problems in the asymptotic limit of large problem size n. We use as an example the NP-complete Number Partitioning problem and map the algorithm dynamics to that of an auxiliary quantum spin glass system with the slowly varying Hamiltonian. We use a Green function method to obtain the adiabatic eigenstates and the minimum exitation gap, gmin = O(n2(sup -n/2)), corresponding to the exponential complexity of the algorithm for Number Partitioning. The key element of the analysis is the conditional energy distribution computed for the set of all spin configurations generated from a given (ancestor) configuration by simultaneous flipping of a fixed number of spins. For the problem in question this distribution is shown to depend on the ancestor spin configuration only via a certain parameter related to the energy of the configuration. As the result, the algorithm dynamics can be described in terms of one-dimensional quantum diffusion in the energy space. This effect provides a general limitation of a quantum adiabatic computation in random optimization problems. Analytical results are in agreement with the numerical simulation of the algorithm.

Smelyanskiy, Vadius

CIP Training Manual: Collaborative Information Portal Advance Training Information for Field Test Participants

The Collaborative Information Portal (CIP) is a web-based information management and retrieval system. Its purpose is to provide users at MER (Mars Exploration Rover) mission operations with easy access to a broad range of mission data and products and contextual information such as the current operations schedule. The CIP web-server provides this content in a user customizable web-portal environment. Since CIP is still under development, only a subset of the full feature set will be available for the EDO field test. The CIP web-portal will be accessed through a standard web browser. CIP is intended to be intuitive and simple to use, however, at the training session, users will receive a one to two page reference guide, which should aid them in using CIP. Users must provide their own computers for accessing CIP during the field test. These computers should be configured with Java 1.3 and a Java 2 enabled browser. Macintosh computers should be running OS 10.1.3 or later. Classic Mac OS (OS 9) is not supported. For more information please read section 7.3 in the FIASCO Rover Science Operations Test Mission Plan. Several screen shots of the Beta Release of CIP are shown on the following pages.

Schreiner, John

MERBoard User's Guide

An important goal of MERBoard is to allow users to quickly and easily share information. The front-end interface is physically a large plasma computer display with a touch screen, allowing multiple people to interact shoulder-to-shoulder or in a small meeting area. The software system allows people to interactively create digital whiteboards, browse the web, give presentations and connect to personal computers (for example, to run applications not on the MERBoard computer itself). There are four major integrated applications: a browser; a remote connection to another computer (VNC); a digital whiteboard; and a digital space (MERSpace), which is a digital repository for each individual user.

Trimble, Jay

Verification and Validation of Neural Networks for Aerospace Systems

The Dryden Flight Research Center V&V working group and NASA Ames Research Center Automated Software Engineering (ASE) group collaborated to prepare this report. The purpose is to describe V&V processes and methods for certification of neural networks for aerospace applications, particularly adaptive flight control systems like Intelligent Flight Control Systems (IFCS) that use neural networks. This report is divided into the following two sections: 1) Overview of Adaptive Systems; and 2) V&V Processes/Methods.

Mackall, Dale

On Abstractions and Simplifications in the Design of Human-Automation Interfaces

This report addresses the design of human-automation interaction from a formal perspective that focuses on the information content of the interface, rather than the design of the graphical user interface. It also addresses the issue of the information provided to the user (e.g., user-manuals, training material, and all other resources). In this report, we propose a formal procedure for generating interfaces and user-manuals. The procedure is guided by two criteria: First, the interface must be correct, that is, with the given interface the user will be able to perform the specified tasks correctly. Second, the interface should be succinct. The report discusses the underlying concepts and the formal methods for this approach. Two examples are used to illustrate the procedure. The algorithm for constructing interfaces can be automated, and a preliminary software system for its implementation has been developed.

Heymann, Michael

A Survey of Knowledge Management Research & Development at NASA Ames Research Center

This chapter catalogs knowledge management research and development activities at NASA Ames Research Center as of April 2002. A general categorization scheme for knowledge management systems is first introduced. This categorization scheme divides knowledge management capabilities into five broad categories: knowledge capture, knowledge preservation, knowledge augmentation, knowledge dissemination, and knowledge infrastructure. Each of nearly 30 knowledge management systems developed at Ames is then classified according to this system. Finally, a capsule description of each system is presented along with information on deployment status, funding sources, contact information, and both published and internet-based references.

Keller, Richard M.

Challenging Aerospace Problems for Intelligent Systems

In this paper we highlight four problem domains that are well suited and challenging for intelligent system technologies. The problems are defined and an outline of a probable approach is presented. No attempt is made to define the problems as test cases. In other words, no data or set of equations that a user can code and get results are provided. The main idea behind this paper is to motivate intelligent system researchers to examine problems that will elevate intelligent system technologies and applications to a higher level.

Krishnakumar, Kalmanje

The Challenge of Planning and Execution for Spacecraft Mobile Robots

The need for spacecraft mobile robots continues to grow. These robots offer the potential to increase the capability, productivity, and duration of space missions while decreasing mission risk and cost. Spacecraft Mobile Robots (SMRs) can serve a number of functions inside and outside of spacecraft from simpler tasks, such as performing visual diagnostics and crew support, to more complex tasks, such as performing maintenance and in-situ construction. One of the predominant challenges to deploying SMRs is to reduce the need for direct operator interaction. Teleoperation is often not practical due to the communication latencies incurred because of the distances involved and in many cases a crewmember would directly perform a task rather than teleoperate a robot to do it. By integrating a mixed-initiative constraint-based planner with an executive that supports adjustably autonomous control, we intend to demonstrate the feasibility of autonomous SMRs by deploying one inside the International Space Station (ISS) and demonstrate in simulation one that operates outside of the ISS. This paper discusses the progress made at NASA towards this end, the challenges ahead, and concludes with an invitation to the research community to participate.

Dorais, Gregory A.

Deriving Function-failure Similarity Information for Failure-free Rotorcraft Component Design

Performance and safety are the top concerns of high-risk aerospace applications at NASA. Eliminating or reducing performance and safety problems can be achieved with a thorough understanding of potential failure modes in the design that lead to these problems. The majority of techniques use prior knowledge and experience as well as Failure Modes and Effects as methods to determine potential failure modes of aircraft. The aircraft design needs to be passed through a general technique to ensure that every potential failure mode is considered, while avoiding spending time on improbable failure modes. In this work, this is accomplished by mapping failure modes to certain components, which are described by their functionality. In turn, the failure modes are then linked to the basic functions that are carried within the components of the aircraft. Using the technique proposed in this paper, designers can examine the basic functions, and select appropriate analyses to eliminate or design out the potential failure modes. This method was previously applied to a simple rotating machine test rig with basic functions that are common to a rotorcraft. In this paper, this technique is applied to the engine and power train of a rotorcraft, using failures and functions obtained from accident reports and engineering drawings.

Roberts, Rory A.

A Framework for Creating a Function-based Design Tool for Failure Mode Identification

Knowledge of potential failure modes during design is critical for prevention of failures. Currently industries use procedures such as Failure Modes and Effects Analysis (FMEA), Fault Tree analysis, or Failure Modes, Effects and Criticality analysis (FMECA), as well as knowledge and experience, to determine potential failure modes. When new products are being developed there is often a lack of sufficient knowledge of potential failure mode and/or a lack of sufficient experience to identify all failure modes. This gives rise to a situation in which engineers are unable to extract maximum benefits from the above procedures. This work describes a function-based failure identification methodology, which would act as a storehouse of information and experience, providing useful information about the potential failure modes for the design under consideration, as well as enhancing the usefulness of procedures like FMEA. As an example, the method is applied to fifteen products and the benefits are illustrated.

Arunajadai, Srikesh G.

Planning Under Continuous Time and Resource Uncertainty: A Challenge for AI

There has been considerable work in Al on decision-theoretic planning and planning under uncertainty. Unfortunately, all of this work suffers from one or more of the following limitations: 1) it relies on very simple models of actions and time, 2) it assumes that uncertainty is manifested in discrete action outcomes, and 3) it is only practical for very small problems. For many real world problems, these assumptions fail to hold. A case in point is planning the activities for a Mars rover. For this domain none of the above assumptions are valid: 1) actions can be concurrent and have differing durations, 2) there is uncertainty concerning action durations and consumption of continuous resources like power, and 3) typical daily plans involve on the order of a hundred actions. We describe the rover problem, discuss previous work on planning under uncertainty, and present a detailed. but very small, example illustrating some of the difficulties of finding good plans.

Bresina, John