Search NASA⌕ Search

Engineering topics

Koga, Dennis

Publications and source records attributed to Koga, Dennis.

At least 19 records
All sourcesNASA NTRSDOE OSTI
NASA NTRS2003

Design for Verification: Enabling Verification of High Dependability Software-Intensive Systems

Strategies to achieve confidence that high-dependability applications are correctly implemented include testing and automated verification. Testing deals mainly with a limited number of expected execution paths. Verification usually attempts to deal with a larger number of possible execution paths. While the impact of architecture design on testing is well known, its impact on most verification methods is not as well understood. The Design for Verification approach considers verification from the application development perspective, in which system architecture is designed explicitly according to the application's key properties. The D4V-hypothesis is that the same general architecture and design principles that lead to good modularity, extensibility and complexity/functionality ratio can be adapted to overcome some of the constraints on verification tools, such as the production of hand-crafted models and the limits on dynamic and static analysis caused by state space explosion.

Mehlitz, Peter C.↗
NASA NTRS2003

Constraint Reasoning Over Strings

This paper discusses an approach to representing and reasoning about constraints over strings. We discuss how many string domains can often be concisely represented using regular languages, and how constraints over strings, and domain operations on sets of strings, can be carried out using this representation.

Koga, Dennis↗
NASA NTRS2003

On the Critical Behaviour, Crossover Point and Complexity of the Exact Cover Problem

Research into quantum algorithms for NP-complete problems has rekindled interest in the detailed study a broad class of combinatorial problems. A recent paper applied the quantum adiabatic evolution algorithm to the Exact Cover problem for 3-sets (EC3), and provided an empirical evidence that the algorithm was polynomial. In this paper we provide a detailed study of the characteristics of the exact cover problem. We present the annealing approximation applied to EC3, which gives an over-estimate of the phase transition point. We also identify empirically the phase transition point. We also study the complexity of two classical algorithms on this problem: Davis-Putnam and Simulated Annealing. For these algorithms, EC3 is significantly easier than 3-SAT.

Morris, Robin D.↗
NASA NTRS2003

Design for Verification: Using Design Patterns to Build Reliable Systems

Components so far have been mainly used in commercial software development to reduce time to market. While some effort has been spent on formal aspects of components, most of this was done in the context of programming language or operating system framework integration. As a consequence, increased reliability of composed systems is mainly regarded as a side effect of a more rigid testing of pre-fabricated components. In contrast to this, Design for Verification (D4V) puts the focus on component specific property guarantees, which are used to design systems with high reliability requirements. D4V components are domain specific design pattern instances with well-defined property guarantees and usage rules, which are suitable for automatic verification. The guaranteed properties are explicitly used to select components according to key system requirements. The D4V hypothesis is that the same general architecture and design principles leading to good modularity, extensibility and complexity/functionality ratio can be adapted to overcome some of the limitations of conventional reliability assurance measures, such as too large a state space or too many execution paths.

Mehlitz, Peter C.↗
NASA NTRS2003

Hosted Services for Advanced V and V Technologies: An Approach to Achieving Adoption without the Woes of Usage

Attempts to achieve widespread use of software verification tools have been notably unsuccessful. Even 'straightforward', classic, and potentially effective verification tools such as lint-like tools face limits on their acceptance. These limits are imposed by the expertise required applying the tools and interpreting the results, the high false positive rate of many verification tools, and the need to integrate the tools into development environments. The barriers are even greater for more complex advanced technologies such as model checking. Web-hosted services for advanced verification technologies may mitigate these problems by centralizing tool expertise. The possible benefits of this approach include eliminating the need for software developer expertise in tool application and results filtering, and improving integration with other development tools.

Koga, Dennis↗
NASA NTRS2003

Experiments with Test Case Generation and Runtime Analysis

Software testing is typically an ad hoc process where human testers manually write many test inputs and expected test results, perhaps automating their execution in a regression suite. This process is cumbersome and costly. This paper reports preliminary results on an approach to further automate this process. The approach consists of combining automated test case generation based on systematically exploring the program's input domain, with runtime analysis, where execution traces are monitored and verified against temporal logic specifications, or analyzed using advanced algorithms for detecting concurrency errors such as data races and deadlocks. The approach suggests to generate specifications dynamically per input instance rather than statically once-and-for-all. The paper describes experiments with variants of this approach in the context of two examples, a planetary rover controller and a space craft fault protection system.

