SEARCH · Engineering Papers

Results for “Integrated 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.

SourceResearch connectionFrom yearThrough year

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

At least 145 records · Page 8

All sources NASA NTRS DOE OSTI

NASA NTRSDate not supplied

Proof Mate: An Interactive Proof Helper for PVS (Tool Paper)

This paper presents Proof Mate, an interactive proof helper for the PVS verification system. The helper is integrated in VSCode-PVS, the Visual Studio Code extension for PVS. It extends the capabilities of VSCode-PVS by introducing new functionalities for suggesting proof commands, sketching proof attempts, and repairing broken proofs during interactive proof sessions. This work further aligns VSCode-PVS to the functionalities provided by modern development tools, with the ultimate aim to facilitate the adoption of formal methods in engineering practices and education.

Interactive Theorem Proving↗

NASA NTRSDate not supplied

Proof Mate: An Interactive Proof Helper for PVS

Formal Methods↗

NASA NTRS1995

Flight test validation of a frequency-based system identification method on an F-15 aircraft

A frequency-based performance identification approach was evaluated using flight data from the NASA F-15 Highly Integrated Digital Electronic Control aircraft. The approach used frequency separation to identify the effectiveness of multiple controls simultaneously as an alternative to independent control identification methods. Fourier transformations converted measured control and response data into frequency domain representations. Performance gradients were formed using multiterm frequency matching of control and response frequency domain models. An objective function was generated using these performance gradients. This function was formally optimized to produce a coordinated control trim set. This algorithm was applied to longitudinal acceleration and evaluated using two control effectors: nozzle throat area and inlet first ramp. Three criteria were investigated to validate the approach: simultaneous gradient identification, gradient frequency dependency, and repeatability. This report describes the flight test results. These data demonstrate that the approach can accurately identify performance gradients during simultaneous control excitation independent of excitation frequency.

Schkolnik, Gerard S.↗

NASA NTRS2006

Hard and Soft Constraints in Reliability-Based Design Optimization

This paper proposes a framework for the analysis and design optimization of models subject to parametric uncertainty where design requirements in the form of inequality constraints are present. Emphasis is given to uncertainty models prescribed by norm bounded perturbations from a nominal parameter value and by sets of componentwise bounded uncertain variables. These models, which often arise in engineering problems, allow for a sharp mathematical manipulation. Constraints can be implemented in the hard sense, i.e., constraints must be satisfied for all parameter realizations in the uncertainty model, and in the soft sense, i.e., constraints can be violated by some realizations of the uncertain parameter. In regard to hard constraints, this methodology allows (i) to determine if a hard constraint can be satisfied for a given uncertainty model and constraint structure, (ii) to generate conclusive, formally verifiable reliability assessments that allow for unprejudiced comparisons of competing design alternatives and (iii) to identify the critical combination of uncertain parameters leading to constraint violations. In regard to soft constraints, the methodology allows the designer (i) to use probabilistic uncertainty models, (ii) to calculate upper bounds to the probability of constraint violation, and (iii) to efficiently estimate failure probabilities via a hybrid method. This method integrates the upper bounds, for which closed form expressions are derived, along with conditional sampling. In addition, an l(sub infinity) formulation for the efficient manipulation of hyper-rectangular sets is also proposed.

Crespo, L.uis G.↗

NASA NTRS2007

Synthesis from Design Requirements of a Hybrid System for Transport Aircraft Longitudinal Control

Volume I of this report presents a new method for synthesizing hybrid systems directly from design requirements, and applies the method to design of a hybrid system for longitudinal control of transport aircraft. The resulting system satisfies general requirement for safety and effectiveness specified a priori, enabling formal validation to be achieved. Volume II contains seven appendices intended to make the report accessible to readers with backgrounds in human factors, fli ght dynamics and control. and formal logic. Major design goals are (1) system desi g n integrity based on proof of correctness at the design level, (2), significant simplification and cost reduction in system development and certification, and (3) improved operational efficiency, with significant alleviation of human-factors problems encountered by pilots in current transport aircraft. This report provides for the first time a firm technical basis for criteria governing design and certification of avionic systems for transport aircraft. It should be of primary interest to designers of next-generation avionic systems.

Hynes, Charles S.↗

DOE OSTI2025

Extracting scattering amplitudes for arbitrary two-particle systems with one-particle left-hand cuts via lattice QCD

