Search NASA⌕ Search

Engineering topics

Lowry, Michael

Publications and source records attributed to Lowry, Michael.

16 records
All sourcesNASA NTRSDOE OSTI
NASA NTRS2018

Design Considerations for a Variable Autonomy Executive for UAS in the NAS

This paper describes research targeted towards an autonomy executive (AOS) for UAS in the National Air Space (NAS). The project goal is to incrementally provide the knowledge and intelligence onboard a UAS to safely fly in the National Air Space, eventually autonomous from remote human ground crews and communicating directly with air traffic control. Longer-term, the goal is to provide the capability for pilotless air vehicles such as air taxis that will be key for new transportation concepts such as air mobility-on-demand. For both of these targeted applications, AOS is incorporating artificial intelligence capabilities that operationally meet human pilot competencies. Even when autonomy is achieved from a remote human ground crew, AOS will have variable degrees of autonomy with respect to air traffic control (ATC), just as human pilots do now. AOS has the capability of interacting in natural language with ATC, as well as through data link protocols. AOS can adapt to varying levels of autonomy and control directed by ATC in standard and relaxed FAA phraseology- from being vectored moment by moment, to accepting broad directives such as following a specified aircraft or sighting and avoiding traffic. AOS can autonomously manage contingencies such as vehicle systems degradations and failures. It incorporates a decision maker that takes information from multiple diagnostic reasoners, disambiguates (if needed) sensor results to specific failures using active mode changes, then projects forward the impact of the degradation on the nominal plan. If the nominal plan is no longer viable, then alternative plans are formulated, and subsequently selected and executed, including abort options.

Lowry, Michael↗
NASA NTRS2017

Autonomy Operating System for UAVs: Pilot-in-a-Box

The Autonomy Operating System (AOS) is an open flight software platform with Artificial Intelligence for smart UAVs. It is built to be extendable with new apps, similar to smartphones, to enable an expanding set of missions and capabilities. AOS has as its foundations NASAs core flight executive and core flight software (cFEcFS). Pilot-in-a-Box (PIB) is an expanding collection of interacting AOS apps that provide the knowledge and intelligence onboard a UAV to safely and autonomously fly in the National Air Space, eventually without a remote human ground crew. Longer-term, the goal of PIB is to provide the capability for pilotless air vehicles such as air taxis that will be key for new transportation concepts such as mobility-on-demand. PIB provides the procedural knowledge, situational awareness, and anticipatory planning (thinking ahead of the plane) that comprises pilot competencies. These competencies together with a natural language interface will enable Pilot-in-a-Box to dialogue directly with Air Traffic Management from takeoff through landing. This paper describes the overall AOS architecture, Artificial Intelligence reasoning engines, Pilot-in-a-box competencies, and selected experimental flight tests to date.

Lowry, Michael↗
NASA NTRS2013

Human and Robotic Space Mission Use Cases for High-Performance Spaceflight Computing

Spaceflight computing is a key resource in NASA space missions and a core determining factor of spacecraft capability, with ripple effects throughout the spacecraft, end-to-end system, and the mission; it can be aptly viewed as a "technology multiplier" in that advances in onboard computing provide dramatic improvements in flight functions and capabilities across the NASA mission classes, and will enable new flight capabilities and mission scenarios, increasing science and exploration return per mission-dollar.

flight computing↗
NASA NTRS2013

Human and Robotic Space Mission Use Cases for High-Performance Spaceflight Computing

Spaceflight computing is a key resource in NASA space missions and a core determining factor of spacecraft capability, with ripple effects throughout the spacecraft, end-to-end system, and mission. Onboard computing can be aptly viewed as a "technology multiplier" in that advances provide direct dramatic improvements in flight functions and capabilities across the NASA mission classes, and enable new flight capabilities and mission scenarios, increasing science and exploration return. Space-qualified computing technology, however, has not advanced significantly in well over ten years and the current state of the practice fails to meet the near- to mid-term needs of NASA missions. Recognizing this gap, the NASA Game Changing Development Program (GCDP), under the auspices of the NASA Space Technology Mission Directorate, commissioned a study on space-based computing needs, looking out 15-20 years. The study resulted in a recommendation to pursue high-performance spaceflight computing (HPSC) for next-generation missions, and a decision to partner with the Air Force Research Lab (AFRL) in this development.

use cases↗
NASA NTRS2003