Artho, Cyrille↗
NASA NTRS2003

High-Level Data Races

Data races are a common problem in concurrent and multi-threaded programming. They are hard to detect without proper tool support. Despite the successful application of these tools, experience shows that the notion of data race is not powerful enough to capture certain types of inconsistencies occurring in practice. In this paper we investigate data races on a higher abstraction layer. This enables us to detect inconsistent uses of shared variables, even if no classical race condition occurs. For example, a data structure representing a coordinate pair may have to be treated atomically. By lifting the meaning of a data race to a higher level, such problems can now be covered. The paper defines the concepts view and view consistency to give a notation for this novel kind of property. It describes what kinds of errors can be detected with this new definition, and where its limitations are. It also gives a formal guideline for using data structures in a multi-threading environment.

Artho, Cyrille↗
NASA NTRS2003

Scheduling in the Face of Uncertain Resource Consumption and Utility

We discuss the problem of scheduling tasks that consume a resource with known capacity and where the tasks have varying utility. We consider problems in which the resource consumption and utility of each activity is described by probability distributions. In these circumstances, we would like to find schedules that exceed a lower bound on the expected utility when executed. We first show that while some of these problems are NP-complete, others are only NP-Hard. We then describe various heuristic search algorithms to solve these problems and their drawbacks. Finally, we present empirical results that characterize the behavior of these heuristics over a variety of problem classes.

Koga, Dennis↗
NASA NTRS2003

Questions Revisited: A Close Examination of Calculus of Inference and Inquiry

In this paper I examine more closely the way in which probability theory, the calculus of inference, is derived from the Boolean lattice structure of logical assertions ordered by implication. I demonstrate how the duality between the logical conjunction and disjunction in Boolean algebra is lost when deriving the probability calculus. In addition, I look more closely at the other lattice identities to verify that they are satisfied by the probability calculus. Last, I look towards developing the calculus of inquiry demonstrating that there is a sum and product rule for the relevance measure as well as a Bayes theorem. Current difficulties in deriving the complete inquiry calculus will also be discussed.

Knuth, Kevin H.↗
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 NTRS2002

Artificial Immune System Approaches for Aerospace Applications

Artificial Immune Systems (AIS) combine a priori knowledge with the adapting capabilities of biological immune system to provide a powerful alternative to currently available techniques for pattern recognition, modeling, design, and control. Immunology is the science of built-in defense mechanisms that are present in all living beings to protect against external attacks. A biological immune system can be thought of as a robust, adaptive system that is capable of dealing with an enormous variety of disturbances and uncertainties. Biological immune systems use a finite number of discrete "building blocks" to achieve this adaptiveness. These building blocks can be thought of as pieces of a puzzle which must be put together in a specific way-to neutralize, remove, or destroy each unique disturbance the system encounters. In this paper, we outline AIS models that are immediately applicable to aerospace problems and identify application areas that need further investigation.

KrishnaKumar, Kalmanje↗
NASA NTRS2002

A Closed Mars Analog Simulation: The Approach of Crew 5 At the Mars Desert Research Station

For twelve days in April 2002 we performed a closed simulation in the Mars Desert Research Station, isolated from other people, as on Mars, while performing systematic surface exploration and life support chores. Email provided our only means of contact; no phone or radio conversations were possible. All mission-related messages were mediated by a remote mission support team. This protocol enabled a systematic and controlled study of crew activities, scheduling, and use of space. The analysis presented here focuses on two questions: Where did the time go-why did people feel rushed and unable to complete their work? How can we measure and model productivity, to compare habitat designs, schedules, roles, and tools? Analysis suggests that a simple scheduling change-having lunch and dinner earlier, plus eliminating afternoon meetings-increased the available productive time by 41%.

Clancey, William J.↗
NASA NTRS2002

The Mars Exploration Rover/Collaborative Information Portal

