SEARCH · Engineering Papers

Results for “automated verification”

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 127 records · Page 7

All sources NASA NTRS DOE OSTI

NASA NTRS2013

Verification and Validation Studies for the LAVA CFD Solver

The verification and validation of the Launch Ascent and Vehicle Aerodynamics (LAVA) computational fluid dynamics (CFD) solver is presented. A modern strategy for verification and validation is described incorporating verification tests, validation benchmarks, continuous integration and version control methods for automated testing in a collaborative development environment. The purpose of the approach is to integrate the verification and validation process into the development of the solver and improve productivity. This paper uses the Method of Manufactured Solutions (MMS) for the verification of 2D Euler equations, 3D Navier-Stokes equations as well as turbulence models. A method for systematic refinement of unstructured grids is also presented. Verification using inviscid vortex propagation and flow over a flat plate is highlighted. Simulation results using laminar and turbulent flow past a NACA 0012 airfoil and ONERA M6 wing are validated against experimental and numerical data.

Validation↗

NASA NTRS2004

Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software

We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then processed by an automated first-order theorem prover (ATP). For full automation, however, the obligations must be aggressively preprocessed and simplified We describe the unique requirements this places on the ATP and demonstrate how the individual simplification stages, which are implemented by rewriting, influence the ability of the ATP to solve the proof tasks. Experiments on more than 25,000 tasks were carried out using Vampire, Spass, and e-setheo.

Denney, Ewen↗

NASA NTRS2004

An Empirical Evaluation of Automated Theorem Provers in Software Certification

We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then processed by an automated first-order theorem prover (ATP). We discuss the unique requirements this application places on the ATPs, focusing on automation, proof checking, and usability. For full automation, however, the obligations must be aggressively preprocessed and simplified, and we demonstrate how the individual simplification stages, which are implemented by rewriting, influence the ability of the ATPs to solve the proof tasks. Our results are based on 13 certification experiments that lead to more than 25,000 proof tasks which have each been attempted by Vampire, Spass, e-setheo, and Otter. The proofs found by Otter have been proof-checked by IVY.

Denney, Ewen↗

NASA NTRS2017

Land surface Verification Toolkit (LVT)

LVT is a framework developed to provide an automated, consolidated environment for systematic land surface model evaluation Includes support for a range of in-situ, remote-sensing and other model and reanalysis products. Supports the analysis of outputs from various LIS subsystems, including LIS-DA, LIS-OPT, LIS-UE. Note: The Land Information System Verification Toolkit (LVT) is a NASA software tool designed to enable the evaluation, analysis and comparison of outputs generated by the Land Information System (LIS). The LVT software is released under the terms and conditions of the NASA Open Source Agreement (NOSA) Version 1.1 or later. Land Information System Verification Toolkit (LVT) NOSA.

surface model↗

NASA NTRS1989

A verification library for multibody simulation software

A multibody dynamics verification library, that maintains and manages test and validation data is proposed, based on RRC Robot arm and CASE backhoe validation and a comparitive study of DADS, DISCOS, and CONTOPS that are existing public domain and commercial multibody dynamic simulation programs. Using simple representative problems, simulation results from each program are cross checked, and the validation results are presented. Functionalities of the verification library are defined, in order to automate validation procedure.

Kim, Sung-Soo↗

NASA NTRS1992

The Automated Logistics Element Planning System (ALEPS)

ALEPS, which is being developed to provide the SSF program with a computer system to automate logistics resupply/return cargo load planning and verification, is presented. ALEPS will make it possible to simultaneously optimize both the resupply flight load plan and the return flight reload plan for any of the logistics carriers. In the verification mode ALEPS will support the carrier's flight readiness reviews and control proper execution of the approved plans. It will also support the SSF inventory management system by providing electronic block updates to the inventory database on the cargo arriving at or departing the station aboard a logistics carrier. A prototype drawer packing algorithm is described which is capable of generating solutions for 3D packing of cargo items into a logistics carrier storage accommodation. It is concluded that ALEPS will provide the capability to generate and modify optimized loading plans for the logistics elements fleet.

Schwaab, Douglas G.↗

NASA NTRS1994

The Stanford how things work project

