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 91 records · Page 5

Automatic Generation of Guard-Stable Floating-Point Code

In floating-point programs, test instability occurs when the control flow of a conditional statement diverges from its ideal execution under real arithmetic. This phenomenon is caused by the presence of round-off errors in floating-point computations. Writing programs that correctly handle test instability often require expertise on finite precision computations and rounding errors. This paper presents a fully automatic tool chain that generates and formally verifies a test-stable floating-point C program from its functional specification in real arithmetic. The generated program is instrumented to soundly detect when unstable tests may occur and, in these cases, to issue a warning. The proposed approach combines the PRECiSA floating-point static analyzer, the Frama-C software verification suite, and the PVS theorem prover.

Floating-Point Arithmetic↗

Case Study: Test Results of a Tool and Method for In-Flight, Adaptive Control System Verification on a NASA F-15 Flight Research Aircraft

Adaptive control technologies that incorporate learning algorithms have been proposed to enable autonomous flight control and to maintain vehicle performance in the face of unknown, changing, or poorly defined operating environments [1-2]. At the present time, however, it is unknown how adaptive algorithms can be routinely verified, validated, and certified for use in safety-critical applications. Rigorous methods for adaptive software verification end validation must be developed to ensure that. the control software functions as required and is highly safe and reliable. A large gap appears to exist between the point at which control system designers feel the verification process is complete, and when FAA certification officials agree it is complete. Certification of adaptive flight control software verification is complicated by the use of learning algorithms (e.g., neural networks) and degrees of system non-determinism. Of course, analytical efforts must be made in the verification process to place guarantees on learning algorithm stability, rate of convergence, and convergence accuracy. However, to satisfy FAA certification requirements, it must be demonstrated that the adaptive flight control system is also able to fail and still allow the aircraft to be flown safely or to land, while at the same time providing a means of crew notification of the (impending) failure. It was for this purpose that the NASA Ames Confidence Tool was developed [3]. This paper presents the Confidence Tool as a means of providing in-flight software assurance monitoring of an adaptive flight control system. The paper will present the data obtained from flight testing the tool on a specially modified F-15 aircraft designed to simulate loss of flight control faces.

Jacklin, Stephen A.↗

RAPIDS2: A SciDAC Institute for Computer Science, Data, and Artificial Intelligence (University of Delaware)

This report summarizes the activities, technical accomplishments, and outcomes of the RAPIDS2 Institute project at the University of Delaware (UD). The RAPIDS2 Institute was a large multi-institution project with the objective of assisting SciDAC and Office of Science application teams in the use of DOE supercomputing resources to achieve scientific breakthroughs. The UD team contributed to this effort through work on formal software verification. This thrust aims to reduce software developer time and effort, especially regarding debugging and testing, and to increase confidence in the correctness of the results computed by the software.

97 MATHEMATICS AND COMPUTING↗

Formal verification of AI software

The application of formal verification techniques to Artificial Intelligence (AI) software, particularly expert systems, is investigated. Constraint satisfaction and model inversion are identified as two formal specification paradigms for different classes of expert systems. A formal definition of consistency is developed, and the notion of approximate semantics is introduced. Examples are given of how these ideas can be applied in both declarative and imperative forms.

Rushby, John↗

Evaluation of verification and testing tools for FORTRAN programs

Two automated software verification and testing systems were developed for use in the analysis of computer programs. An evaluation of the static analyzer DAVE and the dynamic analyzer PET, which are used in the analysis of FORTRAN programs on Control Data (CDC) computers, are described. Both systems were found to be effective and complementary, and are recommended for use in testing FORTRAN programs.

Smith, K. A.↗

Space station software reliability analysis based on failures observed during testing at the multisystem integration facility

Quality of software not only is vital to the successful operation of the space station, it is also an important factor in establishing testing requirements, time needed for software verification and integration as well as launching schedules for the space station. Defense of management decisions can be greatly strengthened by combining engineering judgments with statistical analysis. Unlike hardware, software has the characteristics of no wearout and costly redundancies, thus making traditional statistical analysis not suitable in evaluating reliability of software. A statistical model was developed to provide a representation of the number as well as types of failures occur during software testing and verification. From this model, quantitative measure of software reliability based on failure history during testing are derived. Criteria to terminate testing based on reliability objectives and methods to estimate the expected number of fixings required are also presented.

