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 361 records · Page 20
All sourcesNASA NTRSDOE OSTI
NASA NTRS1985

One-dimensional kinematics of particle stream flow with application to solar wind simulation

A simple kinematic method for determining the particle velocity distribution of a model solar wind for which the spatial distribution of particles is given as a function of particle travel time has been developed by Hakamada and Akasofu (1982). Here their method is formalized mathematically and an inverse procedure for determining the particle distribution from a given velocity distribution is derived. This inverse procedure is then applied to a simulated velocity distribution obtained from an MHD finite difference code.

Olmsted, C.↗
NASA NTRS1991

A case study for the real-time experimental evaluation of the VIPER microprocessor

An experiment to evaluate the applicability of the Verifiable Integrated Processor for Enhanced Reliability (VIPER) microprocessor to real time control is described. The VIPER microprocessor was invented by the Royal Signals and Radar Establishment (RSRE), U.K., and is an example of the use of formal mathematical methods for developing electronic digital systems with a high degree of assurance on the system design and implementation correctness. The experiment consisted of selecting a control law, writing the control law algorithm for the VIPER processor, and providing real time, dynamic inputs into the processor and monitoring the outputs. The control law selected and coded for the VIPER processor was the yaw damper function of an automatic landing program for a 737 aircraft. The mechanisms for interfacing the VIPER Single Board Computer to the VAX host are described. Results include run time experiences, performance evaluation, and comparison of VIPER and FORTRAN yaw damper algorithm output for accuracy estimation.

Carreno, Victor A.↗
NASA NTRS1991

Estimation of time averages from irregularly spaced observations - With application to coastal zone color scanner estimates of chlorophyll concentration

The sampling error of an arbitrary linear estimate of a time-averaged quantity constructed from a time series of irregularly spaced observations at a fixed located is quantified through a formalism. The method is applied to satellite observations of chlorophyll from the coastal zone color scanner. The two specific linear estimates under consideration are the composite average formed from the simple average of all observations within the averaging period and the optimal estimate formed by minimizing the mean squared error of the temporal average based on all the observations in the time series. The resulting suboptimal estimates are shown to be more accurate than composite averages. Suboptimal estimates are also found to be nearly as accurate as optimal estimates using the correct signal and measurement error variances and correlation functions for realistic ranges of these parameters, which makes it a viable practical alternative to the composite average method generally employed at present.

Chelton, Dudley B.↗
NASA NTRS1991

Formal and heuristic system decomposition methods in multidisciplinary synthesis

The multidisciplinary interactions which exist in large scale engineering design problems provide a unique set of difficulties. These difficulties are associated primarily with unwieldy numbers of design variables and constraints, and with the interdependencies of the discipline analysis modules. Such obstacles require design techniques which account for the inherent disciplinary couplings in the analyses and optimizations. The objective of this work was to develop an efficient holistic design synthesis methodology that takes advantage of the synergistic nature of integrated design. A general decomposition approach for optimization of large engineering systems is presented. The method is particularly applicable for multidisciplinary design problems which are characterized by closely coupled interactions among discipline analyses. The advantage of subsystem modularity allows for implementation of specialized methods for analysis and optimization, computational efficiency, and the ability to incorporate human intervention and decision making in the form of an expert systems capability. The resulting approach is not a method applicable to only a specific situation, but rather, a methodology which can be used for a large class of engineering design problems in which the system is non-hierarchic in nature.

Bloebaum, Christina L.↗
NASA NTRS1991

How to help intelligent systems with different uncertainty representations cooperate with each other

In order to solve a complicated problem one must use the knowledge from different domains. Therefore, if one wants to automatize the solution of these problems, one has to help the knowledge-based systems that correspond to these domains cooperate, that is, communicate facts and conclusions to each other in the process of decision making. One of the main obstacles to such cooperation is the fact that different intelligent systems use different methods of knowledge acquisition and different methods and formalisms for uncertainty representation. So an interface f is needed, 'translating' the values x, y, which represent uncertainty of the experts' knowledge in one system, into the values f(x), f(y) appropriate for another one. The problem of designing such an interface as a mathematical problem is formulated and solved. It is shown that the interface must be fractionally linear: f(x) = (ax + b)/(cx + d).

Kreinovich, Vladik YA.↗
NASA NTRS1992

