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 271 records · Page 15
All sourcesNASA NTRSDOE OSTI
NASA NTRSDate not supplied

An Evaluation of Extended Reality Technologies for Use in Verification Testing at NASA 2024 HRP IWS Abstract

BACKGROUND At NASA, verification testing is the formal process of ensuring that a product conforms to requirements set by a project or program. Some verification methods, such as Demonstrations and Test, require either the end product or a mockup of the product with sufficient fidelity to stand-in for the product during the test. Traditionally, these mockups have been physical (e.g., foam-core and wood) but there is growing interest in exploring new methods for testing with these mockups. These methods include virtual reality (VR), mixed reality, and augmented reality which are collectively referred to as eXtended Reality (XR) technologies. VR has already been adopted and used by many in the aerospace industry as a tool for use in early design phases (e.g., developmental testing) and may have the most potential for use in verification tests. Benefits of using VR mockups offer cost effectiveness, ease of iteration, simulation of hazardous conditions (e.g., an egress through a hatch with smoke obscuring vision), and the ability to simulate microgravity conditions, which are challenging to do with physical mockups. However, the validity of test results obtained from VR mockup demonstrations or testing, compared to the current gold standard of physical mockups, remains uncertain. It is unlikely that there is one clean answer as there are many different types of verification outcomes and each XR technology must be evaluated on its own merits. This is not an issue during developmental testing as the design is still in flux and the total success of the design is not dependent upon the results of a developmental test. Verification tests, however, only happen once, assuming no change to the design, and the results are used to certify the product. Therefore, establishing the validity of XR mockup-based verification outcomes is essential before considering them for any use in verification tests. OBJECTIVE AND METHOD To address this concern, the Human Research Program has funded a project to explore and qualify how XR technologies might be used in verification demonstration and testing at NASA. Currently, we are conducting a review of the literature on the utilization of XR mockups for design activities, prototyping, and user testing. We are employing the Strengths, Weaknesses, Opportunities, and Threats (SWOT) analysis method to identify the pros, cons, and barriers to adoption of XR technologies for verification testing at NASA. Additionally, we are developing a framework to guide the deployment of XR mockups for verification tests. Building upon available evidence from the literature and subject-matter expert feedback, our goal for the framework is to provide guidelines for which forms of XR mockups are suitable for a given verification test, when only physical mockups should be employed and to highlight areas for which more evidence is needed. To further refine our framework and to contribute to the body of evidence, we are planning a lab-based experiment comparing a VR mockup to a physical twin for a set of select verification outcomes. ANTICIPATED RESULTS In this presentation, we will present the work we conducted to evaluate XR technologies for use in verification tests at NASA. We will summarize and report our findings from the SWOT analysis and our lab-based study, and we will present the current state of the XR Technologies for Verification Testing framework. We will conclude by summarizing remaining work and future directions for the project. Technologies for Verification Testing framework. We will conclude by summarizing remaining work and future directions for the project.

Extended Reality↗
NASA NTRS1993

Using Penelope to assess the correctness of NASA Ada software: A demonstration of formal methods as a counterpart to testing

Life-critical applications warrant a higher level of software reliability than has yet been achieved. Since it is not certain that traditional methods alone can provide the required ultra reliability, new methods should be examined as supplements or replacements. This paper describes a mathematical counterpart to the traditional process of empirical testing. ORA's Penelope verification system is demonstrated as a tool for evaluating the correctness of Ada software. Grady Booch's Ada calendar utility package, obtained through NASA, was specified in the Larch/Ada language. Formal verification in the Penelope environment established that many of the package's subprograms met their specifications. In other subprograms, failed attempts at verification revealed several errors that had escaped detection by testing.

Eichenlaub, Carl T.↗
NASA NTRS2020

Bridging the Gap Between Requirements and Model Analysis : Evaluation on Ten Cyber-Physical Challenge Problems

Formal verfication and simulation are powerful tools to validate requirements against complex systems. [Problem] Requirements are developed in early stages of the software lifecycle and are typically written in ambiguous natural language. There is a gap between such requirements and formal notations that can be used by verification tools, and lack of support for proper association of requirements with software artifacts for verification. [Principal idea] We propose to write requirements in an intuitive, structured natural language with formal semantics, and to support formalization and model/code verification as a smooth, well-integrated process. [Contribution] We have developed an end-to-end, open source requirements analysis framework that checks Simulink models against requirements written in structured natural language. Our framework is built in the Formal Requirements Elicitation Tool (fret); we use fret's requirements language named fretish, and formalization of fretish requirements in temporal logics. Our proposed framework contributes the following features: 1) automatic extraction of Simulink model information and association of fretish requirements with target model signals and components; 2) translation of temporal logic formulas into synchronous dataflow cocospec specifications as well as Simulink monitors, to be used by verification tools; we establish correctness of our translation through extensive automated testing; 3) interpretation of counterexamples produced by verification tools back at requirements level. These features support a tight integration and feedback loop between high level requirements and their analysis. We demonstrate our approach on a major case study: the Ten Lockheed Martin Cyber-Physical, aerospace-inspired challenge problems.

