Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “formal 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 487 records · Page 27
All sourcesNASA NTRSDOE OSTI
NASA NTRSDate not supplied

FRET Tutorial

In this tutorial, we present the FRET tool for writing, understanding, formalizing and analyzing requirements. In practice, requirements are typically written in natural language, which is ambiguous and consequently not amenable to formal analysis. Since formal, mathematical notations are unintuitive, requirements in FRET are entered in a restricted, natural language, called FRETish with precise unambiguous meaning. This tutorial explains how requirements can be captured in FRETish and subsequently formalized in temporal logics and in the synchronous data flow language Lustre. We show, through multiple examples, how FRET assists users in understanding FRETish requirements and clarifying subtle semantic issues through English and diagrammatic explanations as well as interactive simulation. FInally, this tutorial describes how FRET can be used to perform realizability checking for identifying conflicting requirements and the connection of FRET with (1) the CoCoSim automated analysis tool for the verification of Simulink and Stateflow models, and (2) the Copilot runtime monitoring tool for the analysis of C programs.

FRET↗
DOE OSTI2025

Real-time neutron multiplicity and source localization for criticality safety during fuel debris removal

Advancing neutron detection and analysis techniques for complex radiation environments is an ongoing focus in nuclear instrumentation and monitoring. This proposal presents research and development of a generalized real-time neutron monitoring and analysis system, applicable to any detector capable of producing time-tagged neutron count data. While the work is demonstrated using the Neutron Multiplication Analysis Detector (NoMAD), a modular 15-tube helium-3 (He-3) array, due to its availability, spatial resolution, and flexible deployment, the methods developed are extensible to other systems, including organic scintillators and fast digital detectors. This research investigates two complementary analytical techniques for real-time characterization of neutron emitting sources: neutron multiplicity estimation based on the Hage-Cifarelli formalism and spatial localization using supervised machine learning applied to spatial count rate patterns. These methods are designed to operate under dynamic, evolving conditions such as fuel debris retrieval or reactor startup, where neutron-emitting material geometries may be partially unknown or changing over time. By integrating statistical neutron emission data with spatial localization, this research aims to develop and evaluate methods for real time neutron monitoring, source characterization, and material verification. Key contributions include implementation of a low-latency data pipeline for continuous neutron multiplicity analysis, development and validation of machine learning models for spatial inference, and experimental evaluation of system performance under variable measurement conditions. The outcomes are intended to support applications in nuclear safeguards, verification, emergency response, and reactor startup.

46 INSTRUMENTATION RELATED TO NUCLEAR SCIENCE AND ↗
NASA NTRS1999

Analyzing Mode Confusion via Model Checking

Mode confusion is one of the most serious problems in aviation safety. Today's complex digital flight decks make it difficult for pilots to maintain awareness of the actual states, or modes, of the flight deck automation. NASA Langley leads an initiative to explore how formal techniques can be used to discover possible sources of mode confusion. As part of this initiative, a flight guidance system was previously specified as a finite Mealy automaton, and the theorem prover PVS was used to reason about it. The objective of the present paper is to investigate whether state-exploration techniques, especially model checking, are better able to achieve this task than theorem proving and also to compare several verification tools for the specific application. The flight guidance system is modeled and analyzed in Murphi, SMV, and Spin. The tools are compared regarding their system description language, their practicality for analyzing mode confusion, and their capabilities for error tracing and for animating diagnostic information. It turns out that their strengths are complementary.

Luettgen, Gerald↗
NASA NTRS2003

Experimental Evaluation of Verification and Validation Tools on Martian Rover Software

We report on a study to determine the maturity of different verification and validation technologies (V&V) on a representative example of NASA flight software. The study consisted of a controlled experiment where three technologies (static analysis, runtime analysis and model checking) were compared to traditional testing with respect to their ability to find seeded errors in a prototype Mars Rover. What makes this study unique is that it is the first (to the best of our knowledge) to do a controlled experiment to compare formal methods based tools to testing on a realistic industrial-size example where the emphasis was on collecting as much data on the performance of the tools and the participants as possible. The paper includes a description of the Rover code that was analyzed, the tools used as well as a detailed description of the experimental setup and the results. Due to the complexity of setting up the experiment, our results can not be generalized, but we believe it can still serve as a valuable point of reference for future studies of this kind. It did confirm the belief we had that advanced tools can outperform testing when trying to locate concurrency errors. Furthermore the results of the experiment inspired a novel framework for testing the next generation of the Rover.