Tamayo, Tak Chai↗

Design and flight experience with a digital fly-by-wire control system in an F-8 airplane

A digital fly-by-wire flight control system was designed, built, and for the first time flown in an airplane. The system, which uses components from the Apollo guidance system, is installed in an F-8 airplane as the primary control system. A lunar module guidance computer is the central element in the three-axis, single-channel, multimode, digital control system. A triplex electrical analog system which provides unaugmented control of the airplane is the only backup to the digital system. Flight results showed highly successful system operation, although the trim update rate was inadequate for precise trim changes, causing minor concern. The use of a digital system to implement conventional control laws proved to be practical for flight. Logic functions coded as an integral part of the control laws were found to be advantageous. Although software verification required extensive effort, confidence in the software was achieved.

Deets, D. A.↗

RELAP5-3D Resolution of Known Restart/Backup Issues

The state-of-the-art nuclear reactor system safety analysis computer program developed at the Idaho National Laboratory (INL), RELAP5-3D, continues to adapt to changes in computer hardware and software and to develop to meet the ever-expanding needs of the nuclear industry. To continue at the forefront, code testing must evolve with both code and industry developments, and it must work correctly. To best ensure this, the processes of Software Verification and Validation (V&V) are applied. Verification compares coding against its documented algorithms and equations and compares its calculations against analytical solutions and the method of manufactured solutions. A form of this, sequential verification, checks code specifications against coding only when originally written then applies regression testing which compares code calculations between consecutive updates or versions on a set of test cases to check that the performance does not change. A sequential verification testing system was specially constructed for RELAP5-3D to both detect errors with extreme accuracy and cover all nuclear-plant-relevant code features. Detection is provided through a “verification file” that records double precision sums of key variables. Coverage is provided by a test suite of input decks that exercise code features and capabilities necessary to model a nuclear power plant. A matrix of test features and short-running cases that exercise them is presented. This testing system is used to test base cases (called null testing) as well as restart and backup cases. It can test RELAP5-3D performance in both standalone and coupled (through PVM to other codes) runs. Application of verification testing revealed numerous restart and backup issues in both standalone and couple modes. This document reports the resolution of these issues.

22 GENERAL STUDIES OF NUCLEAR REACTORS↗

A Framework for Performing Verification and Validation in Reuse Based Software Engineering

Verification and Validation (V&V) is currently performed during application development for many systems, especially safety-critical and mission- critical systems. The V&V process is intended to discover errors, especially errors related to critical processing, as early as possible during the development process. The system application provides the context under which the software artifacts are validated. This paper describes a framework that extends V&V from an individual application system to a product line of systems that are developed within an architecture-based software engineering environment. This framework includes the activities of traditional application-level V&V, and extends these activities into domain engineering and into the transition between domain engineering and application engineering. The framework includes descriptions of the types of activities to be performed during each of the life-cycle phases, and provides motivation for the activities.

Addy, Edward A.↗

Verification and Validation of the PLTEMP/ANL Code for Thermal-Hydraulic Analysis of Experimental and Test Reactors (Code Version 4.3)

The document compiles in a single volume the verification and validation works done for the PLTEMP/ANL code during the years of its development and improvement. The verification of sixteen capabilities of the PLTEMP/ANL Version 4.3 code that were identified by research reactor analysts as frequently used in their thermal-hydraulic analysis are described and documented. Each chapter of the document deals with the verification or validation of a specific part of the software that calculates a specific phenomenon, e.g., channel flow calculation, coolant property calculation, heat transfer calculation, and flow instability calculation. The software verification work is usually done by comparing the code with hand calculation, Microsoft spreadsheet calculation, or Mathematica calculation. The software validation is done by comparing the code with experimental data or a widely tested code like the RELAP5 code. In addition, some PLTEMP/ANL verification works that are available in the open literature are simply referenced and not included in the document. PLTEMP/ANL has been used in conversion safety analysis reports of several US and foreign research reactors that have been licensed and converted. A list of such reactors is given.

22 GENERAL STUDIES OF NUCLEAR REACTORS↗

Program Verification for Extreme-Scale Applications (Final Scientific/Technical Report)