We derive a general formalism that relates the spectrum of two-particle systems in a finite volume to physical scattering amplitudes, taking into account the presence of any left-hand branch cuts due to single-particle exchanges. The method first relates the finite-volume spectrum to an infinite-volume short-range quantity, denoted ${\mathcal{M}}_0$, and then relates the latter to the physical scattering amplitudes via known integral equations. The derivation of both relations is performed using all-orders perturbation theory and is exact up to neglected exponentially suppressed volume dependence. The relations hold for arbitrary two-particle systems with any number of coupled channels, non-identical and non-degenerate particles, and any intrinsic spin.

algorithms↗

NASA NTRS1995

Formal Methods Specification and Verification Guidebook for Software and Computer Systems: Planning and Technology Insertion - Volume 1

The Formal Methods Specification and Verification Guidebook for Software and Computer Systems describes a set of techniques called Formal Methods (FM), and outlines their use in the specification and verification of computer systems and software. Development of increasingly complex systems has created a need for improved specification and verification techniques. NASA's Safety and Mission Quality Office has supported the investigation of techniques such as FM, which are now an accepted method for enhancing the quality of aerospace applications. The guidebook provides information for managers and practitioners who are interested in integrating FM into an existing systems development process. Information includes technical and administrative considerations that must be addressed when establishing the use of FM on a specific project. The guidebook is intended to aid decision makers in the successful application of FM to the development of high-quality systems at reasonable cost. This is the first volume of a planned two-volume set. The current volume focuses on administrative and planning considerations for the successful application of FM.

Source record↗

NASA NTRSDate not supplied

NASA Aeronautics Research Mission Directorate System Security Engineering Approaches

System security engineering (SSE) is a set of formal engineering methods and is considered a subset of systems engineering. It is a relatively new development in systems engineering with the initial NIST (National Institute of Standards) standard published in November of 2016 with updates in 2018, and 2022. The guiding principles in our methodology are based in NIST Special Publication 800-160 Vol. 1 “Systems Security Engineering: Considerations For A Multidisciplinary Approach In The Engineering Of Trustworthy Secure Systems” and integrate methodologies from common IT (Information Technology) threat modeling approaches utilizing MBSE (Model-Based Systems Engineering). The presentation will discuss how our teams utilize SSE and MBSE (Model-Based Systems Engineering) to develop secure architectures for systems under development in our NASA aeronautics research environment. This includes the activities to develop Protection Needs (PN) that, in turn result in security requirements in the design context and policies for the future state operational context for system protection. The process of applying SSE to analyze project architectures and ConOps (Concept of Operations) is intended to ensure the transferred research is both secure and securable in a “real-world” setting.

Systems Security Engineering↗

DOE OSTI2025

Classical eikonal from Magnus expansion

In a classical scattering problem, the classical eikonal is defined as the generator of the canonical transformation that maps in-states to out-states. It can be regarded as the classical limit of the log of the quantum S-matrix. In a classical analog of the Born approximation in quantum mechanics, the classical eikonal admits an expansion in oriented tree graphs, where oriented edges denote retarded/advanced worldline propagators. The Magnus expansion, which takes the log of a time-ordered exponential integral, offers an efficient method to compute the coefficients of the tree graphs to all orders. We exploit a Hopf algebra structure behind the Magnus expansion to develop a fast algorithm which can compute the tree coefficients up to the 12th order (over half a million trees) in less than an hour. In a relativistic setting, our methods can be applied to the post-Minkowskian (PM) expansion for gravitational binaries in the worldline formalism. We demonstrate the methods by computing the 3PM eikonal and find agreement with previous results based on amplitude methods. Importantly, the Magnus expansion yields a finite eikonal, while the naïve eikonal based on the time-symmetric propagator is infrared-divergent from 3PM on.

Black Holes↗

NASA NTRS1995

Modeling of collision-induced infrared absorption spectra of H2 pairs in the first overtone band at temperatures from 20 to 500 K

A simple formalism is presented that permits quick computations of the low-resolution, rotovibrational collision-induced absorption (RV CIA) spectra of H2 pairs in the first overtone band of hydrogen, at temperatures from 20 to 500 K. These spectra account for the free-free transitions. The sharp dimer features, originating from the bound-free, free-bound, and bound-bound transitions are ignored, though their integrated intensities are properly accounted for. The method employs spectral model line- shapes with parameters computed from the three lowest spectral moments. The moments are obtained from first principles expressed as analytical functions of temperature. Except for the sharp dimer features, which are absent in this model, the computed spectra reproduce closely the results of exact quantum mechanical lineshape computations. Comparisons of the computed spectra with existing experimental data also show good agreement. The work interest for the modeling of the atmospheres of the outer planets in the near-infrared region of the spectrum. The user-friendly Fortran program developed here is available on request from the authors.