We provide an overview of the Stanford How Things Work (HTW) project, an ongoing integrated collection of research activities in the Knowledge Systems Laboratory at Stanford University. The project is developing technology for representing knowledge about engineered devices in a form that enables the knowledge to be used in multiple systems for multiple reasoning tasks and reasoning methods that enable the represented knowledge to be effectively applied to the performance of the core engineering task of simulating and analyzing device behavior. The central new capabilities currently being developed in the project are automated assistance with model formulation and with verification that a design for an electro-mechanical device satisfies its functional specification.

Fikes, Richard↗

NASA NTRS2018

High Accuracy Coronagraph Flight Model For WFIRST–CGI Raw Contrast Sensitivity Analysis

A high-accuracy high-fidelity flight wavefront control (WFC) model is developed for detailed raw contrast sensitivity analysis of WFIRST-CGI. Built upon features of recently testbed validated model, it is further refined to combine a full Fresnel propagation diffraction model for high accuracy contrast truth evaluation, and an economical compact model for WFC purposes. Extensive individual raw contrast error sensitivities are evaluated systematically, both as known imperfections and as unknown calibration errors, for both spectroscopy mode and wide field-of-view mode with shaped pupil coronagraph. More than 90 distinct error items were identified, including system aberrations, optical misalignment, component manufacturing error, telescope interface related errors, etc. The result forms the basis for raw contrast error budget flow down to a sub-system level, where detailed specifications needed to aid in component design and manufacturing, mechanical alignment and instrument integration, and verification and validation operations. Evaluations are mostly automated, making it relatively easy for repeat runs of revised design or at new desired error quantity. Top error sensitivities and contrast floor contributors are discussed and several observations are noted.

Poberezhskiy, Ilya↗

NASA NTRS2022

Integrating FRET with Copilot: Automated Translation of Natural Language Requirements to Runtime Monitors

Runtime verification (RV) enables monitoring systems at runtime, to detect property violations early and limit their potential consequences. To provide the level of assurance required for ultra-critical systems, monitor specifications must faithfully reflect the original mission requirements, which are often written in ambiguous natural language. This paper presents an end-to-end framework to capture requirements in structured natural language and generate monitors that capture their semantics faithfully. We leverage NASA’s Formal Requirement Elicitation Tool (FRET), and the RV system Copilot. We extend FRET with mechanisms to capture additional information needed to generate monitors, and introduce OGMA, a new tool to bridge the gap between FRET and Copilot. With this framework, users can write requirements in an intuitive format and obtain real-time C monitors suitable for use in embedded systems. Our tool chain is available as open source.

FRET↗

NASA NTRSDate not supplied

Feature-Guided Analysis of Neural Networks

Applying standard software engineering practices to neural networks is challenging due to the lack of high-level abstractions describing a neural network’s behavior. To address this challenge, we propose to extract high-level task-specific features from the neural network internal representation, based on monitoring the neural network activations.The extracted feature representations can serve as a link to high-level requirements and can be leveraged to enable fundamental software engineering activities, such as automated testing, debugging, requirements analysis, and formal verification, leading to better engineering of neural networks. Using two case studies, we present initial empirical evidence demonstrating the feasibility of our ideas.

Features↗

NASA NTRS2004

Assume-Guarantee Verification of Source Code with Design-Level Assumptions

Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. To address the 'state explosion' problem associated with this technique, we propose to integrate assume-guarantee verification at different phases of system development. During design, developers build abstract behavioral models of the system components and use them to establish key properties of the system. To increase the scalability of model checking at this level, we have developed techniques that automatically decompose the verification task by generating component assumptions for the properties to hold. The design-level artifacts are subsequently used to guide the implementation of the system, but also to enable more efficient reasoning at the source code-level. In particular we propose to use design-level assumptions to similarly decompose the verification of the actual system implementation. We demonstrate our approach on a significant NASA application, where design-level models were used to identify; and correct a safety property violation, and design-level assumptions allowed us to check successfully that the property was presented by the implementation.

Giannakopoulou, Dimitra↗

NASA NTRS1993

Mission Operations and Command Assurance: Automating an Operations TQM Task

