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.

SourceResearch connectionFrom yearThrough year

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

At least 451 records · Page 25

All sources NASA NTRS DOE OSTI

NASA NTRS2009

Theorem Proving in Intel Hardware Design

For the past decade, a framework combining model checking (symbolic trajectory evaluation) and higher-order logic theorem proving has been in production use at Intel. Our tools and methodology have been used to formally verify execution cluster functionality (including floating-point operations) for a number of Intel products, including the Pentium(Registered TradeMark)4 and Core(TradeMark)i7 processors. Hardware verification in 2009 is much more challenging than it was in 1999 - today s CPU chip designs contain many processor cores and significant firmware content. This talk will attempt to distill the lessons learned over the past ten years, discuss how they apply to today s problems, outline some future directions.

O'Leary, John↗

NASA NTRS2017

First Order Temporal Logic Monitoring with BDDs

Runtime verification is aimed at analyzing execution traces stemming from a running program or system. The traditional purpose is to detect the lack of conformance with respect to a formal specification. Numerous efforts in the field have focused on monitoring so-called parametric specifications, where events carry data, and formulas can refer to such. Since a monitor for such specifications has to store observed data, the challenge is to have an efficient representation and manipulation of Boolean operators, quantification, and lookup of data. The fundamental problem is that the actual values of the data are not necessarily bounded or provided in advance. In this work we explore the use of Binary Decision Diagrams (BDDs) for representing observed data. Our experiments show a substantial improvement in performance compared to related work.

Ulus, Dogan↗

DOE OSTI2016

Quantitative Analysis Guidance in Safety Software Validation

Quantitative analysis in software development has been a challenging topic over the years in safety software. While qualitative processes for vigorous safety software verification and validation (V and V) have been provided through standard such as IEEE 1012, quantitative analysis for V and V tasks such as correctness, completeness or accuracy evaluation have not been formally defined. In practice, there are quantitative analyses in terms of using software metrics. Many of these software metrics are useful in analyzing the test results. Some of them are used for providing guidance in code evaluation activities e.g. numbers of line of codes not exceeding certain limits, recursive calls are not allowed, etc. However, few can be used for providing quantitative analysis guidance for the V and V tasks such as completeness evaluation. AREVA Federal Services (AFS) has provided services for many nuclear projects in US. Through compliance with IEEE 1012, AFS V and V processes have provided vigorous qualitative processes ensuring quality level of the software products used in the project meeting the required nuclear software level. In addition, quantitative analysis is developed to provide structured validation framework ensuring 'zero defect' in the software products. This paper describes some aspects of the quantitative approaches using a sample safety application. (authors)

46 INSTRUMENTATION RELATED TO NUCLEAR SCIENCE AND ↗

NASA NTRS2002

Synthesizing Certified Code

Code certification is a lightweight approach to demonstrate software quality on a formal level. Its basic idea is to require producers to provide formal proofs that their code satisfies certain quality properties. These proofs serve as certificates which can be checked independently. Since code certification uses the same underlying technology as program verification, it also requires many detailed annotations (e.g., loop invariants) to make the proofs possible. However, manually adding theses annotations to the code is time-consuming and error-prone. We address this problem by combining code certification with automatic program synthesis. We propose an approach to generate simultaneously, from a high-level specification, code and all annotations required to certify generated code. Here, we describe a certification extension of AUTOBAYES, a synthesis tool which automatically generates complex data analysis programs from compact specifications. AUTOBAYES contains sufficient high-level domain knowledge to generate detailed annotations. This allows us to use a general-purpose verification condition generator to produce a set of proof obligations in first-order logic. The obligations are then discharged using the automated theorem E-SETHEO. We demonstrate our approach by certifying operator safety for a generated iterative data classification program without manual annotation of the code.

Whalen, Michael↗

NASA NTRS2017

Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis

This paper introduces a static analysis technique for computing formally verified round-off error bounds of floating-point functional expressions. The technique is based on a denotational semantics that computes a symbolic estimation of floating-point round-o errors along with a proof certificate that ensures its correctness. The symbolic estimation can be evaluated on concrete inputs using rigorous enclosure methods to produce formally verified numerical error bounds. The proposed technique is implemented in the prototype research tool PRECiSA (Program Round-o Error Certifier via Static Analysis) and used in the verification of floating-point programs of interest to NASA.

Moscato, Mariano↗

DOE OSTI2023

FY23 Status of Quality Assurance Plan for Out-of-Pile Test Data