Zheng, Chunguang↗

NASA NTRS2004

Calculation of the Full Scattering Amplitude without Partial Wave Decomposition: Inclusion of Exchange - 2

The development of a practical method of accurately calculating the full scattering amplitude, without making a partial wave decomposition is continued. The method is developed in the context of electron-hydrogen scattering, and here exchange is dealt with by considering e-H scattering in the static exchange approximation. The Schroedinger equation in this approximation can be simplified to a set of coupled integro-differential equations. The equations are solved numerically for the full scattering wave function. The scattering amplitude can most accurately be calculated from an integral expression for the amplitude; that integral can be formally simplified, and then evaluated using the numerically determined wave function. The results are essentially identical to converged partial wave results.

Shertzer, Janine↗

NASA NTRS2004

A Survey of Formal Methods for Intelligent Swarms

Swarms of intelligent autonomous spacecraft, involving complex behaviors and interactions, are being proposed for future space exploration missions. Such missions provide greater flexibility and offer the possibility of gathering more science data than traditional single spacecraft missions. The emergent properties of swarms make these missions powerful, but simultaneously far more difficult to design, and to assure that the proper behaviors will emerge. These missions are also considerably more complex than previous types of missions, and NASA, like other organizations, has little experience in developing or in verifying and validating these types of missions. A significant challenge when verifying and validating swarms of intelligent interacting agents is how to determine that the possible exponential interactions and emergent behaviors are producing the desired results. Assuring correct behavior and interactions of swarms will be critical to mission success. The Autonomous Nano Technology Swarm (ANTS) mission is an example of one of the swarm types of missions NASA is considering. The ANTS mission will use a swarm of picospacecraft that will fly from Earth orbit to the Asteroid Belt. Using an insect colony analogy, ANTS will be composed of specialized workers for asteroid exploration. Exploration would consist of cataloguing the mass, density, morphology, and chemical composition of the asteroids, including any anomalous concentrations of specific minerals. To perform this task, ANTS would carry miniaturized instruments, such as imagers, spectrometers, and detectors. Since ANTS and other similar missions are going to consist of autonomous spacecraft that may be out of contact with the earth for extended periods of time, and have low bandwidths due to weight constraints, it will be difficult to observe improper behavior and to correct any errors after launch. Providing V&V (verification and validation) for this type of mission is new to NASA, and represents the cutting edge in system correctness, and requires higher levels of assurance than other (traditional) missions that use a single or small number of spacecraft that are deterministic in nature and have near continuous communication access. One of the highest possible levels of assurance comes from the application of formal methods. Formal methods are mathematics-based tools and techniques for specifying and verifying (software and hardware) systems. They are particularly useful for specifying complex parallel systems, such as exemplified by the ANTS mission, where the entire system is difficult for a single person to fully understand, a problem that is multiplied with multiple developers. Once written, a formal specification can be used to prove properties of a system (e.g., the underlying system will go from one state to another or not into a specific state) and check for particular types of errors (e.g., race or livelock conditions). A formal specification can also be used as input to a model checker for further validation. This report gives the results of a survey of formal methods techniques for verification and validation of space missions that use swarm technology. Multiple formal methods were evaluated to determine their effectiveness in modeling and assuring the behavior of swarms of spacecraft using the ANTS mission as an example system. This report is the first result of the project to determine formal approaches that are promising for formally specifying swarm-based systems. From this survey, the most promising approaches were selected and are discussed relative to their possible application to the ANTS mission. Future work will include the application of an integrated approach, based on the selected approaches identified in this report, to the formal specification of the ANTS mission.

Truszkowski, Walt↗

DOE OSTI2025

ARCS: Agentic Retrieval-Augmented Code Synthesis with Iterative Refinement

Agentic Retrieval-Augmented Code Synthesis with Iterative RefinementIn supercomputing, efficient and optimized code generation is essential to leverage high-performance systems effectively. We have developed Agentic Retrieval-Augmented Code Synthesis (ARCS), an advanced framework for accurate, robust, and efficient code generation, completion, and translation. ARCS integrates Retrieval-Augmented Generation (RAG) with Chain-of-Thought (CoT) reasoning to systematically break down and iteratively refine complex programming tasks. An agent-based RAG mechanism retrieves relevant code snippets, while real-time execution feedback drives the synthesis of candidate solutions. This process is formalized as a state-action search tree optimization, balancing code correctness with editing efficiency. Evaluations on the Geeks4Geeks and HumanEval benchmarks demonstrate that ARCS significantly outperforms traditional prompting methods in translation and generation quality. By enabling scalable and precise code synthesis, ARCS offers transformative potential for automating and optimizing code development in supercomputing applications, enhancing computational resource utilization