Transitioning from Software Requirements Models to Design Models

Summary: 1. Proof-of-concept of state machine synthesis from scenarios - CTAS case study. 2. CTAS team wants to use the syntheses algorithm to validate trajectory generation. 3. Extending synthesis algorithm towards requirements validation: (a) scenario relationships' (b) methodology for generalizing/refining scenarios, and (c) interaction patterns to control synthesis. 4. Initial ideas tested on conflict detection scenarios.

Lowry, Michael↗
NASA NTRS2001

Certifying Domain-Specific Policies

Proof-checking code for compliance to safety policies potentially enables a product-oriented approach to certain aspects of software certification. To date, previous research has focused on generic, low-level programming-language properties such as memory type safety. In this paper we consider proof-checking higher-level domain -specific properties for compliance to safety policies. The paper first describes a framework related to abstract interpretation in which compliance to a class of certification policies can be efficiently calculated Membership equational logic is shown to provide a rich logic for carrying out such calculations, including partiality, for certification. The architecture for a domain-specific certifier is described, followed by an implemented case study. The case study considers consistency of abstract variable attributes in code that performs geometric calculations in Aerospace systems.

Lowry, Michael↗
NASA NTRS1999

Transformation Systems at NASA Ames

In this paper, we describe the experiences of the Automated Software Engineering Group at the NASA Ames Research Center in the development and application of three different transformation systems. The systems span the entire technology range, from deductive synthesis, to logic-based transformation, to almost compiler-like source-to-source transformation. These systems also span a range of NASA applications, including solving solar system geometry problems, generating data analysis software, and analyzing multi-threaded Java code.

Buntine, Wray↗
NASA NTRS1998

Towards a Theory for Integration of Mathematical Verification and Empirical Testing

From the viewpoint of a project manager responsible for the V&V (verification and validation) of a software system, mathematical verification techniques provide a possibly useful orthogonal dimension to otherwise standard empirical testing. However, the value they add to an empirical testing regime both in terms of coverage and in fault detection has been difficult to quantify. Furthermore, potential cost savings from replacing testing with mathematical verification techniques cannot be realized until the tradeoffs and synergies can be formulated. Integration of formal verification with empirical testing is also difficult because the idealized view of mathematical verification providing a correctness proof with total coverage is unrealistic and does not reflect the limitations imposed by computational complexity of mathematical techniques. This paper first describes a framework based on software reliability and formalized fault models for a theory of software design fault detection - and hence the utility of various tools for debugging. It then describes a utility model for integrating mathematical and empirical techniques with respect to fault detection and coverage analysis. It then considers the optimal combination of black-box testing, white-box (structural) testing, and formal methods in V&V of a software system. Using case studies from NASA software systems, it then demonstrates how this utility model can be used in practice.

Lowry, Michael↗
NASA NTRS1998

Explaining Synthesized Software

Motivated by NASA's need for high-assurance software, NASA Ames' Amphion project has developed a generic program generation system based on deductive synthesis. Amphion has a number of advantages, such as the ability to develop a new synthesis system simply by writing a declarative domain theory. However, as a practical matter, the validation of the domain theory for such a system is problematic because the link between generated programs and the domain theory is complex. As a result, when generated programs do not behave as expected, it is difficult to isolate the cause, whether it be an incorrect problem specification or an error in the domain theory. This paper describes a tool we are developing that provides formal traceability between specifications and generated code for deductive synthesis systems. It is based on extensive instrumentation of the refutation-based theorem prover used to synthesize programs. It takes augmented proof structures and abstracts them to provide explanations of the relation between a specification, a domain theory, and synthesized code. In generating these explanations, the tool exploits the structure of Amphion domain theories, so the end user is not confronted with the intricacies of raw proof traces. This tool is crucial for the validation of domain theories as well as being important in everyday use of the code synthesis system. It plays an important role in validation because when generated programs exhibit incorrect behavior, it provides the links that can be traced to identify errors in specifications or domain theory. It plays an important role in the everyday use of the synthesis system by explaining to users what parts of a specification or of the domain theory contribute to what pieces of a generated program. Comments are inserted into the synthesized code that document these explanations.

VanBaalen, Jeffrey↗
NASA NTRS1997

Towards High-Assurance High-Performance Program Synthesis

