Engineering topics

Pressburger, Thomas

Publications and source records attributed to Pressburger, Thomas.

14 records

NASA NTRS2020

Formal Requirements Elicitation with FRET

FRET is a tool for writing, understanding, formalizing and analyzing requirements. Users write requirements in an intuitive, restricted natural language, called FRETISH, with precise, unambiguous meaning. For a FRETISH requirement, FRET: 1) produces natural language and diagrammatic explanations of its exact meaning, 2) formalizes the requirement in logics, and 3) supports interactive simulation of produced logic formulas to ensure that they capture user intentions. FRET connects to analysis tools by facilitating the mapping between requirements and models/code, and by generating verification code. FRET is available open source at https://github.com/NASA-SW-VnV/fret; a video can be accessed at : https://tinyurl.com/fretForREFSQ.

Giannakopoulou, Dimitra↗

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 NTRS2006

Infusing Software Engineering Technology into Practice at NASA

We present an ongoing effort of the NASA Software Engineering Initiative to encourage the use of advanced software engineering technology on NASA projects. Technology infusion is in general a difficult process yet this effort seems to have found a modest approach that is successful for some types of technologies. We outline the process and describe the experience of the technology infusions that occurred over a two year period. We also present some lessons from the experiences.

software assurance↗

NASA NTRS2006

Infusing Software Assurance Research Techniques into Use

Research in the software engineering community continues to lead to new development techniques that encompass processes, methods and tools. However, a number of obstacles impede their infusion into software development practices. These are the recurring obstacles common to many forms of research. Practitioners cannot readily identify the emerging techniques that may benefit them, and cannot afford to risk time and effort evaluating and trying one out while there remains uncertainty about whether it will work for them. Researchers cannot readily identify the practitioners whose problems would be amenable to their techniques, and, lacking feedback from practical applications, are hard-pressed to gauge the where and in what ways to evolve their techniques to make them more likely to be successful. This paper describes an ongoing effort conducted by a software engineering research infusion team established by NASA s Software Engineering Initiative to overcome these obstacles. .

Pressburger, Thomas↗

NASA NTRS2006

The NASA Software Research Infusion Initiative: Successful Technology Transfer for Software Assurance

New processes, methods and tools are constantly appearing in the field of software engineering. Many of these augur great potential in improving software development processes, resulting in higher quality software with greater levels of assurance. However, there are a number of obstacles that impede their infusion into software development practices. These are the recurring obstacles common to many forms of research. Practitioners cannot readily identify the emerging techniques that may most benefit them, and cannot afford to risk time and effort in evaluating and experimenting with them while there is still uncertainty about whether they will have payoff in this particular context. Similarly, researchers cannot readily identify those practitioners whose problems would be amenable to their techniques and lack the feedback from practical applications necessary to help them to evolve their techniques to make them more likely to be successful. This paper describes an ongoing effort conducted by a software engineering research infusion team, and the NASA Research Infusion Initiative, established by NASA s Software Engineering Initiative, to overcome these obstacles.

Hinchey, Michael G.↗

NASA NTRS2005

Infusing software assurance research techniques into use

Research in the software engineering community continues to lead to new development techniques that encompass processes, methods and tools. However, a number of obstacles impede their infusion into software deveopment practices. This paper describes an ongoing effort conducted by a software engineering research infusion team established by NASA's Software Engineering Intiative to overcome these obstacles.

Trevino, Luis C.↗

NASA NTRS2001

The AutoBayes Program Synthesis System: System Description

AUTOBAYES is a fully automatic program synthesis system for the statistical data analysis domain. Its input is a concise description of a data analysis problem in the form of a statistical model; its output is optimized and fully documented C/C++ code which can be linked dynamically into the Matlab and Octave environments. AUTOBAYES synthesizes code by a schema-guided deductive process. Schemas (i.e., code templates with associated semantic constraints) are applied to the original problem and recursively to emerging subproblems. AUTOBAYES complements this approach by symbolic computation to derive closed-form solutions whenever possible. In this paper, we concentrate on the interaction between the symbolic computations and the deductive synthesis process. A statistical model specifies for each problem variable (i.e., data or parameter) its properties and dependencies in the form of a probability distribution, A typical data analysis task is to estimate the best possible parameter values from the given observations or measurements. The following example models normal-distributed data but takes prior information (e.g., from previous experiments) on the data's mean value and variance into account.

Fischer, Bernd↗

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 NTRS2000

Model Checking JAVA Programs Using Java Pathfinder

This paper describes a translator called JAVA PATHFINDER from JAVA to PROMELA, the "programming language" of the SPIN model checker. The purpose is to establish a framework for verification and debugging of JAVA programs based on model checking. This work should be seen in a broader attempt to make formal methods applicable "in the loop" of programming within NASA's areas such as space, aviation, and robotics. Our main goal is to create automated formal methods such that programmers themselves can apply these in their daily work (in the loop) without the need for specialists to manually reformulate a program into a different notation in order to analyze the program. This work is a continuation of an effort to formally verify, using SPIN, a multi-threaded operating system programmed in Lisp for the Deep-Space 1 spacecraft, and of previous work in applying existing model checkers and theorem provers to real applications.

Havelund, Klaus↗

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

Automated Reuse of Scientific Subroutine Libraries through Deductive Synthesis

Systematic software construction offers the potential of elevating software engineering from an art-form to an engineering discipline. The desired result is more predictable software development leading to better quality and more maintainable software. However, the overhead costs associated with the formalisms, mathematics, and methods of systematic software construction have largely precluded their adoption in real-world software development. In fact, many mainstream software development organizations, such as Microsoft, still maintain a predominantly oral culture for software development projects; which is far removed from a formalism-based culture for software development. An exception is the limited domain of safety-critical software, where the high-assuiance inherent in systematic software construction justifies the additional cost. We believe that systematic software construction will only be adopted by mainstream software development organization when the overhead costs have been greatly reduced. Two approaches to cost mitigation are reuse (amortizing costs over many applications) and automation. For the last four years, NASA Ames has funded the Amphion project, whose objective is to automate software reuse through techniques from systematic software construction. In particular, deductive program synthesis (i.e., program extraction from proofs) is used to derive a composition of software components (e.g., subroutines) that correctly implements a specification. The construction of reuse libraries of software components is the standard software engineering solution for improving software development productivity and quality.

Lowry, Michael R.↗

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↗