The DOE Advanced Reactor Technology program has supported recovery and preservation of legacy metallic fuel data collected as part of the US fast reactor program, recognizing it as essential to development and licensing activities for advanced fast reactors. Databases were established as organized collections of experimental records and data generated from in-pile experiments at EBRII, FFTF, and TREAT as well as related out-of-pile examinations of irradiated fuels. The Out-of-Pile Transient Database (OPTD), includes records of over 150 out-of-pile furnace transient tests on metallic fuels conducted at Argonne’s Alpha-Gamma Hot Cell Facility to evaluate their transient performance and characterize fuel/cladding interaction. The database is accessible to registered users from US universities, laboratories, and nuclear industry. Because the data in OPTD has not been formally qualified, its applicability and ability to support licensing activities is limited. This report outlines progress and plans to quality assure data in OPTD, maximizing its impact for model validation and verification as well as qualification of fuels for safe and effective use in advanced reactor designs.

11 NUCLEAR FUEL CYCLE AND FUEL MATERIALS↗

NASA NTRS1995

DRS: Derivational Reasoning System

The high reliability requirements for airborne systems requires fault-tolerant architectures to address failures in the presence of physical faults, and the elimination of design flaws during the specification and validation phase of the design cycle. Although much progress has been made in developing methods to address physical faults, design flaws remain a serious problem. Formal methods provides a mathematical basis for removing design flaws from digital systems. DRS (Derivational Reasoning System) is a formal design tool based on advanced research in mathematical modeling and formal synthesis. The system implements a basic design algebra for synthesizing digital circuit descriptions from high level functional specifications. DRS incorporates an executable specification language, a set of correctness preserving transformations, verification interface, and a logic synthesis interface, making it a powerful tool for realizing hardware from abstract specifications. DRS integrates recent advances in transformational reasoning, automated theorem proving and high-level CAD synthesis systems in order to provide enhanced reliability in designs with reduced time and cost.

Bose, Bhaskar↗

DOE OSTI2019

A framework for assessment of predictive capability maturity and its application in nuclear thermal hydraulics

Here this work presents a formalized and computerized framework for the assessment of decision regarding the adequacy of a simulation tool for a nuclear reactor application. The decision regarding a code’s adequacy for an application is dependent on the assessment of different attributes that govern verification, validation, and uncertainty quantification of the code. In this work, the focus is on code validation. Therefore, the framework is developed and illustrated from the perspective of decision regarding the validation assessment of a code. Code validation assessment is performed based on the validation test results, data applicability, and process quality assurance factors. The process quality assurance factors warrant the trustworthiness of the evidence and help in checking people and process compliance with respect to the standard requirements. The proposed framework is developed using an argument modeling technique called Goal Structuring Notation (GSN). Goal structuring notation facilitates structural knowledge representation, information abstraction, evidence incorporation, and provides a skeletal structure for quantitative maturity assessment. The decision schema for the development of the decision model is based on the Predictive Capability Maturity Model (PCMM) and Analytic Hierarchy Process (AHP) and formalized using Goal structuring notation. Each decision attribute is formulated as a claim, where the degree of validity of the claim (attribute’s assessment) is expressed using different maturity levels. The GSN representation of the decision model is transformed into a confidence network to provide evidence-based quantitative maturity assessment using the Bayesian network. A metric based on the expected utility of maturity levels, called expected distance metric, is proposed to measure the distance between target maturity and achieved maturity on a scale of zero to one. Expected distance metric helps in comparing the assessment of different attributes and identification of major areas of concern in terms of modeling capability, data needs, and quality of assessment process. The practical application of the framework is demonstrated by a case study on validation assessment of a thermal-hydraulic code for a challenge problem called Departure from Nucleate Boiling (DNB).

42 ENGINEERING↗

NASA NTRS2014

Data Automata in Scala

The field of runtime verification has during the last decade seen a multitude of systems for monitoring event sequences (traces) emitted by a running system. The objective is to ensure correctness of a system by checking its execution traces against formal specifications representing requirements. A special challenge is data parameterized events, where monitors have to keep track of the combination of control states as well as data constraints, relating events and the data they carry across time points. This poses a challenge wrt. efficiency of monitors, as well as expressiveness of logics. Data automata is a form of automata where states are parameterized with data, supporting monitoring of data parameterized events. We describe the full details of a very simple API in the Scala programming language, an internal DSL (Domain-Specific Language), implementing data automata. The small implementation suggests a design pattern. Data automata allow transition conditions to refer to other states than the source state, and allow target states of transitions to be inlined, offering a temporal logic flavored notation. An embedding of a logic in a high-level language like Scala in addition allows monitors to be programmed using all of Scala's language constructs, offering the full flexibility of a programming language. The framework is demonstrated on an XML processing scenario previously addressed in related work.

runtime verification↗

NASA NTRS2011

Systems, methods and apparatus for generation and verification of policies in autonomic computing systems

