Engineering Papers⌕ Search

SEARCH · Engineering Papers

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

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

At least 613 records · Page 34
All sourcesNASA NTRSDOE OSTI
NASA NTRS1993

Formalizing structured file services for the data storage and retrieval subsystem of the data management system for Spacestation Freedom

A brief example of the use of formal methods techniques in the specification of a software system is presented. The report is part of a larger effort targeted at defining a formal methods pilot project for NASA. One possible application domain that may be used to demonstrate the effective use of formal methods techniques within the NASA environment is presented. It is not intended to provide a tutorial on either formal methods techniques or the application being addressed. It should, however, provide an indication that the application being considered is suitable for a formal methods by showing how such a task may be started. The particular system being addressed is the Structured File Services (SFS), which is a part of the Data Storage and Retrieval Subsystem (DSAR), which in turn is part of the Data Management System (DMS) onboard Spacestation Freedom. This is a software system that is currently under development for NASA. An informal mathematical development is presented. Section 3 contains the same development using Penelope (23), an Ada specification and verification system. The complete text of the English version Software Requirements Specification (SRS) is reproduced in Appendix A.

Jamsek, Damir A.↗
NASA NTRS1991

Rule groupings: An approach towards verification of expert systems

Knowledge-based expert systems are playing an increasingly important role in NASA space and aircraft systems. However, many of NASA's software applications are life- or mission-critical and knowledge-based systems do not lend themselves to the traditional verification and validation techniques for highly reliable software. Rule-based systems lack the control abstractions found in procedural languages. Hence, it is difficult to verify or maintain such systems. Our goal is to automatically structure a rule-based system into a set of rule-groups having a well-defined interface to other rule-groups. Once a rule base is decomposed into such 'firewalled' units, studying the interactions between rules would become more tractable. Verification-aid tools can then be developed to test the behavior of each such rule-group. Furthermore, the interactions between rule-groups can be studied in a manner similar to integration testing. Such efforts will go a long way towards increasing our confidence in the expert-system software. Our research efforts address the feasibility of automating the identification of rule groups, in order to decompose the rule base into a number of meaningful units.

Mehrotra, Mala↗
DOE OSTI2025

An Open-Source Python Package for CFD Solution Verification

Informed decision-making using computational fluid dynamics (CFD) results requires quantifying the errors and uncertainties of a simulation. Verification, validation, and uncertainty quantification (VVUQ) methods were developed to address this need and have matured. However, these VVUQ analyses are often non-trivial and require CFD analysts and practitioners to have specific skill sets. This has led to the uneven adoption of VVUQ analyses, in part, based on the availability of software tools to aid CFD analysts and practitioners. Solution verification, a procedure to evaluate the accuracy of a simulation by estimating potential errors arising from the computational model and computing the uncertainties without comparing to results from a physical system, is one of the lagging VVUQ analyses as the absence of software has forced CFD analysts and practitioners to develop their own codes or piece together incomplete software from across the internet. This work presents an opensource Python package, CFDverify, to lower the barrier of entry and fill in the technological gap in solution verification. CFDverify also provides a streamlined framework to remove some potential errors in post-processing CFD results. The hope is that CFDverify can improve the quality and quantity of CFD solution verification in scientific and research studies and attract interest in developing a communal tool. This paper describes the design, features, and an example use of CFDverify.