Large project experiences with object-oriented methods and reuse

The SSVTF (Space Station Verification and Training Facility) project is completing the Preliminary Design Review of a large software development using object-oriented methods and systematic reuse. An incremental developmental lifecycle was tailored to provide early feedback and guidance on methods and products, with repeated attention to reuse. Object oriented methods were formally taught and supported by realistic examples. Reuse was readily accepted and planned by the developers. Schedule and budget issues were handled by agreements and work sharing arranged by the developers.

Wessale, William↗
NASA NTRS1993

The quantum dynamics of electronically nonadiabatic chemical reactions

Considerable progress was achieved on the quantum mechanical treatment of electronically nonadiabatic collisions involving energy transfer and chemical reaction in the collision of an electronically excited atom with a molecule. In the first step, a new diabatic representation for the coupled potential energy surfaces was created. A two-state diabatic representation was developed which was designed to realistically reproduce the two lowest adiabatic states of the valence bond model and also to have the following three desirable features: (1) it is more economical to evaluate; (2) it is more portable; and (3) all spline fits are replaced by analytic functions. The new representation consists of a set of two coupled diabatic potential energy surfaces plus a coupling surface. It is suitable for dynamics calculations on both the electronic quenching and reaction processes in collisions of Na(3p2p) with H2. The new two-state representation was obtained by a three-step process from a modified eight-state diatomics-in-molecules (DIM) representation of Blais. The second step required the development of new dynamical methods. A formalism was developed for treating reactions with very general basis functions including electronically excited states. Our formalism is based on the generalized Newton, scattered wave, and outgoing wave variational principles that were used previously for reactive collisions on a single potential energy surface, and it incorporates three new features: (1) the basis functions include electronic degrees of freedom, as required to treat reactions involving electronic excitation and two or more coupled potential energy surfaces; (2) the primitive electronic basis is assumed to be diabatic, and it is not assumed that it diagonalizes the electronic Hamiltonian even asymptotically; and (3) contracted basis functions for vibrational-rotational-orbital degrees of freedom are included in a very general way, similar to previous prescriptions for locally adiabatic functions in various quantum scattering algorithms.

Truhlar, Donald G.↗
NASA NTRS1994

Derivation and experimental verification of clock synchronization theory

The objective of this work is to validate mathematically derived clock synchronization theories and their associated algorithms through experiment. Two theories are considered, the Interactive Convergence Clock Synchronization Algorithm and the Mid-Point Algorithm. Special clock circuitry was designed and built so that several operating conditions and failure modes (including malicious failures) could be tested. Both theories are shown to predict conservative upper bounds (i.e., measured values of clock skew were always less than the theory prediction). Insight gained during experimentation led to alternative derivations of the theories. These new theories accurately predict the clock system's behavior. It is found that a 100% penalty is paid to tolerate worst case failures. It is also shown that under optimal conditions (with minimum error and no failures) the clock skew can be as much as 3 clock ticks. Clock skew grows to 6 clock ticks when failures are present. Finally, it is concluded that one cannot rely solely on test procedures or theoretical analysis to predict worst case conditions. conditions.

INTERACTIVE CONVERGENCE CLOCK↗
NASA NTRS1995

Model checking

Automatic formal verification methods for finite-state systems, also known as model-checking, successfully reduce labor costs since they are mostly automatic. Model checkers explicitly or implicitly enumerate the reachable state space of a system, whose behavior is described implicitly, perhaps by a program or a collection of finite automata. Simple properties, such as mutual exclusion or absence of deadlock, can be checked by inspecting individual states. More complex properties, such as lack of starvation, require search for cycles in the state graph with particular properties. Specifications to be checked may consist of built-in properties, such as deadlock or 'unspecified receptions' of messages, another program or implicit description, to be compared with a simulation, bisimulation, or language inclusion relation, or an assertion in one of several temporal logics. Finite-state verification tools are beginning to have a significant impact in commercial designs. There are many success stories of verification tools finding bugs in protocols or hardware controllers. In some cases, these tools have been incorporated into design methodology. Research in finite-state verification has been advancing rapidly, and is showing no signs of slowing down. Recent results include probabilistic algorithms for verification, exploitation of symmetry and independent events, and the use symbolic representations for Boolean functions and systems of linear inequalities. One of the most exciting areas for further research is the combination of model-checking with theorem-proving methods.