The project seeks to develop tools and techniques to help software developers verify the correctness and accuracy of their code. The target domain is scientific software of the kind widely used and developed in the Department of Energy research community, with a particular focus on "extreme scale" programs - those that are expected to involve possibly millions of parallel threads of execution. The report covers the University of Delaware contribution to the collaborative project. The project had a number of successful outcomes, especially regarding the development and extension of the CIVL software verification framework. CIVL is a verification tool for C or Fortran programs that use MPI, OpenMP, CUDA, and/or Pthreads for parallelization. CIVL went through vast improvements and extensions, and was successfully applied to a number of challenging codes. It found a subtle bug in the Devito PDE framework. It was able to verify the functional correctness of a conjugate gradient solver using a novel probabilistic technique with vanishingly small chance of error. CIVL was used very successfully in verification competitions, and the CIVL solutions to the competition challenges were presented and published. CIVL was also used successfully by other researchers on a computational chemistry kernel.

97 MATHEMATICS AND COMPUTING↗

Comparative Assessment of Experimental Testing of Instrument with an Embedded Digital Device Using Model-Based and Conventional Methods

The use of digital equipment has not been widespread in U.S. nuclear facilities. A major contributing factor to this situation arises from regulatory concerns about common cause failures (CCFs) stemming from the use of identical software in redundant systems, questions as to how to quantify the reliability of software-based products, validity of tools that are used for software verification and validation (V&V), and the effectiveness of software QA procedures. Compounding the concerns are sporadic incidents of digital equipment malfunctions in nuclear power plants, including lockups resulting from software memory leaks, feedwater control malfunctions due to excessive traffic on Ethernet networks, software logic errors, and other problems leading to plant trips. Additionally, the limited amount of demonstrated research and a lack of industry consensus on quantitative software reliability methodologies has hindered the widespread adoption of digital I&C in the nuclear industry. In a recent Regulatory Issue Summary (RIS), the U.S. Nuclear Regulatory Commission (NRC) identified concerns about the impact of greater use of instrumentation and control (I&C) equipment with an embedded digital device (EDD) [1]. Specifically, the NRC staff states that increased use of such devices “may increase a facility’s vulnerability to a CCF” (i.e., common-cause failure). The prevailing NRC guidance regarding software CCF (SCCF) identifies two design attributes that are acceptable for eliminating CCF concerns: (1) diversity or (2) testability (specifically, 100% testability). Either solution can result in high costs and remaining licensing uncertainty (i.e., how much diversity is enough? how to ensure test coverage of every possible sequence of device states?). Consequently, many utilities and reactor designers have limited or avoided more extensive use of digital technology to minimize licensing, scheduling, and financial risk. Without development of cost effective qualification methods to satisfy regulatory requirements and address the potential for CCF vulnerability associated with EDDs, the nuclear power industry may not be able to realize the benefits of digital technology achieved by other industries. In order to address these challenges, the U.S. Department of Energy (DOE) is sponsoring this research to assess the prospect of CCF in digital I&C equipment. The purpose of the current research is to develop an effective approach employing science-based methods to resolve concerns about CCF vulnerability that serve to inhibit deployment of advanced instrumentation (e.g., sensors, actuators, microcontrollers) with EDDs in nuclear power applications. The research objectives address the challenge of establishing high levels of safety and reliability assurance needed for the qualification of EDDs (e.g., microprocessors, programmable logic devices) that are subject to software design faults, complex failure modes, and CCF vulnerability. Specific objectives are: (1) assess the regulatory context for treatment of CCF vulnerability a graded approach to their qualification, (3) develop and extend model-based testing methods to enable effective demonstration of whether devices are subject to CCF, which may arise from vulnerabilities introduced at any stage of the design lifecycle, (4) establish a cost-effective testing framework that incorporates automation and test scenario prioritization, and (5) demonstrate the qualification approach through selection and testing of candidate digital device(s). This report documents an assessment of the results from experimental testing of a representative instrument with an embedded digital device. The experiment serves as a proof-of-concept demonstration of a model-based testing (MBT) framework. The objective of MBT is to ensure that an EDD undergoes suitably comprehensive testing to establish that it is not subject to SCCF. The approach by which MBT accomplishes this objective is through development and application of an effective test suite that provides the appropriate coverage to detect the full range of postulated faults that may arise at the requirements, design, and code (implementation) level of the EDD software. The findings of the experiment involve the application of the MBT framework by Ohio State University (OSU) through testing of the selected demonstration instrument (i.e., the prototype smart pressure sensor developed by Virginia Commonwealth University, VCU). In addition, the experiment findings also involve application of a more conventional black-box testing approach that serves as a baseline against which the MBT methodology can be compared. The primary outcome documented in this report is the comparative analysis of the capabilities demonstrated for each method. The results of the analysis demonstrate clear benefits that arise from the MBT methodology. The comparison indicates greater effectiveness from the more comprehensive evidence available through MBT and enhanced efficiency achieved through automation within the MBT framework. The structure of the report addresses the approach and application of each test method as well as the comparative analysis of the experimental results. Chapter 2 gives a summary overview of the demonstration approach. Chapter 3 covers the baseline testing and Chapter 4 documents the model-based testing. Chapter 5 describes the findings of the comparative analysis and presents the conclusions that can be drawn about the effectiveness and efficiency of the MBT methodology.