Mavridou, Anastasia↗
DOE OSTI2021

Open Building Control

Best practice control sequences are often not implemented correctly, or are not implemented at all, in large commercial buildings. This typically leads to 10-30 percent energy waste, along with reduced occupant productivity and unnecessary equipment wear. The current process of designing and implementing such control sequences is a manual process that starts with designers who often don’t have adequate training, then requires controls programmers to interpret and program a verbose written sequence. This process has been shown to fail to deliver high performance control sequences at scale. The Open Building Control project digitizes the current control delivery process. The project is developing tools for system designers to select control sequences, assess their energy performance and load flexibility potential using whole building simulation, specify the sequence for implementation using machine-to-machine translation by a control provider and formally testing the as-installed sequences by a commissioning agent. The project developed tools for each stage of this delivery process. The key innovation of the project is the development of the Control Description Language, a language that allows such a digitized control delivery process with end-to-end verification. Libraries of control sequences have been implemented using the Control Description Language, and their performance has been demonstrated using whole building energy simulation. An automated translation of such sequences to a commercial control product line has been conducted using a prototype translator. Tools for formal verification of as-installed control sequences relative to their specification have been developed and demonstrated. The American Society of Heating, Refrigerating and Air-Conditioning Engineers (ASHRAE) started the process of forming a committee to make this language an ASHRAE/ANSI Standard. This new standard will complement existing and emerging ASHRAE standards for building communication and semantic modeling by providing a standard for expressing the control logic - the actual brain of the building. We expect this language and the process it enables to be an important contribution to the deployment of high performance building control sequences at scale because it allows taming the complexity of the control delivery process, which is continually increasing due to the need for higher performance and increased load flexibility to meet goals for net zero energy and increased renewable integration.

32 ENERGY CONSERVATION, CONSUMPTION, AND UTILIZATI↗
DOE OSTI2022

Verification and Validation Activities for the Multi-Fidelity Toolkit

The Multi-Fidelity Toolkit (MFTK) is a simulation tool being developed at Sandia National Laboratories for aerodynamic predictions of compressible flows over a range of physics fidelities and computational speeds. These models include the Reynolds-Averaged-Navier-Stokes (RANS) equations, the Euler equations, and modified Newtonian aerodynamics (MNA) equations, and they can be invoked independently or coupled with hierarchical Kriging to interpolate between high-fidelity simulations using lower-fidelity data. However, as with any new simulation capability, verification and validation are necessary to gather credibility evidence. This work describes formal code- and solution-verification activities as well as model validation with uncertainty considerations. Code verification is performed on the MNA model by comparing with an analytical solution for flat-plate and inclined-plate geometries. Solution-verification activities include grid-refinement studies of HIFiRE-1 wind tunnel measurements, which are used for validation, for all model fidelities. A thorough treatment of the validation comparison with prediction error and validation uncertainty is also presented.

42 ENGINEERING↗
DOE OSTI2023

Expanded verification and validation studies of hypersonic aerodynamics with multiple physics-fidelity models

Hypersonic aerothermodynamics is an important domain of modern multiphysics simulation. The Multi-Fidelity Toolkit is a simulation tool being developed at Sandia National Laboratories to predict aerodynamic properties for compressible flows from a range of physics fidelities and computational speeds. These models include the Reynolds-averaged Navier–Stokes (RANS) equations, the Euler equations with momentum-energy integral technique (MEIT), and modified Newtonian aerodynamics with flat-plate boundary layer (MNA+FPBL) equations, and they can be invoked independently or coupled with hierarchical Kriging to interpolate between high-fidelity simulations using lower-fidelity data. However, as with any new simulation capability, verification and validation are necessary to gather credibility evidence. This work describes formal code- and solution-verification activities, as well as model validation with uncertainty considerations. Code verification activities on the MNA+FPBL model build on previous work by focusing on the viscous portion of the model. Viscous quantities of interest are compared against those from an analytical solution for flat-plate, inclined-plate, and cone geometries. The code verification methodology for the MEIT model is also presented. Test setup and results of code verification tests on the laminar and turbulent models within MEIT are shown. Solution-verification activities include grid-refinement studies on simulations that model the HIFiRE-1 wind tunnel experiments. These experiments are used for validation of all model fidelities. A thorough validation comparison with prediction error and uncertainty is also presented. Three additional HIFiRE-1 experimental runs are simulated in this study, and the solution verification and validation work examines the effects of the associated parameter changes on model performance. Finally, a study is presented that compares the computational costs and fidelities from each of the different models.