Astrology has long argued that the alignment of the planets governs human affairs. Science usually scoffs at this. There is, however, an important exception: sending spacecraft for planetary exploration. In late May and early June, 2003, Mars will be in position for Earth launch. Two Mars Exploration Rovers (MER) will rocket towards the red planet. The rovers will perform a series of geological and meteorological experiments, seeking to examine geological evidence for water and conditions once favorable for life. Back on earth, a small army of surface operations staff will work to keep the rovers running, sending directions for each day's operations and receiving the files encoding the outputs of the Rover's six instruments. (Mars is twenty light minutes from Earth. The rovers must be robots.) The fundamental purpose of the project is, after all, Science. Scientists have experiments they want to run. Ideally, scientists want to be immediately notified when the data products of their experiments have been received, so that they can examine their data and (collaboratively) deduce results. Mars is an unpredictable environment. We may issue commands to the rovers but there is considerable uncertainty in how the commands will be executed and whether what the rovers sense will be worthy of further pursuit. The steps of what is, to a scientist, conceptually an individual experiment may be scattered over a large number of activities. While the scientific staff has an overall strategic idea of what it would like to accomplish, activities are planned daily. The data and surprises of the previous day need to be integrated into the negotiations for the next day's activities, all synchronized to a schedule of transmission windows . Negotiations is the operative term, as different scientists want the resources to run possibly incompatible experiments. Many meetings plan each day's activities.

Walton, Joan↗
NASA NTRS2002

NETMARK

This presentation discuss NASA's proposed NETMARK knowledge management tool which aims 'to control and interoperate with every block in a document, email, spreadsheet, power point, database, etc. across the lifecycle'. Topics covered include: system software requirements and hardware requirements, seamless information systems, computer architecture issues, and potential benefits to NETMARK users.

Maluf, David A.↗
NASA NTRS2002

NASA Smart Surgical Probe Project

Information Technologies being developed by NASA to assist astronaut-physician in responding to medical emergencies during long space flights are being employed for the improvement of women's health in the form of "smart surgical probe". This technology, initially developed for neurosurgery applications, not only has enormous potential for the diagnosis and treatment of breast cancer, but broad applicability to a wide range of medical challenges. For the breast cancer application, the smart surgical probe is being designed to "see" a suspicious lump, determine by its features if it is cancerous, and ultimately predict how the disease may progress. A revolutionary early breast cancer detection tool based on this technology has been developed by a commercial company and is being tested in human clinical trials at the University of California at Davis, School of Medicine. The smart surgical probe technology makes use of adaptive intelligent software (hybrid neural networks/fuzzy logic algorithms) with the most advanced physiologic sensors to provide real-time in vivo tissue characterization for the detection, diagnosis and treatment of tumors, including determination of tumor microenvironment and evaluation of tumor margins. The software solutions and tools from these medical applications will lead to the development of better real-time minimally-invasive smart surgical probes for emergency medical care and treatment of astronauts on long space flights.

Mah, Robert W.↗
NASA NTRS2002

SOFIA's Choice: Scheduling Observations for an Airborne Observatory

We describe the problem of scheduling observations for an airborne observatory. The problem is more complex than traditional scheduling problems in that it incorporates complex constraints relating the feasibility of an astronomical observation to the position and time of a mobile observatory, as well as traditional temporal constraints and optimization criteria. We describe the problem, its proposed solution and the empirical validation of that solution.

Frank, Jeremy↗
NASA NTRS2002

Classification of Aircraft Maneuvers for Fault Detection

Automated fault detection is an increasingly important problem in aircraft maintenance and operation. Standard methods of fault detection assume the availability of either data produced during all possible faulty operation modes or a clearly-defined means to determine whether the data provide a reasonable match to known examples of proper operation. In the domain of fault detection in aircraft, the first assumption is unreasonable and the second is difficult to determine. We envision a system for online fault detection in aircraft, one part of which is a classifier that predicts the maneuver being performed by the aircraft as a function of vibration data and other available data. To develop such a system, we use flight data collected under a controlled test environment, subject to many sources of variability. We explain where our classifier fits into the envisioned fault detection system as well as experiments showing the promise of this classification subsystem.

Oza, Nikunj↗