Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Formal Methods”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

At least 235 records · Page 13
All sourcesNASA NTRSDOE OSTI
NASA NTRS1982

Advanced flight control system study

A fly by wire flight control system architecture designed for high reliability includes spare sensor and computer elements to permit safe dispatch with failed elements, thereby reducing unscheduled maintenance. A methodology capable of demonstrating that the architecture does achieve the predicted performance characteristics consists of a hierarchy of activities ranging from analytical calculations of system reliability and formal methods of software verification to iron bird testing followed by flight evaluation. Interfacing this architecture to the Lockheed S-3A aircraft for flight test is discussed. This testbed vehicle can be expanded to support flight experiments in advanced aerodynamics, electromechanical actuators, secondary power systems, flight management, new displays, and air traffic control concepts.

Hartmann, G. L.↗
NASA NTRS1987

Software reliability perspectives

Software which is used in life critical functions must be known to be highly reliable before installation. This requires a strong testing program to estimate the reliability, since neither formal methods, software engineering nor fault tolerant methods can guarantee perfection. Prior to the final testing software goes through a debugging period and many models have been developed to try to estimate reliability from the debugging data. However, the existing models are poorly validated and often give poor performance. This paper emphasizes the fact that part of their failures can be attributed to the random nature of the debugging data given to these models as input, and it poses the problem of correcting this defect as an area of future research.

Wilson, Larry↗
NASA NTRS1989

A methodology for commonality analysis, with applications to selected space station systems

The application of commonality in a system represents an attempt to reduce costs by reducing the number of unique components. A formal method for conducting commonality analysis has not been established. In this dissertation, commonality analysis is characterized as a partitioning problem. The cost impacts of commonality are quantified in an objective function, and the solution is that partition which minimizes this objective function. Clustering techniques are used to approximate a solution, and sufficient conditions are developed which can be used to verify the optimality of the solution. This method for commonality analysis is general in scope. It may be applied to the various types of commonality analysis required in the conceptual, preliminary, and detail design phases of the system development cycle.

Thomas, Lawrence Dale↗
NASA NTRS1989

The Sizing and Optimization Language (SOL): A computer language to improve the user/optimizer interface

The nonlinear mathematical programming method (formal optimization) has had many applications in engineering design. A figure illustrates the use of optimization techniques in the design process. The design process begins with the design problem, such as the classic example of the two-bar truss designed for minimum weight as seen in the leftmost part of the figure. If formal optimization is to be applied, the design problem must be recast in the form of an optimization problem consisting of an objective function, design variables, and constraint function relations. The middle part of the figure shows the two-bar truss design posed as an optimization problem. The total truss weight is the objective function, the tube diameter and truss height are design variables, with stress and Euler buckling considered as constraint function relations. Lastly, the designer develops or obtains analysis software containing a mathematical model of the object being optimized, and then interfaces the analysis routine with existing optimization software such as CONMIN, ADS, or NPSOL. This final state of software development can be both tedious and error-prone. The Sizing and Optimization Language (SOL), a special-purpose computer language whose goal is to make the software implementation phase of optimum design easier and less error-prone, is presented.

Lucas, S. H.↗
NASA NTRS1989

Human aspects of mission safety

Recent discussions of psychology's involvement in spaceflight have emphasized its role in enhancing space living conditions and incresing crew productivity. While these goals are central to space missions, behavioral scientists should not lose sight of a more basic flight requirement - that of crew safety. This paper examines some of the processes employed in the American space program in support of crew safety and suggests that behavioral scientists could contribute to flight safety, both through these formal processes and through less formal methods. Various safety areas of relevance to behavioral scientists are discussed.

Connors, Mary M.↗
NASA NTRS1990

What FM can offer DFCS design

The results of aircrafts and spacecrafts flight tests are reported. It is shown that the problems of Digital Flight Control Systems (DFCS) are the problems of systems whose complexity has exceeded the reach of the intellectual tools employed. It is also shown that intuition, experience, and techniques derived from mechanical and analog systems are insufficient for complex, integrated, digital systems. Formal Methods (FM) of computer science can offer DFCS systematic techniques for the construction of trustworthy software, including: techniques for the precise specification of requirements and the development of designs; systematic approaches to the design and structuring of distributed and concurrent systems; fault tolerance algorithms; and systematic methods of testing and analytic methods of verification.