Weinmeister, Justin [ORNL] (ORCID:0000000160090237↗
NASA NTRS2020

IV&V Assurance Case Design for Artemis II

As human-rated missions like those in NASA’s Artemis program continue to grow in both size and complexity, and the role of software in achieving mission objectives expands dramatically, NASA’s Independent Verification and Validation (IV&V) Teams face evolving challenges in assuring the safety and performance of the safety- and mission-critical embedded software that is essential to landing astronauts on the surface of the Moon by 2024. Key among these challenges is IV&V’s desire to present a cohesive, integrated assurance statement to its stakeholders that encapsulates and summarizes our assurance positions across the integrated Artemis systems and their combined role in support of a safe and successful flight. In order to meet this challenge, the IV&V Teams have begun a transition to using formal assurance case concepts and documentation in the Goal Structuring Notation (GSN) to build an argument in support of software assurance. IV&V recognizes significant benefits to the logical argumentation structure provided by assurance cases and GSN over our current practices for documenting and managing assurance claims. In order to reap these benefits, IV&V is integrating the use of assurance case concepts with our paradigm of follow-the-risk capability based assurance. Because of this, assurance cases created and used by IV&V are distinct from the sort of assurance case created by a development project or embedded software assurance organization. IV&V’s assurance cases depend much less upon standards and regulations, and more on evidence captured by IV&V regarding the environment, requirements, design, and implementation. IV&V constructs an independent network of claims based on an independent decomposition of arguments. Based upon the risk posture of these claims and their associated software and software artifacts, IV&V then develops and executes engineering analyses and testing, which provide evidence to either support or refute the claim. This emerging risk-informed assurance case methodology is being put into practice as IV&V plans for support of the Artemis II mission, the first flight of the Orion capsule and Space Launch System with astronauts on board.

Gerek Whitman↗
NASA NTRS2020

IV&V Assurance Case Design for Artemis II

As human-rated missions like those in NASA's Artemis program continue to grow in both size and complexity, and the role of software in achieving mission objectives expands dramatically, NASA's Independent Verification and Validation (IV&V) Teams face evolving challenges in assuring the safety and performance of the safety- and mission-critical embedded software that is essential to landing astronauts on the surface of the Moon by 2024. Key among these challenges is IV&V's desire to present a cohesive, integrated assurance statement to its stakeholders that encapsulates and summarizes our assurance positions across the integrated Artemis systems and their combined role in support of a safe and successful flight. In order to meet this challenge, the IV&V Teams have begun a transition to using formal assurance case concepts and documentation in the Goal Structuring Notation (GSN) to build an argument in support of software assurance. IV&V recognizes significant benefits to the logical argumentation structure provided by assurance cases and GSN over our current practices for documenting and managing assurance claims. In order to reap these benefits, IV&V is integrating the use of assurance case concepts with our paradigm of follow-the-risk capability based assurance. Because of this, assurance cases created and used by IV&V are distinct from the sort of assurance case created by a development project or embedded software assurance organization. IV&V's assurance cases depend much less upon standards and regulations, and more on evidence captured by IV&V regarding the environment, requirements, design, and implementation. IV&V constructs an independent network of claims based on an independent decomposition of arguments. Based upon the risk posture of these claims and their associated software and software artifacts, IV&V then develops and executes engineering analyses and testing, which provide evidence to either support or refute the claim. This emerging risk-informed assurance case methodology is being put into practice as IV&V plans for support of the Artemis II mission, the first flight of the Orion capsule and Space Launch System with astronauts on board.

Whitman, Gerek↗
DOE OSTI2014

SU-E-CAMPUS-T-06: Initial Experience of Patient-Specific QA Using a Pencil Beam Scanning Proton Therapy System

Purpose: To illustrate patient QA results for the first 10 patients treated at Scripps Proton Center by comparing point dose measurement using an ion chamber and in-house developed secondary MU program, and the measurement of 2D dose distribution using an ion chamber array. Methods: At the time of writing, 10 patient plans were approved for treatment using Varian ProBeam pencil beam scanning system and Eclipse treatment planning software. We used the IBA CC04 0.04 cm3 ion chamber and PTW Unidos E electrometer for point dose measurement in a small water tank (Sun Nuclear 1D scanner). We developed independent MU check software based on measured pencil beam dose profiles for various energies. We used PTW Octavius 729 XDR array to evaluate 2D planar dose distribution. The 3D gamma at 3%/3 mm local dose was used to compare a 3D calculated dose plan with a 2D measured dose distribution using PTW Verisoft software. All fields were exported to a verification phantom plan and delivered at 0 degrees for simplicity. Results: Comparisons between the CC04 ion chamber measurement and calculated dose agree well within 1%. The PTW Octavius 729 XDR array exhibited some dose rate dependence in high dose rate pencil beam delivery. Nevertheless, the results, used as a relative measurement, passed the gamma criteria of 3%/3mm for greater than 90% of area in all patient fields. Visual inspection showed good agreement between ion chamber dose profile and the calculated plan. The in-house secondary check for MU agreed very well with the plan dose and measurement. The results will be updated with more patients treated. Conclusion: The initial patient specific QA results are encouraging for a new pencil beam scanning only proton therapy system.

60 APPLIED LIFE SCIENCES↗
DOE OSTI2025

ACTIVE

The Automated Control Testbed for Integration, Verification, and Emulation (ACTIVE) framework is a software platform designed to support the optimized operation and management of a wide range of building types. It enables the development, testing, and validation of diverse control strategies, including AI-based, rule-based, and model-based approaches. The platform facilitates a seamless transition from simulation-based evaluation of control strategies to real-world field validation and deployment. ACTIVE supports the full building management lifecycle, encompassing data acquisition and management, system monitoring, optimized control, adaptive learning services, device dispatch and coordination, as well as advanced analytics and visualization. Together, these capabilities provide an integrated environment for improving building performance, operational efficiency, reducing energy cost, and reliability.

Smith, Robert [Oak Ridge National Laboratory (ORNL↗
DOE OSTI2020

Resistive heating in an electrified domain with a spherical inclusion: an ALEGRA verification study

A verification study is conducted for the ALEGRA software, using the problem of an electrified medium with a spherical inclusion, paying special attention to resistive heating. We do so by extending an existing analytic solution for this problem to include both conducting and insulating inclusions, and we examine the effects of mesh resolution and mesh topology, considering both body-fitted and rectangular meshes containing mixed cells. We present observed rates of convergence with respect to mesh refinement for four electromagnetic quantities: electric potential, electric field, current density and Joule power.

97 MATHEMATICS AND COMPUTING↗
DOE OSTI2023

Correct Compilation of Concurrent C Code

The CompCert compiler represents a landmark effort in program verification as both a piece of verified software and as a compiler for verified C programs. A key shortcoming of CompCert however is that it does not support multithreaded programs. Prior work to add threads to CompCert has either required major rewrites of parts of the proof or only works for well synchronized programs. The problem is that CompCert’s backward simulation derives from a forward simulation via the determinism of the semantics of intermediate representation languages. This makes the proofs in CompCert easier but also makes them incompatible with standard models of multithreading which are non-deterministic. Here we propose an alternate formulation of CompCert’s proof structure that parameterizes the existing single threaded semantics with nondeterministic behavior generated at the multithreading level. While this is an old trick where program equivalence is concerned, performing it in the context of CompCert is quite subtle. Our approach allows for expressive concurrent semantics and does not require major proof rewrites but still results in a global backward simulation for multithreaded programs.

97 MATHEMATICS AND COMPUTING↗
NASA NTRS1973

Design of a modular digital computer system DRL 4 and 5

Design and development efforts for a spaceborne modular computer system are reported. An initial baseline description is followed by an interface design that includes definition of the overall system response to all classes of failure. Final versions for the register level designs for all module types were completed. Packaging, support and control executive software, including memory utilization estimates and design verification plan, were formalized to insure a soundly integrated design of the digital computer system.

Source record↗
NASA NTRS1983

A system for intelligent teleoperation research

The Automation Technology Branch of NASA Langley Research Center is developing a research capability in the field of artificial intelligence, particularly as applicable in teleoperator/robotics development for remote space operations. As a testbed for experimentation in these areas, a system concept has been developed and is being implemented. This system termed DAISIE (Distributed Artificially Intelligent System for Interacting with the Environment), interfaces the key processes of perception, reasoning, and manipulation by linking hardware sensors and manipulators to a modular artificial intelligence (AI) software system in a hierarchical control structure. Verification experiments have been performed: one experiment used a blocksworld database and planner embedded in the DAISIE system to intelligently manipulate a simple physical environment; the other experiment implemented a joint-space collision avoidance algorithm. Continued system development is planned.

Orlando, N. E.↗
NASA NTRS1985

Space station data system analysis/architecture study. Task 2: Options development, DR-5. Volume 3: Programmatic options

Task 2 in the Space Station Data System (SSDS) Analysis/Architecture Study is the development of an information base that will support the conduct of trade studies and provide sufficient data to make design/programmatic decisions. This volume identifies the preferred options in the programmatic category and characterizes these options with respect to performance attributes, constraints, costs, and risks. The programmatic category includes methods used to administrate/manage the development, operation and maintenance of the SSDS. The specific areas discussed include standardization/commonality; systems management; and systems development, including hardware procurement, software development and system integration, test and verification.

Source record↗
NASA NTRS1987

Space station definition and preliminary design, WP-01. Volume 1: Executive summary

System activities are summarized and an overview of the system level engineering tasks performed are provided. Areas discussed include requirements, system test and verification, the advanced development plan, customer accommodations, software, growth, productivity, operations, product assurance and metrication. The hardware element study results are summarized. Overviews of recommended configurations are provided for the core module, the USL, the logistics elements, the propulsion subsystems, reboost, vehicle accommodations, and the smart front end. A brief overview is provided for costing activities.

Lenda, J. A.↗
NASA NTRS1987

KBS V and V as related to automation of space station subsystems: Rationale for a KBS lifecycle

The role of verification and validation (V and V) in software has been to support and strengthen the software lifecycle and to ensure that the resultant code meets the standards of the requirements document. Knowledge based systems (KBS) V and V should serve the same role, but the KBS lifecycle is ill-defined. Here, the rationale of the simple form of the KBS lifecycle is explained. Special KBS development requirements are accommodated where possible by modifications to the traditional software lifecycle. Research areas are suggested for those aspects which present new or unusual difficulties for V and V.

Richardson, K.↗
NASA NTRS1988

Knowledge based system verification and validation as related to automation of space station subsystems: Rationale for a knowledge based system lifecycle

The role of verification and validation (V and V) in software has been to support and strengthen the software lifecycle and to ensure that the resultant code meets the standards of the requirements documents. Knowledge Based System (KBS) V and V should serve the same role, but the KBS lifecycle is ill-defined. The rationale of a simple form of the KBS lifecycle is presented, including accommodation to certain critical KBS differences from software development.

Richardson, Keith↗
NASA NTRS1988

Knowledge based system verification and validation as related to automation of Space Station subsystems - Rationale for a knowledge based system lifecycle

The role of verification and validation (V and V) in software has been to support and strengthen the software lifecycle and to ensure that the resultant code meets the standards of the requirements documents. Knowledge-based system (KBS) V and V should serve the same role, but the KBS lifecycle is ill-defined. The rationale of a simple form of the KBS lifecycle is presented, including accommodation to certain critical KBS differences from software development.

Richardson, Keith↗
NASA NTRS1995

A highly reliable, high performance open avionics architecture for real time Nap-of-the-Earth operations

An Army Fault Tolerant Architecture (AFTA) has been developed to meet real-time fault tolerant processing requirements of future Army applications. AFTA is the enabling technology that will allow the Army to configure existing processors and other hardware to provide high throughput and ultrahigh reliability necessary for TF/TA/NOE flight control and other advanced Army applications. A comprehensive conceptual study of AFTA has been completed that addresses a wide range of issues including requirements, architecture, hardware, software, testability, producibility, analytical models, validation and verification, common mode faults, VHDL, and a fault tolerant data bus. A Brassboard AFTA for demonstration and validation has been fabricated, and two operating systems and a flight-critical Army application have been ported to it. Detailed performance measurements have been made of fault tolerance and operating system overheads while AFTA was executing the flight application in the presence of faults.

Harper, Richard E.↗