Described herein is a method that produces fully (mathematically) tractable development of policies for autonomic systems from requirements through to code generation. This method is illustrated through an example showing how user formulated policies can be translated into a formal mode which can then be converted to code. The requirements-based programming method described provides faster, higher quality development and maintenance of autonomic systems based on user formulation of policies.Further, the systems, methods and apparatus described herein provide a way of analyzing policies for autonomic systems and facilities the generation of provably correct implementations automatically, which in turn provides reduced development time, reduced testing requirements, guarantees of correctness of the implementation with respect to the policies specified at the outset, and provides a higher degree of confidence that the policies are both complete and reasonable. The ability to specify the policy for the management of a system and then automatically generate an equivalent implementation greatly improves the quality of software, the survivability of future missions, in particular when the system will operate untended in very remote environments, and greatly reduces development lead times and costs.

Hinchey, Michael G.↗

DOE OSTI2022

Qualification of SAS4A/SASSYS-1 for Sodium-Cooled Fast Reactor Authorization and Licensing (Final CRADA Report)

This project focuses on assessment and qualification of the SAS4A/SASSYS-1 advanced reactor safety analysis code and its capacity to fulfill requirements associated with license/authorization of a sodium-cooled fast reactor (SFR). Specific objectives of this proposal include: development of a formal documentation requirements matrix that complies with a vendor’s NQA-1 program to identify needs for qualification documentation; completion of software methods qualification gap analysis to identify and close gaps in the verification and validation basis of the software; generation of an Acceptance Test Report to confirm compliance with the software requirements specification; and closure of gaps in Software Design Description (SDD) to assist with the eventual generation of a Modeling Licensing Topic Report (LTR).

21 SPECIFIC NUCLEAR REACTORS AND ASSOCIATED PLANTS↗

NASA NTRS2017

Advanced Software V&V for Civil Aviation and Autonomy

With the advances in high-computing platform (e.g., advanced graphical processing units or multi-core processors), computationally-intensive software techniques such as the ones used in artificial intelligence or formal methods have provided us with an opportunity to further increase safety in the aviation industry. Some of these techniques have facilitated building safety at design time, like in aircraft engines or software verification and validation, and others can introduce safety benefits during operations as long as we adapt our processes. In this talk, I will present how NASA is taking advantage of these new software techniques to build in safety at design time through advanced software verification and validation, which can be applied earlier and earlier in the design life cycle and thus help also reduce the cost of aviation assurance. I will then show how run-time techniques (such as runtime assurance or data analytics) offer us a chance to catch even more complex problems, even in the face of changing and unpredictable environments. These new techniques will be extremely useful as our aviation systems become more complex and more autonomous.

software assurance↗

NASA NTRS2000

An Overview of SAL

To become practical for assurance, automated formal methods must be made more scalable, automatic, and cost-effective. Such an increase in scope, scale, automation, and utility can be derived from an emphasis on a systematic separation of concerns during verification. SAL (Symbolic Analysis Laboratory) attempts to address these issues. It is a framework for combining different tools to calculate properties of concurrent systems. The heart of SAL is a language, developed in collaboration with Stanford, Berkeley, and Verimag for specifying concurrent systems in a compositional way. Our instantiation of the SAL framework augments PVS with tools for abstraction, invariant generation, program analysis (such as slicing), theorem proving, and model checking to separate concerns as well as calculate properties (i.e., perform, symbolic analysis) of concurrent systems. We. describe the motivation, the language, the tools, their integration in SAL/PAS, and some preliminary experience of their use.

Bensalem, Saddek↗

NASA NTRS2008

Web Based Tool for Mission Operations Scenarios

A conventional practice for spaceflight projects is to document scenarios in a monolithic Operations Concept document. Such documents can be hundreds of pages long and may require laborious updates. Software development practice utilizes scenarios in the form of smaller, individual use cases, which are often structured and managed using UML. We have developed a process and a web-based scenario tool that utilizes a similar philosophy of smaller, more compact scenarios (but avoids the formality of UML). The need for a scenario process and tool became apparent during the authors' work on a large astrophysics mission. It was noted that every phase of the Mission (e.g., formulation, design, verification and validation, and operations) looked back to scenarios to assess completeness of requirements and design. It was also noted that terminology needed to be clarified and structured to assure communication across all levels of the project. Attempts to manage, communicate, and evolve scenarios at all levels of a project using conventional tools (e.g., Excel) and methods (Scenario Working Group meetings) were not effective given limitations on budget and staffing. The objective of this paper is to document the scenario process and tool created to offer projects a low-cost capability to create, communicate, manage, and evolve scenarios throughout project development. The process and tool have the further benefit of allowing the association of requirements with particular scenarios, establishing and viewing relationships between higher- and lower-level scenarios, and the ability to place all scenarios in a shared context. The resulting structured set of scenarios is widely visible (using a web browser), easily updated, and can be searched according to various criteria including the level (e.g., Project, System, and Team) and Mission Phase. Scenarios are maintained in a web-accessible environment that provides a structured set of scenario fields and allows for maximum visibility across the project. One key aspect is that the tool was built for a scenario process that accounts for stakeholder input, review, comment, and concurrence. By creating well-designed opportunities for stakeholder input and concurrence and by making the scenario content easily accessible to all project personnel, we maximize the opportunities for stakeholders to both understand and agree on the concepts for how their mission is to be carried out.