Rushby, John↗
NASA NTRS1990

Vibration and wave propagation characteristics of multisegmented elastic beams

Closed form analytical solutions are derived for the vibration and wave propagation of multisegmented elastic beams. Each segment is modeled as a Timoshenko beam with possible inclusion of material viscosity, elastic foundation and axial forces. Solutions are obtained by using transfer matrix methods. According to these methods formal solutions are first constructed which relate the deflection, slope, moment and shear force of one end of the individual segment to those of the other. By satisfying appropriate continuity conditions at segment junctions, a global 4x4 matrix results which relates the deflection, slope, moment and shear force of one end of the beam to those of the other. If any boundary conditions are subsequently invoked on the ends of the beam one gets the appropriate characteristic equation for the natural frequencies. Furthermore, by invoking appropriate periodicity conditions the dispersion relation for a periodic system is obtained. A variety of numerical examples are included.

Nayfeh, Adnan H.↗
NASA NTRS1991

Integrity and security in an Ada runtime environment

A review is provided of the Formal Methods group discussions. It was stated that integrity is not a pure mathematical dual of security. The input data is part of the integrity domain. The group provided a roadmap for research. One item of the roadmap and the final position statement are closely related to the space shuttle and space station. The group's position is to use a safe subset of Ada. Examples of safe sets include the Army Secure Operating System and the Penelope Ada verification tool. It is recommended that a conservative attitude is required when writing Ada code for life and property critical systems.

Bown, Rodney L.↗
NASA NTRS1991

Formal specification and verification of Ada software

The use of formal methods in software development achieves levels of quality assurance unobtainable by other means. The Larch approach to specification is described, and the specification of avionics software designed to implement the logic of a flight control system is given as an example. Penelope is described which is an Ada-verification environment. The Penelope user inputs mathematical definitions, Larch-style specifications and Ada code and performs machine-assisted proofs that the code obeys its specifications. As an example, the verification of a binary search function is considered. Emphasis is given to techniques assisting the reuse of a verification effort on modified code.

Hird, Geoffrey R.↗
NASA NTRS1992

Formal design specification of a Processor Interface Unit

This report describes work to formally specify the requirements and design of a processor interface unit (PIU), a single-chip subsystem providing memory-interface bus-interface, and additional support services for a commercial microprocessor within a fault-tolerant computer system. This system, the Fault-Tolerant Embedded Processor (FTEP), is targeted towards applications in avionics and space requiring extremely high levels of mission reliability, extended maintenance-free operation, or both. The need for high-quality design assurance in such applications is an undisputed fact, given the disastrous consequences that even a single design flaw can produce. Thus, the further development and application of formal methods to fault-tolerant systems is of critical importance as these systems see increasing use in modern society.

Fura, David A.↗
NASA NTRS1991

Verification of VLSI designs

In this paper we explore the specification and verification of VLSI designs. The paper focuses on abstract specification and verification of functionality using mathematical logic as opposed to low-level boolean equivalence verification such as that done using BDD's and Model Checking. Specification and verification, sometimes called formal methods, is one tool for increasing computer dependability in the face of an exponentially increasing testing effort.

Windley, P. J.↗
NASA NTRS1994

Technology Benefit Estimator (T/BEST): User's Manual