Brat, Guillaume↗
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 NTRS1994

Automated Test Environment for a Real-Time Control System

An automated environment with hardware-in-the-loop has been developed by Rocketdyne Huntsville for test of a real-time control system. The target system of application is the man-rated real-time system which controls the Space Shuttle Main Engines (SSME). The primary use of the environment is software verification and validation, but it is also useful for evaluation and analysis of SSME avionics hardware and mathematical engine models. It provides a test bed for the integration of software and hardware. The principles and skills upon which it operates may be applied to other target systems, such as those requiring hardware-in-the-loop simulation and control system development. Potential applications are in problem domains demanding highly reliable software systems requiring testing to formal requirements and verifying successful transition to/from off-nominal system states.

Hall, Ronald O.↗
NASA NTRS1994

Formal semantics for a subset of VHDL and its use in analysis of the FTPP scoreboard circuit

In the first part of the report, we give a detailed description of an operational semantics for a large subset of VHDL, the VHSIC Hardware Description Language. The semantics is written in the functional language Caliban, similar to Haskell, used by the theorem prover Clio. We also describe a translator from VHDL into Caliban semantics and give some examples of its use. In the second part of the report, we describe our experience in using the VHDL semantics to try to verify a large VHDL design. We were not able to complete the verification due to certain complexities of VHDL which we discuss. We propose a VHDL verification method that addresses the problems we encountered but which builds on the operational semantics described in the first part of the report.

Bickford, Mark↗
NASA NTRS2013

Modeling and Analysis of Asynchronous Systems Using SAL and Hybrid SAL

We present formal models and results of formal analysis of two different asynchronous systems. We first examine a mid-value select module that merges the signals coming from three different sensors that are each asynchronously sampling the same input signal. We then consider the phase locking protocol proposed by Daly, Hopkins, and McKenna. This protocol is designed to keep a set of non-faulty (asynchronous) clocks phase locked even in the presence of Byzantine-faulty clocks on the network. All models and verifications have been developed using the SAL model checking tools and the Hybrid SAL abstractor.

Tiwari, Ashish↗
NASA NTRS1991

Integrity and security in an Ada runtime environment

A review is provided of the Formal Methods group discussions. It was stated that integrity is not a pure mathematical dual of security. The input data is part of the integrity domain. The group provided a roadmap for research. One item of the roadmap and the final position statement are closely related to the space shuttle and space station. The group's position is to use a safe subset of Ada. Examples of safe sets include the Army Secure Operating System and the Penelope Ada verification tool. It is recommended that a conservative attitude is required when writing Ada code for life and property critical systems.

Bown, Rodney L.↗
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 NTRS1995

Sea surface topography fields of the tropical Pacific from data assimilation

Time series of maps of monthly tropical Pacific dynamic topography anomalies from 1979 through 1985 were constructed by means of assimilation of the tide gauge and expendable bathythermograph (XBT) data into a linear model driven by observed winds. Estimates of error statistics were calculated and compared to actual differences between hindcasts and observations. Four experiements were performed as follows: one with no assimilation, one with assimiation of sea level anomaly data from eight selected island tide gauge stations, one with assimilation of dynamic height anomalies derived from XBT data, and one with both XBT and tide gauge data assimilated. Data from seven additional tide gauge stations were withheld from the assimilation process and used for verification in all four experiements. Statistical objective maps based on data alone were also constructed for comparison purposes. The dynamic response of the model without assimilation was, in general, weaker than the observed response. Assimilation resulted in enhanced signal amplitude in all three assimilation experiments. With few exceptions the error estimated generated by the Kalman filter appeared quite reasonable. Since the error processes cannot be assumed to be white or stationary, we could find no straightforward way to test the formal statistical hypothesis that the time series of differences between the filter ouput and the actual observations were drawn from a population with statistics given by the Kalman filter estimaes. We found that the best filter we could devise was still short of the goal of producing a white innovation sequence. Extensive changes in the assumed error statistics make only marginal differences. The same is true for long time and space scale behavior of different models with richer physics and finer resolution. Better data assimilation results will probably require relaxation of the assumptions of stationarity and serial independence of the errors. Formation of such detailed noise models will require longer time series, with the attendant problems of matching very different data sets.