Dill, David L.↗
NASA NTRS2004

Spray Characteristics of a Hybrid Twin-Fluid Pressure-Swirl Atomizer

The spray performance of a fuel injection system applicable for use in main combustion chamber of an oxidizer-rich staged combustion (ORSC) cycles is presented. The experimental data reported here include mean drop size and drop size distribution, spray cone half-angle, and momentum rate (directly related to spray penetration). The maximum entropy formalism, MEF, method to predict drop size distribution is applied and compared to the experimental data. Geometric variables considered include the radius of the injector inlet orifice plate through which oxidizer flows (&) and the exposed length from the fuel inlet to the injector exit plane (L2). Operating conditions that were varied include the liquid mass flow rate and air mass flow rate. For orifices B and C there is a significant dependence of D3Z on both the air and liquid mass flow rates, as well as on L2. For the A orifice, the momentum rate of the air flow appears to exceed a threshold value above which a constant D32 is obtained. Using the MEF method, a semi-analytical process was developed to model the spray distribution using two input parameters (q = 0.4 and Dso). The momentum rate of the spray is directly related to the air and liquid mass flow rates. The cone half angle of the spray ranges from 25 to 17 degrees. The data resulting from this project will eventually be used to develop advanced rocket systems.

Durham, M. J.↗
NASA NTRS1997

T/BEST: Technology Benefit Estimator for Composites and Applications to Engine Structures

Progress in the field of aerospace propulsion has heightened the need to combine advanced technologies. These benefits will provide guidelines for identifying and prioritizing high-payoff research areas, will help manage research with limited resources, and will show the link between advanced and basic concepts. An effort was undertaken at the NASA Lewis Research Center to develop a formal computational method, T/BEST (Technology Benefit Estimator), to assess advanced aerospace technologies, such as fibrous composites, and credibly communicate the benefits of research. Fibrous composites are ideal for structural applications such as high-performance aircraft engine blades where high strength-to-weight and stiffness-to-weight ratios are required. These factors - along with the flexibility to select the composite system and layup, and to favorably orient fiber directions - reduce the displacements and stresses caused by large rotational speeds in aircraft engines.

Chamis, Christos↗
NASA NTRS2005

Autonomous and Autonomic Swarms

A watershed in systems engineering is represented by the advent of swarm-based systems that accomplish missions through cooperative action by a (large) group of autonomous individuals each having simple capabilities and no global knowledge of the group s objective. Such systems, with individuals capable of surviving in hostile environments, pose unprecedented challenges to system developers. Design and testing and verification at much higher levels will be required, together with the corresponding tools, to bring such systems to fruition. Concepts for possible future NASA space exploration missions include autonomous, autonomic swarms. Engineering swarm-based missions begins with understanding autonomy and autonomicity and how to design, test, and verify systems that have those properties and, simultaneously, the capability to accomplish prescribed mission goals. Formal methods-based technologies, both projected and in development, are described in terms of their potential utility to swarm-based system developers.

Hinchey, Michael G.↗
NASA NTRS2006

Electron-He(+) P-wave Elastic Scattering and Photoabsorption in Two-electron Systems

In a previous paper [Bhatia, Phys. Rev. A 69,032714 (2004)], electron-hydrogen P-wave scattering phase shifts were calculated using the optical potential approach based on the Feshbach projection operator formalism. This method is now extended to the singlet and triplet electron-He(+) P-wave scattering in the elastic region. Phase shifts are calculated using Hylleraas-type correlation functions with up to 220 terms. Results are rigorous lower bounds to the exact phase shifts and they are compared to phase shifts obtained from the method of polarized orbitals and close-coupling calculations. The continuum functions calculated here are used to calculate photoabsorption cross sections. Photoionization cross sections of He and photodetachment cross sections of H(-) are calculated in the elastic region, i.e. leaving He(+) and H in their respective ground states, and compared with previous calculations. Radiative attachment rates are also calculated.

Bhatia, A. K.↗
NASA NTRS2003

Model checking for software security properties

This paper describes the use of the Flexible Modeling Framework (FMF) for model checking (MC) to perform and search for vulnerabilities in the Secure Socket Layer (SSL) communication protocol.

model checking formal methods software security↗