The Technology Benefit Estimator (T/BEST) system is a formal method to assess advanced technologies and quantify the benefit contributions for prioritization. T/BEST may be used to provide guidelines to identify and prioritize high payoff research areas, help manage research and limited resources, show the link between advanced concepts and the bottom line, i.e., accrued benefit and value, and to communicate credibly the benefits of research. The T/BEST software computer program is specifically designed to estimating benefits, and benefit sensitivities, of introducing new technologies into existing propulsion systems. Key engine cycle, structural, fluid, mission and cost analysis modules are used to provide a framework for interfacing with advanced technologies. An open-ended, modular approach is used to allow for modification and addition of both key and advanced technology modules. T/BEST has a hierarchical framework that yields varying levels of benefit estimation accuracy that are dependent on the degree of input detail available. This hierarchical feature permits rapid estimation of technology benefits even when the technology is at the conceptual stage. As knowledge of the technology details increases the accuracy of the benefit analysis increases. Included in T/BEST's framework are correlations developed from a statistical data base that is relied upon if there is insufficient information given in a particular area, e.g., fuel capacity or aircraft landing weight. Statistical predictions are not required if these data are specified in the mission requirements. The engine cycle, structural fluid, cost, noise, and emissions analyses interact with the default or user material and component libraries to yield estimates of specific global benefits: range, speed, thrust, capacity, component life, noise, emissions, specific fuel consumption, component and engine weights, pre-certification test, mission performance engine cost, direct operating cost, life cycle cost, manufacturing cost, development cost, risk, and development time. Currently, T/BEST operates on stand-alone or networked workstations, and uses a UNIX shell or script to control the operation of interfaced FORTRAN based analyses. T/BEST's interface structure works equally well with non-FORTRAN or mixed software analysis. This interface structure is designed to maintain the integrity of the expert's analyses by interfacing with expert's existing input and output files. Parameter input and output data (e.g., number of blades, hub diameters, etc.) are passed via T/BEST's neutral file, while copious data (e.g., finite element models, profiles, etc.) are passed via file pointers that point to the expert's analyses output files. In order to make the communications between the T/BEST's neutral file and attached analyses codes simple, only two software commands, PUT and GET, are required. This simplicity permits easy access to all input and output variables contained within the neutral file. Both public domain and proprietary analyses codes may be attached with a minimal amount of effort, while maintaining full data and analysis integrity, and security. T/BESt's sotware framework, status, beginner-to-expert operation, interface architecture, analysis module addition, and key analysis modules are discussed. Representative examples of T/BEST benefit analyses are shown.

Generazio, Edward R.↗
NASA NTRS1994

The navigation toolkit

This report summarizes the experience of the authors in managing, designing, and implementing an object-oriented applications framework for orbital navigation analysis for the Flight Design and Dynamics Department of the Rockwell Space Operations Company in Houston, in support of the Mission Operations Directorate of NASA's Johnson Space Center. The 8 person year project spanned 1.5 years and produced 30,000 lines of C++ code, replacing 150,000 lines of Fortran/C. We believe that our experience is important because it represents a 'second project' experience and generated real production-quality code - it was not a pilot. The project successfully demonstrated the use of 'continuous development' or rapid prototyping techniques. Use of formal methods and executable models contributed to the quality of the code. Keys to the success of the project were a strong architectural vision and highly skilled workers. This report focuses on process and methodology, and not on a detailed design description of the product. But the true importance of the object-oriented paradigm is its liberation of the developer to focus on the problem rather than the means used to solve the problem.

Rich, William F.↗
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 NTRS1995

T/BEST: Technology Benefit Estimator Select Features and Applications

A Technology Benefit Estimator (T/BEST) system has been developed to provide a formal method to assess advanced aerospace technologies and quantify the benefit contributions for prioritization. An open-ended, modular approach is used to allow for upgrade and insertion of advanced technology modules. T/BEST's software framework, beginner-to-expert operation, interface architecture, and key analysis modules are discussed. In this paper, selected features and applications of T/BEST are demonstrated. Sample cases pertaining to structural analysis of titanium and composite blades are presented. The performance of hot and cold composite fan blades is also discussed. The cost required to manufacture titanium and composite fan blades is estimated.

Generazio, Edward R.↗
NASA NTRS1998

An Integrated Environment for Efficient Formal Design and Verification

The general goal of this project was to improve the practicality of formal methods by combining techniques from model checking and theorem proving. At the time the project was proposed, the model checking and theorem proving communities were applying different tools to similar problems, but there was not much cross-fertilization. This project involved a group from SRI that had substantial experience in the development and application of theorem-proving technology, and a group at Stanford that specialized in model checking techniques. Now, over five years after the proposal was submitted, there are many research groups working on combining theorem-proving and model checking techniques, and much more communication between the model checking and theorem proving research communities. This project contributed significantly to this research trend. The research work under this project covered a variety of topics: new theory and algorithms; prototype tools; verification methodology; and applications to problems in particular domains.

Source record↗