Domain-specific automatic program synthesis tools, also called application generators, are playing an ever-increasing role in software development. However, high-performance application generators require difficult manual construction, and are very difficult to verify correct. This paper describes research and an implemented system that transforms program synthesis tools based on deductive synthesis into high-performance application generators. Deductive synthesis uses theorem-proving to construct solutions when given problem specifications. The verification condition for a deductive synthesis tool is essentially the soundness of the implemented inference rules. Theory Operationalization for Program Synthesis (TOPS) synergistically combines reformulation, automated mathematical classification, and compilation through partial deduction to decision procedures. It transforms general-purpose deductive synthesis, with exponential performance, into efficient special-purpose deductive synthesis, with near-linear performance. This paper describes our experience with and empirical results of PD(TH) theory-based partial deduction - in which partial deduction of a set of first-order formulae is performed within the context of a background theory. The implemented TOPS system currently performs a special variant of PD(TH) in which the compilation process results in the transformation of a set of first order formulae into the theory of an instantiated library decision procedure augmented by a compiled unit theory.

Lowry, Michael↗
NASA NTRS1994

AMPHION: Specification-based programming for scientific subroutine libraries

AMPHION is a knowledge-based software engineering (KBSE) system that guides a user in developing a diagram representing a formal problem specification. It then automatically implements a solution to this specification as a program consisting of calls to subroutines from a library. The diagram provides an intuitive domain oriented notation for creating a specification that also facilitates reuse and modification. AMPHION'S architecture is domain independent. AMPHION is specialized to an application domain by developing a declarative domain theory. Creating a domain theory is an iterative process that currently requires the joint expertise of domain experts and experts in automated formal methods for software development.

Lowry, Michael↗
NASA NTRS1994

A Formal Approach to Domain-Oriented Software Design Environments

This paper describes a formal approach to domain-oriented software design environments, based on declarative domain theories, formal specifications, and deductive program synthesis. A declarative domain theory defines the semantics of a domain-oriented specification language and its relationship to implementation-level subroutines. Formal specification development and reuse is made accessible to end-users through an intuitive graphical interface that guides them in creating diagrams denoting formal specifications. The diagrams also serve to document the specifications. Deductive program synthesis ensures that end-user specifications are correctly implemented. AMPHION has been applied to the domain of solar system kinematics through the development of a declarative domain theory, which includes an axiomatization of JPL's SPICELIB subroutine library. Testing over six months with planetary scientists indicates that AMPHION's interactive specification acquisition paradigm enables users to develop, modify, and reuse specifications at least an order of magnitude more rapidly than manual program development. Furthermore, AMPHION synthesizes one to two page programs consisting of calls to SPICELIB subroutines from these specifications in just a few minutes. Test results obtained by metering AMPHION's deductive program synthesis component are examined. AMPHION has been installed at JPL and is currently undergoing further refinement in preparation for distribution to hundreds of SPICELIB users worldwide. Current work to support end-user customization of AMPHION's specification acquisition subsystem is briefly discussed, as well as future work to enable domain-expert creation of new AMPHION applications through development of suitable domain theories.

Lowry, Michael↗
NASA NTRS1994

User Interface Technology for Formal Specification Development

Formal specification development and modification are an essential component of the knowledge-based software life cycle. User interface technology is needed to empower end-users to create their own formal specifications. This paper describes the advanced user interface for AMPHION1 a knowledge-based software engineering system that targets scientific subroutine libraries. AMPHION is a generic, domain-independent architecture that is specialized to an application domain through a declarative domain theory. Formal specification development and reuse is made accessible to end-users through an intuitive graphical interface that provides semantic guidance in creating diagrams denoting formal specifications in an application domain. The diagrams also serve to document the specifications. Automatic deductive program synthesis ensures that end-user specifications are correctly implemented. The tables that drive AMPHION's user interface are automatically compiled from a domain theory; portions of the interface can be customized by the end-user. The user interface facilitates formal specification development by hiding syntactic details, such as logical notation. It also turns some of the barriers for end-user specification development associated with strongly typed formal languages into active sources of guidance, without restricting advanced users. The interface is especially suited for specification modification. AMPHION has been applied to the domain of solar system kinematics through the development of a declarative domain theory. Testing over six months with planetary scientists indicates that AMPHION's interactive specification acquisition paradigm enables users to develop, modify, and reuse specifications at least an order of magnitude more rapidly than manual program development.

Lowry, Michael↗