Engineering topics

Holloway, C. Michael

Publications and source records attributed to Holloway, C. Michael.

28 records · Page 2

NASA NTRS1998

Streamlining Software Aspects of Certification: Technical Team Report on the First Industry Workshop

To address concerns about time and expense associated with software aspects of certification, the Federal Aviation Administration (FAA) began the Streamlining Software Aspects of Certification (SSAC) program. As part of this program, a Technical Team was established to determine whether the cost and time associated with certifying aircraft can be reduced while maintaining or improving safety, with the intent of impacting the FAA's Flight 2000 program. The Technical Team conducted a workshop to gain a better understanding of the major concerns in industry about software cost and schedule. Over 120 people attended the workshop, including representatives from the FAA,commercial transport and general aviation aircraft manufacturers and suppliers, and procurers and developers of non-airborne systems; and, more than 200 issues about software aspects of certification were recorded. This paper provides an overview of the SSAC program, motivation for the workshop, details of the workshop activities and outcomes, and recommendations for follow-on work.

Hayhurst, Kelly J.↗

NASA NTRS1997

Fourth NASA Langley Formal Methods Workshop

This publication consists of papers presented at NASA Langley Research Center's fourth workshop on the application of formal methods to the design and verification of life-critical systems. Topic considered include: Proving properties of accident; modeling and validating SAFER in VDM-SL; requirement analysis of real-time control systems using PVS; a tabular language for system design; automated deductive verification of parallel systems. Also included is a fundamental hardware design in PVS.

Holloway, C. Michael↗

NASA NTRS1997

Why Engineers Should Consider Formal Methods

This paper presents a logical analysis of a typical argument favoring the use of formal methods for software development, and suggests an alternative argument that is simpler and stronger than the typical one.

Holloway, C. Michael↗

NASA NTRS1995

Third NASA Langley Formal Methods Workshop

This publication constitutes the proceedings of NASA Langley Research Center's third workshop on the application of formal methods to the design and verification of life-critical systems. This workshop brought together formal methods researchers, industry engineers, and academicians to discuss the potential of NASA-sponsored formal methods and to investigate new opportunities for applying these methods to industry problems. contained herein are copies of the material presented at the workshop, summaries of many of the presentations, a complete list of attendees, and a detailed summary of the Langley formal methods program. Much of this material is available electronically through the World-Wide Web via the following URL.

Holloway, C. Michael↗

NASA NTRS1995

NASA Langley Research and Technology-Transfer Program in Formal Methods

This paper presents an overview of NASA Langley research program in formal methods. The major goals of this work are to make formal methods practical for use on life critical systems, and to orchestrate the transfer of this technology to U.S. industry through use of carefully designed demonstration projects. Several direct technology transfer efforts have been initiated that apply formal methods to critical subsystems of real aerospace computer systems. The research team consists of five NASA civil servants and contractors from Odyssey Research Associates, SRI International, and VIGYAN Inc.

Butler, Ricky W.↗

NASA NTRS1994

Epistemology, software engineering and formal methods

One of the most basic questions anyone can ask is, 'How do I know that what I think I know is true?' The study of this question is called epistemology. Traditionally, epistemology has been considered to be of legitimate interest only to philosophers, theologians, and three year old children who respond to every statement by asking, 'Why?' Software engineers need to be interested in the subject, however, because a lack of sufficient understanding of epistemology contributes to many of the current problems in the field.

Holloway, C. Michael↗

NASA NTRS1994

Formal design and verification of a reliable computing platform for real-time control (phase 3 results)

In this paper the design and formal verification of the lower levels of the Reliable Computing Platform (RCP), a fault-tolerant computing system for digital flight control applications, are presented. The RCP uses NMR-style redundancy to mask faults and internal majority voting to flush the effects of transient faults. Two new layers of the RCP hierarchy are introduced: the Minimal Voting refinement (DA_minv) of the Distributed Asynchronous (DA) model and the Local Executive (LE) Model. Both the DA_minv model and the LE model are specified formally and have been verified using the Ehdm verification system. All specifications and proofs are available electronically via the Internet using anonymous FTP or World Wide Web (WWW) access.

Butler, Ricky W.↗

NASA NTRS1992

The Second NASA Formal Methods Workshop 1992

The primary goal of the workshop was to bring together formal methods researchers and aerospace industry engineers to investigate new opportunities for applying formal methods to aerospace problems. The first part of the workshop was tutorial in nature. The second part of the workshop explored the potential of formal methods to address current aerospace design and verification problems. The third part of the workshop involved on-line demonstrations of state-of-the-art formal verification tools. Also, a detailed survey was filled in by the attendees; the results of the survey are compiled.

Johnson, Sally C.↗

NASA NTRS1992

The syntax of DRAGOON: Evaluation and recommendations

Several different ways to add linguistic support for object-oriented programming to the Ada programming language have been proposed and developed in recent years. The Distributable Reusable Ada Generated from an Object-Oriented Notation (DRAGOON) language is one such Ada extension. The DRAGOON syntax is described for classes, objects, and inheritance, and the syntax is evaluated against the following five criteria: readability, writeability, lack of ambiguity, ease of translation, and consistency with existing Ada syntax. The evaluation reveals several deficiencies in the notation. A revised syntax that corrects these deficiencies is proposed.

Holloway, C. Michael↗

NASA NTRS1987

Analysis of Ada as a prototyping language

This paper examines the suitability of Ada as a language for developing software prototypes. The differences between software prototypes and traditional engineering prototypes are discussed; the approaches to software prototyping are identified. Ada's potential as a language for prototyping is evaluated according to the writability, expressiveness, and flexibility of the language; Ada is found to be inadequate as a prototyping language because it lacks writability and expressiveness. Possible approaches to improving the expressiveness of the language are discussed.

Holloway, C. Michael↗