Boyles, Carole A.↗

NASA NTRSDate not supplied

From Correct Specifications to Automatically Verified Implementations

Creating formally verified implementations of software can be time-consuming and difficult. This presentation details this process, and the attempts at easing the level of difficulty and human interaction. It begins by discussing the verification of an implementation of the Compact Position Reporting algorithm, which was an involved and manual process, and goes on to show the advances made since.

Mariano M. Moscato↗

NASA NTRS1995

An approach to verification and validation of a reliable multicasting protocol

This paper describes the process of implementing a complex communications protocol that provides reliable delivery of data in multicast-capable, packet-switching telecommunication networks. The protocol, called the Reliable Multicasting Protocol (RMP), was developed incrementally using a combination of formal and informal techniques in an attempt to ensure the correctness of its implementation. Our development process involved three concurrent activities: (1) the initial construction and incremental enhancement of a formal state model of the protocol machine; (2) the initial coding and incremental enhancement of the implementation; and (3) model-based testing of iterative implementations of the protocol. These activities were carried out by two separate teams: a design team and a V&V team. The design team built the first version of RMP with limited functionality to handle only nominal requirements of data delivery. In a series of iterative steps, the design team added new functionality to the implementation while the V&V team kept the state model in fidelity with the implementation. This was done by generating test cases based on suspected errant or off-nominal behaviors predicted by the current model. If the execution of a test was different between the model and implementation, then the differences helped identify inconsistencies between the model and implementation. The dialogue between both teams drove the co-evolution of the model and implementation. Testing served as the vehicle for keeping the model and implementation in fidelity with each other. This paper describes (1) our experiences in developing our process model; and (2) three example problems found during the development of RMP.

Callahan, John R.↗

NASA NTRS1994

An Approach to Verification and Validation of a Reliable Multicasting Protocol

This paper describes the process of implementing a complex communications protocol that provides reliable delivery of data in multicast-capable, packet-switching telecommunication networks. The protocol, called the Reliable Multicasting Protocol (RMP), was developed incrementally using a combination of formal and informal techniques in an attempt to ensure the correctness of its implementation. Our development process involved three concurrent activities: (1) the initial construction and incremental enhancement of a formal state model of the protocol machine; (2) the initial coding and incremental enhancement of the implementation; and (3) model-based testing of iterative implementations of the protocol. These activities were carried out by two separate teams: a design team and a V&V team. The design team built the first version of RMP with limited functionality to handle only nominal requirements of data delivery. In a series of iterative steps, the design team added new functionality to the implementation while the V&V team kept the state model in fidelity with the implementation. This was done by generating test cases based on suspected errant or offnominal behaviors predicted by the current model. If the execution of a test was different between the model and implementation, then the differences helped identify inconsistencies between the model and implementation. The dialogue between both teams drove the co-evolution of the model and implementation. Testing served as the vehicle for keeping the model and implementation in fidelity with each other. This paper describes (1) our experiences in developing our process model; and (2) three example problems found during the development of RMP.

Callahan, John R.↗

DOE OSTI2017

Model-based verification of I and C specifications - 184

In the field of nuclear I and C (Instrumentation and Control), the late detection of errors in the specifications and the design of I and C has a strong impact in terms of time and money. The early verification in the V cycle of I and C functions is a key issue to capture inconsistencies and errors before the implementation and on-site tests. EDF, in the framework of the collaborative project CONNEXION, has investigated methods based on simulation to formalize I and C requirements and to evaluate them at the conceptual and basic design phases. Behavioral models of the physic parts of the system and I and C functions, described as functional diagrams, are co-simulated in an integration environment based on the FMI (Functional Mockup Interface) standard. In this specific environment, test scenarios are performed on these models. These scenarios are defined on the basis of a high level model of the studied system that takes into account the states to cover (in normal and degraded situations). Requirements, once formalized, are translated into observers that evaluate their fulfillment during the simulations. Simulation logs are then a tool for the designer to analyze the causes of the possible non-fulfillment of requirements and to fix the corresponding errors in the specifications. The proposed methodology enables to detect errors in the specifications of I and C functions, to generate automatically functional test scenarios taking into account the coverage of the requirements and all the different operational modes of the system. (authors)

22 GENERAL STUDIES OF NUCLEAR REACTORS↗