47 OTHER INSTRUMENTATION↗

Electric power system test and verification program

Space Station Freedom's (SSF's) electric power system (EPS) hardware and software verification is performed at all levels of integration, from components to assembly and system level tests. Careful planning is essential to ensure the EPS is tested properly on the ground prior to launch. The results of the test performed on breadboard model hardware and analyses completed to date have been evaluated and used to plan for design qualification and flight acceptance test phases. These results and plans indicate the verification program for SSF's 75-kW EPS would have been successful and completed in time to support the scheduled first element launch.

Rylicki, Daniel S.↗

Uncertainty Propagation from Flux to α and from Time to α in Reaction History

This report documents measurement uncertainty propagation from flux to α and from time to α in gamma reaction history. Analytical formulas are derived, and on the basis of them, their discrete versions are provided to serve for current reaction history software verification, and for development of the future versions of the software. The discrete version is provided for the general case: sparse data with varying time intervals between the data points.

73 NUCLEAR PHYSICS AND RADIATION PHYSICS↗

Verification of the REBUS Software

Ongoing design activities at Argonne National Laboratory are requiring a thorough verification of the Argonne Reactor Computation codes be performed. REBUS is central to this system. The driver for this effort requires the Triangular-Z and hexagonal-Z core geometry options of REBUS to be verified. Previous work identified the REBUS features required to be verified to support current design activities, features of which are generally applicable to hexagonal-Z fast reactor designs. The scope of this verification effort includes verifying REBUS’s ability to correctly intepret the user input model, verifying that the features identified yield the intended results, and verifying the correctness of the REBUS output tables. The REBUS software verification relies heavily upon the accuracy of the embedded DIF3D software, the verification of which was completed and documented elsewhere. Given that DIF3D produces an accurate solution, the primary focus of the verification in the REBUS software is to ensure that it properly uses the DIF3D solution and that the depletion system (Bateman equations) are correctly implemented. This manuscript reiterates the verification tasks and displays results with respect to the features needed for current design activities. Analytic solutions of the Batemen equations are displayed and the results calculated with REBUS are displayed demonstrating the accuracy. Since coupled Bateman and neutron diffusion/transport solutions are extremely difficult to obtain, much of the focus is placed on how REBUS uses a given DIF3D solution assuming the accuracy of the DIF3D solution. The verification effort identified no issues that are debilitating or otherwise impactful to the design usage of REBUS, and thus REBUS version 11.0, release 3012 is considered verified. It is important to note that several outputs of REBUS are identified to be inaccurate, such as burnup in MWD/MT. Most of the relevant ones for VTR are generally accurate with 10-20% errors which is not impactful as all regular REBUS users are aware of this issue and know how to hand calculate the results. The REBUS manual further makes it clear that these values are consistent with the methodology being used by REBUS and thus the “errors” are more of an inconsistent definition with respect to what a user would expect given a definition in literature. Other issues that were identified included unclear documentation and software bugs all of which were inconsequential to the final results.

22 GENERAL STUDIES OF NUCLEAR REACTORS↗