A long-term program is in progress at JPL to reduce cost and risk of mission operations through defect prevention and error management. A major element of this program, Mission Operations and Command Assurance (MO&QA), provides a system level function on flight projects to instill quality in mission operations. MO&CA embodies the Total Quality Management (TQM) principle of Continuous Process Inprovement (CPI) and uses CPI in applying automation to mission operations to reduce risk and costs. MO&CA has led efforts to apply and has implemented automation in areas that impact the daily flight project environment including Incident Surprise Anomoly tracking and reporting; command data verification, tracking, and reporting; and command support data usage. MO&CA's future work in automation will take into account that future missions systems must be designed to avoid increasing error through the introduction of automation, while adapting to the demands of smaller flight teams.

automation↗

NASA NTRS2017

Program to Optimize Simulated Trajectories II (POST2) Surrogate Models for Mars Ascent Vehicle (MAV) Performance Assessment

The primary purpose of the multiPOST tool is to enable the execution of much larger sets of vehicle cases to allow for broader trade space exploration. However, this exploration is not achieved solely with the increased case throughput. The multiPOST tool is applied to carry out a Design of Experiments (DOE), which is a set of cases that have been structured to capture a maximum amount of information about the design space with minimal computational effort. The results of the DOE are then used to fit a surrogate model, ultimately enabling parametric design space exploration. The approach used for the MAV study includes both DOE and surrogate modeling. First, the primary design considerations for the vehicle were used to develop the variables and ranges for the multiPOST DOE. The final set of DOE variables were carefully selected in order to capture the desired vehicle trades and take into account any special considerations for surrogate modeling. Next, the DOE sets were executed through multiPOST. Following successful completion of the DOE cases, a manual verification trial was performed. The trial involved randomly selecting cases from the DOE set and running them by hand. The results from the human analyst's run and multiPOST were then compared to ensure that the automated runs were being executed properly. Completion of the verification trials was then followed by surrogate model fitting. After fits to the multiPOST data were successfully created, the surrogate models were used as a stand-in for POST2 to carry out the desired MAV trades. Using the surrogate models in lieu of POST2 allowed for visualization of vehicle sensitivities to the input variables as well as rapid evaluation of vehicle performance. Although the models introduce some error into the output of the trade study, they were very effective at identifying areas of interest within the trade space for further refinement by human analysts. The next section will cover all of the ground rules and assumptions associated with DOE setup and multiPOST execution. Section 3.1 gives the final DOE variables and ranges, while section 3.2 addresses the POST2 specific assumptions. The results of the verification trials are given in section 4. Section 5 gives the surrogate model fitting results, including the goodness-of-fit metrics for each fit. Finally, the MAV specific results are discussed in section 6.

Zwack, M. R.↗

NASA NTRS1991

Application of software technology to automatic test data analysis

The verification process for a major software subsystem was partially automated as part of a feasibility demonstration. The methods employed are generally useful and applicable to other types of subsystems. The effort resulted in substantial savings in test engineer analysis time and offers a method for inclusion of automatic verification as a part of regression testing.

Stagner, J. R.↗

NASA NTRS2003

Simulation-Based Verification of Livingstone Applications

AI software is viewed as a means to give greater autonomy to automated systems, capable of coping with harsh and unpredictable environments in deep space missions. Autonomous systems pose a serious challenge to traditional test-based verification approaches, because of the enormous space of possible situations that they aim to address. Before these systems are put in control of critical applications, appropriate new verification approaches need to be developed. This article describes Livingstone PathFinder (LPF), a verification tool for autonomous diagnosis applications based on NASA's Livingstone model-based diagnosis system. LPF applies state space exploration algorithms to an instrumented testbed, consisting of the Livingstone diagnosis system embedded in a simulated operating environment. The article describes different facets of LPF and reports some experimental results from applying LPF to a Livingstone model of the main propulsion feed subsystem of the X-34 space vehicle. This paper describes Livingstone PathFinder (LPF), a verification tool for autonomous diagnosis applications based on NASA's Livingstone model-based diagnosis system. LPF applies state space exploration algorithms to an instrumented testbed, consisting of the Livingstone diagnosis system embedded in a simulated operating environment. Section 2 provides an overview of Livingstone; Section 3 describes the LPF architecture; Section 4 discusses its applicability; Section 5 reviews some experimental results; Section 6 compares LPF to related verification approaches; Section 7 draws conclusions and discusses some perspectives.