Bhattarai, Manish [Los Alamos National Labs]↗

DOE OSTI2024

Gravitational scattering and beyond from extreme mass ratio effective field theory

We explore a recently proposed effective field theory describing electromagnetically or gravitationally interacting massive particles in an expansion about their mass ratio, also known as the self-force (SF) expansion. By integrating out the deviation of the heavy particle about its inertial trajectory, we obtain an effective action whose only degrees of freedom are the lighter particle together with the photon or graviton, all propagating in a Coulomb or Schwarzschild background. The 0SF dynamics are described by the usual background field method, which at 1SF is supplemented by a “recoil operator” that encodes the wobble of the heavy particle, and similarly computable corrections appearing at 2SF and higher. Our formalism exploits the fact that the analytic expressions for classical backgrounds and particle trajectories encode dynamical information to all orders in the couplings, and from them we extract multiloop integrands for perturbative scattering. As a check, we study the two-loop classical scattering of scalar particles in electromagnetism and gravity, verifying known results. We then present new calculations for the two-loop classical scattering of dyons, and of particles interacting with an additional scalar or vector field coupling directly to the lighter particle but only gravitationally to the heavier particle.

72 PHYSICS OF ELEMENTARY PARTICLES AND FIELDS↗

NASA NTRS1995

DRS: Derivational Reasoning System

The high reliability requirements for airborne systems requires fault-tolerant architectures to address failures in the presence of physical faults, and the elimination of design flaws during the specification and validation phase of the design cycle. Although much progress has been made in developing methods to address physical faults, design flaws remain a serious problem. Formal methods provides a mathematical basis for removing design flaws from digital systems. DRS (Derivational Reasoning System) is a formal design tool based on advanced research in mathematical modeling and formal synthesis. The system implements a basic design algebra for synthesizing digital circuit descriptions from high level functional specifications. DRS incorporates an executable specification language, a set of correctness preserving transformations, verification interface, and a logic synthesis interface, making it a powerful tool for realizing hardware from abstract specifications. DRS integrates recent advances in transformational reasoning, automated theorem proving and high-level CAD synthesis systems in order to provide enhanced reliability in designs with reduced time and cost.

Bose, Bhaskar↗

NASA NTRS1983

Derivation of the fundamental equation of sound generated by moving aerodynamic surfaces

Ffowcs Williams and Hawkings (1969) based their derivation of the fundamental equation of the sound generated by arbitrarily moving aerodynamic surfaces on the study of mass and momentum balance of a control volume imbedding a mathematical surface(s) exactly corresponding to real surface(s). These investigators also sketched an alternative method, employing generalized functions, for its derivation. This latter method, which was later developed by Farassat (1975), is purely mathematical and formal. Goldstein (1976) used the free-space Green function to produce an implicit derivation of the Ffowcs Williams and Hawkings equation. In the study presented here, Lowson's (1965) concept of moving point singularities is generalized to moving surface singularities, and a new derivation is given of the fundamental equation. The derivation is based on topological considerations of the underlying space, the fluid medium, and the integral properties of the Dirac delta function.

Aggarwal, H. R.↗

NASA NTRS1970

The integration of system specifications and program coding

Experience in maintaining up-to-date documentation for one module of the large-scale Medical Literature Analysis and Retrieval System 2 (MEDLARS 2) is described. Several innovative techniques were explored in the development of this system's data management environment, particularly those that use PL/I as an automatic documenter. The PL/I data description section can provide automatic documentation by means of a master description of data elements that has long and highly meaningful mnemonic names and a formalized technique for the production of descriptive commentary. The techniques discussed are practical methods that employ the computer during system development in a manner that assists system implementation, provides interim documentation for customer review, and satisfies some of the deliverable documentation requirements.

Luebke, W. R.↗

NASA NTRS2011

Two-Point Turbulence Closure Applied to Variable Resolution Modeling

Variable resolution methods have become frontline CFD tools, but in order to take full advantage of this promising new technology, more formal theoretical development is desirable. Two general classes of variable resolution methods can be identified: hybrid or zonal methods in which RANS and LES models are solved in different flow regions, and bridging or seamless models which interpolate smoothly between RANS and LES. This paper considers the formulation of bridging methods using methods of two-point closure theory. The fundamental problem is to derive a subgrid two-equation model. We compare and reconcile two different approaches to this goal: the Partially Integrated Transport Model, and the Partially Averaged Navier-Stokes method.

Girimaji, Sharath S.↗