42 ENGINEERING↗
NASA NTRS1983

The use of a formal simulator to verify a simple real time control program

The authors present an initial and elementary investigation of the formal specification and mechanical verification of programs that interact with environments. They describe a mechanical proof that a simple, real time control program keeps a vehicle on a straightline course in a variable crosswind. To formalize the specification they define a mathematical function which models the interaction of the program and its environment. They then state and proved two theorems about this function: the simulated vehicle never gets farther than three units away from the intended course, and it comes to the course if the wind ever remains steady for at least four sampling units.

Boyer, R. S.↗
NASA NTRS1990

A verified model of fault-tolerance

The main objectives are: a model of a replicated system with exact-match voting; a fault model that includes transients; a theorem that establishes the conditions under which the system provides fault tolerance; a formal specification of the model; and a mechanically checked verification of the theorem that is consonant with the journal-level presentation. Formal specification and verification revealed typos in the original report, exposed omission in original proof, led to the stronger theorem and more elegant proof, and confirmed that Enhanced Hierarchical Development Methodology (EHDM) has the capability to specify interesting and useful properties in a direct, natural, and readable manner.

Rushby, John↗
NASA NTRS1995

Third NASA Langley Formal Methods Workshop

This publication constitutes the proceedings of NASA Langley Research Center's third workshop on the application of formal methods to the design and verification of life-critical systems. This workshop brought together formal methods researchers, industry engineers, and academicians to discuss the potential of NASA-sponsored formal methods and to investigate new opportunities for applying these methods to industry problems. contained herein are copies of the material presented at the workshop, summaries of many of the presentations, a complete list of attendees, and a detailed summary of the Langley formal methods program. Much of this material is available electronically through the World-Wide Web via the following URL.

Holloway, C. Michael↗
NASA NTRSDate not supplied

From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project