Miller, Robert N.↗
NASA NTRS2020

Europa Clipper Mission: Onward to Implementation!

Europa, the fourth largest moon of Jupiter, is believed to be one of the best places in the solar system to look for extant life beyond Earth, and the Europa Clipper Mission is preparing to investigate. Now entering the fifth year of life as a formal project, the Europa Clipper Mission has completed its major design phase and is preparing for implementation. The mission envisions sending a flight system, consisting of a spacecraft equipped with a payload of NASA-selected scientific instruments, to execute numerous flybys of Europa while in Jupiter orbit. The mission is being formulated and implemented by a joint Jet Propulsion Laboratory (JPL) and Applied Physics Laboratory (APL) Project team. At the Project Preliminary Design Review (PDR) in August 2018, it was determined that the unique integration of the REASON instrument’s antennas with the spacecraft’s solar arrays required additional time for maturity and review. The required maturity was demonstrated, and in June 2019 the Clipper Mission passed its Delta Preliminary Design Review, and formal confirmation for entry into Phase C was announced by NASA in August 2019. The earliest launch opportunity is now in July 2023, one year later than originally planned. The Project is now working toward its Critical Design Review in May 2020. This paper will describe the progress of the Europa Clipper Mission since January 2019, including maturation of the spacecraft, subsystem and instrument designs, the beginning of fabrication of engineering models and the first flight models, planning for the verification & validation phase, and planning for operations.

Jackson, Maddalena↗
NASA NTRS1939

Full-Scale Wind-Tunnel Investigation of Wing-Cooling Ducts Effects of Propeller Slipstream, Special Report

The safety of remotely operated vehicles depends on the correctness of the distributed protocol that facilitates the communication between the vehicle and the operator. A failure in this communication can result in catastrophic loss of the vehicle. To complicate matters, the communication system may be required to satisfy several, possibly conflicting, requirements. The design of protocols is typically an informal process based on successive iterations of a prototype implementation. Yet distributed protocols are notoriously difficult to get correct using such informal techniques. We present a formal specification of the design of a distributed protocol intended for use in a remotely operated vehicle, which is built from the composition of several simpler protocols. We demonstrate proof strategies that allow us to prove properties of each component protocol individually while ensuring that the property is preserved in the composition forming the entire system. Given that designs are likely to evolve as additional requirements emerge, we show how we have automated most of the repetitive proof steps to enable verification of rapidly changing designs.

Nickle, F. R.↗
NASA NTRS1977

Documentation requirements for Applications Systems Verification and Transfer projects (ASVTs)

NASA's Application Systems Verification and Transfer Projects (ASVTs) are deliberate efforts to facilitate the transfer of applications of NASA-developed space technology to users such as federal agencies, state and local governments, regional planning groups, public service institutions, and private industry. This study focused on the role of documentation in facilitating technology transfer both to primary users identified during project planning and to others with similar information needs. It was understood that documentation can be used effectively when it is combined with informal (primarily verbal) communication within each user community and with other formal techniques such as organized demonstrations and training programs. Documentation examples from eight ASVT projects and one potential project were examined to give scope to the investigation.

Suchy, J. T.↗
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↗
NASA NTRS1992

Software design as a problem in learning theory (a research overview)

Our interest in automating software design has come out of our research in automated reasoning, inductive inference, learnability, and algebraic machine theory. We have investigated these areas extensively, in connection with specific problems of language representation, acquisition, processing, and design. In the case of formal context-free (CF) languages we established existence of finite learnable models ('behavioral realizations') and procedures for constructing them effectively. We also determined techniques for automatic construction of the models, inductively inferring them from finite examples of how they should 'behave'. These results were obtainable due to appropriate representation of domain knowledge, and constraints on the domain that the representation defined. It was when we sought to generalize our results, and adapt or apply them, that we began investigating the possibility of determining similar procedures for constructing correct software. Discussions with other researchers led us to examine testing and verification processes, as they are related to inference, and due to their considerable importance in correct software design. Motivating papers by other researchers, led us to examine these processes in some depth. Here we present our approach to those software design issues raised by other researchers, within our own theoretical context. We describe our results, relative to those of the other researchers, and conclude that they do not compare unfavorably.

Fass, Leona F.↗