Lindsey, Anthony E.↗

NASA NTRS2002

Program Model Checking as a New Trend

This paper introduces a special section of STTT (International Journal on Software Tools for Technology Transfer) containing a selection of papers that were presented at the 7th International SPIN workshop, Stanford, August 30 - September 1, 2000. The workshop was named SPIN Model Checking and Software Verification, with an emphasis on model checking of programs. The paper outlines the motivation for stressing software verification, rather than only design and model verification, by presenting the work done in the Automated Software Engineering group at NASA Ames Research Center within the last 5 years. This includes work in software model checking, testing like technologies and static analysis.

Havelund, Klaus↗

NASA NTRS2012

Optimized Temporal Monitors for SystemC

SystemC is a modeling language built as an extension of C++. Its growing popularity and the increasing complexity of designs have motivated research efforts aimed at the verification of SystemC models using assertion-based verification (ABV), where the designer asserts properties that capture the design intent in a formal language such as PSL or SVA. The model then can be verified against the properties using runtime or formal verification techniques. In this paper we focus on automated generation of runtime monitors from temporal properties. Our focus is on minimizing runtime overhead, rather than monitor size or monitor-generation time. We identify four issues in monitor generation: state minimization, alphabet representation, alphabet minimization, and monitor encoding. We conduct extensive experimentation and identify a combination of settings that offers the best performance in terms of runtime overhead.

Tabakov, Deian↗

NASA NTRS2013

The DEEP2 Galaxy Redshift Survey: Design, Observations, Data Reduction, and Redshifts

We describe the design and data analysis of the DEEP2 Galaxy Redshift Survey, the densest and largest high-precision redshift survey of galaxies at z approx. 1 completed to date. The survey was designed to conduct a comprehensive census of massive galaxies, their properties, environments, and large-scale structure down to absolute magnitude MB = −20 at z approx. 1 via approx.90 nights of observation on the Keck telescope. The survey covers an area of 2.8 Sq. deg divided into four separate fields observed to a limiting apparent magnitude of R(sub AB) = 24.1. Objects with z approx. < 0.7 are readily identifiable using BRI photometry and rejected in three of the four DEEP2 fields, allowing galaxies with z > 0.7 to be targeted approx. 2.5 times more efficiently than in a purely magnitude-limited sample. Approximately 60% of eligible targets are chosen for spectroscopy, yielding nearly 53,000 spectra and more than 38,000 reliable redshift measurements. Most of the targets that fail to yield secure redshifts are blue objects that lie beyond z approx. 1.45, where the [O ii] 3727 Ang. doublet lies in the infrared. The DEIMOS 1200 line mm(exp −1) grating used for the survey delivers high spectral resolution (R approx. 6000), accurate and secure redshifts, and unique internal kinematic information. Extensive ancillary data are available in the DEEP2 fields, particularly in the Extended Groth Strip, which has evolved into one of the richest multiwavelength regions on the sky. This paper is intended as a handbook for users of the DEEP2 Data Release 4, which includes all DEEP2 spectra and redshifts, as well as for the DEEP2 DEIMOS data reduction pipelines. Extensive details are provided on object selection, mask design, biases in target selection and redshift measurements, the spec2d two-dimensional data-reduction pipeline, the spec1d automated redshift pipeline, and the zspec visual redshift verification process, along with examples of instrumental signatures or other artifacts that in some cases remain after data reduction. Redshift errors and catastrophic failure rates are assessed through more than 2000 objects with duplicate observations. Sky subtraction is essentially photon-limited even under bright OH sky lines; we describe the strategies that permitted this, based on high image stability, accurate wavelength solutions, and powerful B-spline modeling methods. We also investigate the impact of targets that appear to be single objects in ground-based targeting imaging but prove to be composite in Hubble Space Telescope data; they constitute several percent of targets at z approx. 1, approaching approx. 5%-10% at z > 1.5. Summary data are given that demonstrate the superiority of DEEP2 over other deep high-precision redshift surveys at z approx. 1 in terms of redshift accuracy, sample number density, and amount of spectral information. We also provide an overview of the scientific highlights of the DEEP2 survey thus far.

Galaxy↗