The Independent Configurable Architecture for Reliable Operations of Unmanned Systems(ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.

Formal Methods↗
NASA NTRSDate not supplied

Monitoring ICAROUS: From Requirements to Autonomous Flight

The Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.

Formal Methods↗
NASA NTRSDate not supplied

Embedding Differential Dynamic Logic in PVS

Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and mission-critical applications. This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and dL’s proof calculus. The formalization embeds dL into the PVS logic, resulting in a version of dL whose proof calculus is not only formally verified, but is also available for the verification of hybrid programs within PVS itself. This embedding, called Plaidypvs (Properly Assured Implementation of dL for Hybrid Program Verification and Specification), supports standard dL style proofs, but further leverages the capabilities of PVS to allow reasoning about entire classes of hybrid programs. The embedding also allows the user to import the well-established definitions and mathematical theories available in PVS.

PVS↗
NASA NTRS1996

Using Formal Methods to Assist in the Requirements Analysis of the Space Shuttle GPS Change Request

We describe a recent NASA-sponsored pilot project intended to gauge the effectiveness of using formal methods in Space Shuttle software requirements analysis. Several Change Requests (CR's) were selected as promising targets to demonstrate the utility of formal methods in this application domain. A CR to add new navigation capabilities to the Shuttle, based on Global Positioning System (GPS) technology, is the focus of this report. Carried out in parallel with the Shuttle program's conventional requirements analysis process was a limited form of analysis based on formalized requirements. Portions of the GPS CR were modeled using the language of SRI's Prototype Verification System (PVS). During the formal methods-based analysis, numerous requirements issues were discovered and submitted as official issues through the normal requirements inspection process. Shuttle analysts felt that many of these issues were uncovered earlier than would have occurred with conventional methods. We present a summary of these encouraging results and conclusions we have drawn from the pilot project.

DiVito, Ben L.↗
NASA NTRS1996

The Verification-based Analysis of Reliable Multicast Protocol

Reliable Multicast Protocol (RMP) is a communication protocol that provides an atomic, totally ordered, reliable multicast service on top of unreliable IP Multicasting. In this paper, we develop formal models for R.W using existing automatic verification systems, and perform verification-based analysis on the formal RMP specifications. We also use the formal models of RW specifications to generate a test suite for conformance testing of the RMP implementation. Throughout the process of RMP development, we follow an iterative, interactive approach that emphasizes concurrent and parallel progress between the implementation and verification processes. Through this approach, we incorporate formal techniques into our development process, promote a common understanding for the protocol, increase the reliability of our software, and maintain high fidelity between the specifications of RMP and its implementation.

Wu, Yunqing↗
NASA NTRS1982

Advanced flight control system study

A fly by wire flight control system architecture designed for high reliability includes spare sensor and computer elements to permit safe dispatch with failed elements, thereby reducing unscheduled maintenance. A methodology capable of demonstrating that the architecture does achieve the predicted performance characteristics consists of a hierarchy of activities ranging from analytical calculations of system reliability and formal methods of software verification to iron bird testing followed by flight evaluation. Interfacing this architecture to the Lockheed S-3A aircraft for flight test is discussed. This testbed vehicle can be expanded to support flight experiments in advanced aerodynamics, electromechanical actuators, secondary power systems, flight management, new displays, and air traffic control concepts.

Hartmann, G. L.↗
NASA NTRS2004

Meeting the Deadline: Why, When and How

A normative system is defined as any set of interacting agents whose behavior can usefully be regarded as norm-directed. Most organizations, and more specifically institutions, fall under this definition. Interactions in these normative systems are regulated by normative templates that describe desired behavior in terms of deontic concepts (obligations, prohibitions and permissions), deadlines, violations and sanctions. Agreements between agents, and between an agent and the society, can then be specified by means of contracts. Contracts provide flexible but verifiable means to integrate society requirements and agent autonomy. and are an adequate means for the explicit specification of interactions. From the society perspective, it is important that these contracts adhere to the specifications described in the model of the organization. If we want to automate such verifications, we have to formalize the languages used for contracts and for the specification of organizations. The logic LCR is based on deontic temporal logic. LCR is an expressive language for describing interaction in multi-agent systems, including obligations with deadlines. Deadlines are important norms in most interactions between agents. Intuitively, a deadline states that an agent should perform an action before a certain point in time. The obligation to perform the action starts at the moment the deadline becomes active. E.g. when a contract is signed or approved. If the action is not performed in time a violation of the deadline occurs. It can be specified independently what measure has to be taken in this case. In this paper we investigate the deadline concept in more detail. The paper is organized as follows. Section 2 defines the variant of CTL we use. In section 3, we discuss the basic intuitions of deadlines. Section 4 presents a first intuitive formalization for deadlines. In section 5, we look at a more complex model for deadlines trying to catch some more practical aspects. Finally, in section 6 we present issues for future work and our conciusions.

Dignum, Frank↗
NASA NTRS2014

Numerical Simulations For the F-16XL Aircraft Configuration

Numerical simulations of flow around the F-16XL are presented as a contribution to the Cranked Arrow Wing Aerodynamic Project International II (CAWAPI-II). The NASA Tetrahedral Unstructured Software System (TetrUSS) is used to perform numerical simulations. This CFD suite, developed and maintained by NASA Langley Research Center, includes an unstructured grid generation program called VGRID, a postprocessor named POSTGRID, and the flow solver USM3D. The CRISP CFD package is utilized to provide error estimates and grid adaption for verification of USM3D results. A subsonic high angle-of-attack case flight condition (FC) 25 is computed and analyzed. Three turbulence models are used in the calculations: the one-equation Spalart-Allmaras (SA), the two-equation shear stress transport (SST) and the kε turbulence models. Computational results, and surface static pressure profiles are presented and compared with flight data. Solution verification is performed using formal grid refinement studies, the solution of Error Transport Equations, and adaptive mesh refinement. The current study shows that the USM3D solver coupled with CRISP CFD can be used in an engineering environment in predicting vortex-flow physics on a complex configuration at flight Reynolds numbers.

Elmiligui, Alaa A.↗
NASA NTRS2013

Soil Moisture Active Passive Mission: Fault Management Design Analyses

As a general trend, the complexities of modern spacecraft are increasing to include more ambitious mission goals with tighter timing requirements and on-board autonomy. As a byproduct, the protective features that monitor the performance of these systems have also increased in scope and complexity. Given cost and schedule pressures, there is an increasing emphasis on understanding the behavior of the system at design time. Formal test-driven verification and validation (V&V) is rarely able to test the significant combinatorics of states, and often finds problems late in the development cycle forcing design changes that can be costly. This paper describes the approach the SMAP Fault Protection team has taken to address some of the above-mentioned issues.

Earth↗