Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “certification coding”

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 19 records
All sourcesNASA NTRSDOE OSTI
NASA NTRS2002

AutoBayes/CC: Combining Program Synthesis with Automatic Code Certification: System Description

Code certification is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be defined and formalized via properties, e.g., operator safety or memory safety. Its basic idea is to require code producers to provide formal proofs that their code satisfies these quality properties. The proofs serve as certificates which can be checked independently, by the code consumer or by certification authorities, e.g., the FAA. It is the idea underlying such approaches as proof-carrying code [6]. Code certification can be viewed as a more practical version of traditional Hoare-style program verification. The properties to be verified are fairly simple and regular so that it is often possible to use an automated theorem prover to automatically discharge all emerging proof obligations. Usually, however, the programmer must still splice auxiliary annotations (e.g., loop invariants) into the program to facilitate the proofs. For complex properties or larger programs this quickly becomes the limiting factor for the applicability of current certification approaches.

Whalen, Michael↗
NASA NTRS2004

Synthesizing Safety Conditions for Code Certification Using Meta-Level Programming

In code certification the code consumer publishes a safety policy and the code producer generates a proof that the produced code is in compliance with the published safety policy. In this paper, a novel viewpoint approach towards an implementational re-use oriented framework for code certification is taken. It adopts ingredients from Necula's approach for proof-carrying code, but in this work safety properties can be analyzed on a higher code level than assembly language instructions. It consists of three parts: (1) The specification language is extended to include generic pre-conditions that shall ensure safety at all states that can be reached during program execution. Actual safety requirements can be expressed by providing domain-specific definitions for the generic predicates which act as interface to the environment. (2) The Floyd-Hoare inductive assertion method is refined to obtain proof rules that allow the derivation of the proof obligations in terms of the generic safety predicates. (3) A meta-interpreter is designed and experimentally implemented that enables automatic synthesis of proof obligations for submitted programs by applying the modified Floyd-Hoare rules. The proof obligations have two separate conjuncts, one for functional correctness and another for the generic safety obligations. Proof of the generic obligations, having provided the actual safety definitions as context, ensures domain-specific safety of program execution in a particular environment and is simpler than full program verification.

Eusterbrock, Jutta↗
NASA NTRS2011

Software Certification - Coding, Code, and Coders

We describe a certification approach for software development that has been adopted at our organization. JPL develops robotic spacecraft for the exploration of the solar system. The flight software that controls these spacecraft is considered to be mission critical. We argue that the goal of a software certification process cannot be the development of "perfect" software, i.e., software that can be formally proven to be correct under all imaginable and unimaginable circumstances. More realistically, the goal is to guarantee a software development process that is conducted by knowledgeable engineers, who follow generally accepted procedures to control known risks, while meeting agreed upon standards of workmanship. We target three specific issues that must be addressed in such a certification procedure: the coding process, the code that is developed, and the skills of the coders. The coding process is driven by standards (e.g., a coding standard) and tools. The code is mechanically checked against the standard with the help of state-of-the-art static source code analyzers. The coders, finally, are certified in on-site training courses that include formal exams.

training↗
DOE OSTI2020

Certification Validation Libraries

“The code “Certificate Validation Libraries” provides the ability to validate x509 certificates in python using a simple library. These libraries validate certificates in 3 ways: 1) validation that certificate has not expired. 2) validation that certificate has not been revoked and 3) validation of certificate's digital signature. The benefits of this code is that one can properly validate x509 certificates, thus strengthening the security of systems using these libraries.”

Maerz, StefanA↗
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↗
DOE OSTI2018

Competitiveness Improvement Project Informational Workshop

This presentation was given at the Competitiveness Improvement Project (CIP) Informational Workshop on December 6, 2017. Topics covered during the workshop include an overview of the CIP, past projects, scoring criteria, technical support opportunities, certification body requirements, standards applicable to distributed wind generators, information on the National Electric Code, certification testing requirements, test site requirements, National Environmental Policy Act, design review, levelized cost of energy, procurement/contracting, project management/deliverables, and outreach materials.

17 WIND ENERGY↗
DOE OSTI2023

Development of Corrosion Resistant Coatings for Structural Materials for Liquid Fueled Molten Salts Reactors Applications (Final Report)

Current structural alloys, code certified for the MSRs temperature ranges, contain high levels of chromium, making them highly susceptible to molten halide salt corrosion. One potential solution to circumvent the need for code certification of novel alloys, which is expensive and time consuming, is to design claddings that will protect the underlying code certified materials from corrosion damage during operation. In this work, we examined the corrosion of Ni and Cu electroplated, Ni and CuNi weld overlay, Mo-laser clad, and carburized claddings on SS316H for use in molten salt reactor environments. After characterization of the cladded materials (Task 1), static corrosion tests were used to assess corrosion resistance of the claddings in typical molten fluoride salts (Task 2). The corrosion tests were performed in molten FLiNaK at 700°C up to 1000 hours. Pre- and post-corrosion Scanning Electron Microscopy (SEM), energy-dispersive-spectroscopy (EDS), Transmission Electron Microscopy (TEM), X-ray Diffraction (XRD) and glow-discharge-optical-emission-spectroscopy (GDOES) were performed on cladding cross-sections and surfaces to evaluate degradation. The Cu and Ni electroplated samples, as well as the carburized samples, showed excellent corrosion resistance relative to the bare SS316H. To assess high temperature cladding stability, ageing experiments were performed at temperatures up to 900 C in inert atmosphere for the electroplated and carburized samples and a diffusion model was developed to predict long term cladding behavior (Task 3). It was found that the Cu cladding was basically insensitive to the high temperature ageing, except for small secondary phases forming at the interface. On the other hand, the Ni electroplated cladding experienced significant interdiffusion. Nevertheless, the gain in corrosion resistance for a 100μm Ni electroplated cladding is phenomenal, with more than 50% reduction in chromium dissolution from the substrate material for the first 15 years of salt exposure at 700°C. To assess radiation resistance and phase stability, high-temperature 4MeV Ni heavy ion irradiation was performed across the cladding/substrate interface up to 50 displacement-per-atom (DPA) at 500°C and 700°C to assess the phase stability and irradiation behaviors of the electroplated systems (Task 4). The Ni and Cu electroplated systems did not experience void swelling at the contrary to the SS316H substrate due to their nanocrystalline nature. Some level of recrystallization was observed in the cladding, as well as radiation induced segregation and enhanced diffusion. The interface acted as a potent sink for point defects with the presence of a void denuded zone. The mechanical properties of the claddings were assessed using thermal shock, micro-indentation, nano-indentation, and four-point bend testing experiments (Task 5). These experiments were performed on the claddings in as-received, corroded, irradiated, and thermally aged states to determine the effects of typical molten salt reactor environments on cladding integrity. No significant mass loss was observed after repeated thermal shocks. While the electroplated samples softened after high-temperature ageing, irradiation hardening compensate this effect, such that there is little different with the as-received materials. The results of these experiments suggest that the electroplated (copper/nickel) show the greatest promise for application in molten salt reactor development. These claddings prevented any chromium dissolution from occurring during the static corrosion experiments. Additionally, they demonstrated favorable properties for high temperature diffusion, phase stability, interfacial mechanical properties, and irradiation resistance. Weld-overlay cladding are also of great interest and could reach properties similar to the electroplated samples upon optimization (especially with multiple weld passes). The carburized SS316H showed excellent behavior as well, but more work needs to be done to assess their long-term stability. Finally, the Mo-laser clad system was not pursued further due to the manufacturing challenges. It is also worth noting that the Ni cladding systems should behave relatively well in terms of weldability since the Ni-weld overlay microstructure and associated corrosion rate are sound. While the NiCu weld-overlay has even lower corrosion rates than the Ni-weld overlay, more studies on welding of Cu-electroplated systems are necessary since Cu clusters are known to embrittle steels.

36 MATERIALS SCIENCE↗
NASA NTRS2009

Proceedings of the Third International Workshop on Proof-Carrying Code and Software Certification

This NASA conference publication contains the proceedings of the Third International Workshop on Proof-Carrying Code and Software Certification, held as part of LICS in Los Angeles, CA, USA, on August 15, 2009. Software certification demonstrates the reliability, safety, or security of software systems in such a way that it can be checked by an independent authority with minimal trust in the techniques and tools used in the certification process itself. It can build on existing validation and verification (V&V) techniques but introduces the notion of explicit software certificates, Vvilich contain all the information necessary for an independent assessment of the demonstrated properties. One such example is proof-carrying code (PCC) which is an important and distinctive approach to enhancing trust in programs. It provides a practical framework for independent assurance of program behavior; especially where source code is not available, or the code author and user are unknown to each other. The workshop wiII address theoretical foundations of logic-based software certification as well as practical examples and work on alternative application domains. Here "certificate" is construed broadly, to include not just mathematical derivations and proofs but also safety and assurance cases, or any fonnal evidence that supports the semantic analysis of programs: that is, evidence about an intrinsic property of code and its behaviour that can be independently checked by any user, intermediary, or third party. These guarantees mean that software certificates raise trust in the code itself, distinct from and complementary to any existing trust in the creator of the code, the process used to produce it, or its distributor. In addition to the contributed talks, the workshop featured two invited talks, by Kelly Hayhurst and Andrew Appel. The PCC 2009 website can be found at http://ti.arc.nasa.gov /event/pcc 091.

Ewen, Denney, W.↗
DOE OSTI2017

Corrosion of Structural Materials for Advanced Supercritical Carbon- Dioxide Brayton Cycle

The supercritical carbon-dioxide (referred to as SC-CO 2 hereon) Brayton cycle is being considered for power conversion systems for a number of nuclear reactor concepts, including the sodium fast reactor (SFR), fluoride saltcooled high temperature reactor (FHR), and high temperature gas reactor (HTGR), and several types of small modular reactors (SMR). The SC-CO 2 direct cycle gas fast reactor has also been recently proposed. The SC-CO 2 Brayton cycle (discussed in Chapter 1) provides higher efficiencies compared to the Rankine steam cycle due to less compression work stemming from higher SC-CO 2 densities, and allows for smaller components size, fewer components, and simpler cycle layout. For example, in the case of a SFR using a SC-CO 2 Brayton cycle instead of a steam cycle would also eliminate the possibility of sodium-water interactions. The SC-CO 2 cycle has a higher efficiency than the helium Brayton cycle, with the additional advantage of being able to operate at lower temperatures and higher pressures. In general, the SC-CO 2 Brayton cycle is well-suited for any type of nuclear reactor (including SMR) with core outlet temperature above ~ 500°C in either direct or indirect versions. In all the above applications, materials corrosion in high temperature SC-CO 2 is an important consideration, given their expected lifetimes of 20 years or longer. Our discussions with National Laboratories and private industry early on in this project indicated materials corrosion to be one of the significant gaps in the implementation of SC-CO 2 Brayton cycle. Corrosion can lead to a loss of effective load-bearing wall thickness of a component and can potentially lead to the generation of oxide particulate debris which can lead to three-body wear in turbomachinery components. Another environmental degradation effect that is rather unique to CO 2 environment is the possibility for simultaneous occurrence of carburization during oxidation of the material. Carburization can potentially lead to embrittlement of structural alloys in SC-CO 2 Brayton cycle. An important consideration in regards to corrosion is that the temperatures can vary widely across the various sections of the SC-CO 2 Brayton cycle, from room temperature to 750°C, with even higher temperatures being desirable for higher efficiencies. Thus the extent of corrosion and corrosion mechanisms in various components and SC-CO 2 Brayton cycle will be different, requiring a judicious selection of materials for different sections of the cycle. The goal of this project was to address materials corrosion-related challenges, identify appropriate materials, and advance the body of scientific knowledge in the area of high temperature SC-CO 2 corrosion. The focus was on corrosion of materials in SC-CO 2 environment in the temperature range of 450°C to 750°C at a pressure of 2900 psi for exposure duration for up to 1000 hours. The Table below lists the materials tested in the project. The materials were selected based on their high temperature strength, their code certification status, commercial availabilities, and their prior or current usage in the nuclear reactor industry. Additionally, pure Fe, Fe-12%Cr, and Ni-22%Cr were investigated as simple model materials to more clearly understand corrosion mechanisms. This first phase of the project involved testing in research grade SC-CO 2 (99.999% purity). Specially designed autoclaves with high fidelity temperature, pressure, and flow control capabilities were built or modified for this project.

36 MATERIALS SCIENCE↗
NASA NTRS1990

The aerospace plane design challenge: Credible computational fluid dynamics results

Computational fluid dynamics (CFD) is necessary in the design processes of all current aerospace plane programs. Single-stage-to-orbit (STTO) aerospace planes with air-breathing supersonic combustion are going to be largely designed by means of CFD. The challenge of the aerospace plane design is to provide credible CFD results to work from, to assess the risk associated with the use of those results, and to certify CFD codes that produce credible results. To establish the credibility of CFD results used in design, the following topics are discussed: CFD validation vis-a-vis measurable fluid dynamics (MFD) validation; responsibility for credibility; credibility requirement; and a guide for establishing credibility. Quantification of CFD uncertainties helps to assess success risk and safety risks, and the development of CFD as a design tool requires code certification. This challenge is managed by designing the designers to use CFD effectively, by ensuring quality control, and by balancing the design process. For designing the designers, the following topics are discussed: how CFD design technology is developed; the reasons Japanese companies, by and large, produce goods of higher quality than the U.S. counterparts; teamwork as a new way of doing business; and how ideas, quality, and teaming can be brought together. Quality control for reducing the loss imparted to the society begins with the quality of the CFD results used in the design process, and balancing the design process means using a judicious balance of CFD and MFD.

Mehta, Unmeel B.↗
DOE OSTI2016

Corrosion of Candidate Materials in Molten FLiBe Salt for Fluoride-Salt-Cooled High-Temperature Reactor (FHR)

Molten fluoride salts have attracted considerable attention because of their desirable thermophysical properties that lead to superior heat transfer. Recently, fluoride salts are being considered as coolants in the fluoride salt-cooled high temperature reactors (FHRs). The successes of the molten salt reactor experiment (MSRE) program in 1950's-70's at Oak Ridge National Laboratory (ORNL) has also driven the pursuit of molten salt nuclear reactor as one of the lead next generation nuclear reactor concepts. Unlike MSRE where the uranium fuel was dissolved in the molten fluoride salt, the FHR concept is expected to use molten salt (2LiF-BeF{sub 2}, FLiBe) only as coolant in conjunction with solid TRISO fuel particles immersed in the molten salt. One of the important challenges in FHR development is corrosion of structural materials in high-temperature molten 2LiF-BeF{sub 2} (FLiBe) salt. Currently, 316 stainless steel (nominal composition: Fe-12Ni-17Cr-2.5Mo-1Si-2Mn-0.03C) and Hastelloy N (nominal composition: Ni-7Cr-16Mo-5Fe-1Si-0.8Mn) are deemed as promising candidate alloys for the construction of some of the structural components of FHR. 316 stainless steel is ASME code certified for high temperatures (up to 760 deg. C) applications. Hastelloy N has been shown to have outstanding corrosion resistance in molten FLiBe but present code certification data limit the use of this alloy to only about 704 deg. C. Modifications of Hastelloy N with higher creep strength are presently being developed at ORNL. Other materials such graphite, SiC/SiCf and C/Cf composites, are also considered for structural applications in the FHR. The presence of these multiple materials in a molten FLiBe salt medium can further exacerbate and complicate corrosion effects. Therefore, it is necessary to understand the corrosion behavior of these materials in molten FLiBe salt. The corrosion behavior of Hastelloy N, 316 stainless steel, and CVD SiC and two types of SiC-SiC{sub f} composites have been tested in molten FLiBe salt at 700 deg. C. When tested in metal-lined crucibles both Hastelloy N and 316 stainless steel showed very good corrosion resistance. Samples tested in graphite crucibles showed greater propensity for corrosion and carburization was observed in the near surface regions of the alloys. CVD SiC showed outstanding corrosion resistance. However, the two SiC-SiC{sub f} composites exhibited corrosion attack implying that the manufacturing process may play a role in the corrosion of these composites. (authors)

21 SPECIFIC NUCLEAR REACTORS AND ASSOCIATED PLANTS↗
NASA NTRS2009

Deriving Safety Cases for the Formal Safety Certification of Automatically Generated Code

We present an approach to systematically derive safety cases for automatically generated code from information collected during a formal, Hoare-style safety certification of the code. This safety case makes explicit the formal and informal reasoning principles, and reveals the top-level assumptions and external dependencies that must be taken into account; however, the evidence still comes from the formal safety proofs. It uses a generic goal-based argument that is instantiated with respect to the certified safety property (i.e., safety claims) and the program. This will be combined with a complementary safety case that argues the safety of the framework itself, in particular the correctness of the Hoare rules with respect to the safety property and the trustworthiness of the certification system and its individual components. Keywords: Automated code generation, Hoare logic, formal code certification, safety case, Goal Structuring Notation.

Basir, Nurlida↗
NASA NTRS1994

Role of Wind Tunnels and Computer Codes in the Certification and Qualification of Rotorcraft for Flight in Forecast Icing

The cost and time to certify or qualify a rotorcraft for flight in forecast icing has been a major impediment to the development of ice protection systems for helicopter rotors. Development and flight test programs for those aircraft that have achieved certification or qualification for flight in icing conditions have taken many years, and the costs have been very high. NASA, Sikorsky, and others have been conducting research into alternative means for providing information for the development of ice protection systems, and subsequent flight testing to substantiate the air-worthiness of a rotor ice protection system. Model rotor icing tests conducted in 1989 and 1993 have provided a data base for correlation of codes, and for the validation of wind tunnel icing test techniques. This paper summarizes this research, showing test and correlation trends as functions of cloud liquid water content, rotor lift, flight speed, and ambient temperature. Molds were made of several of the ice formations on the rotor blades. These molds were used to form simulated ice on the rotor blades, and the blades were then tested in a wind tunnel to determine flight performance characteristics. These simulated-ice rotor performance tests are discussed in the paper. The levels of correlation achieved and the role of these tools (codes and wind tunnel tests) in flight test planning, testing, and extension of flight data to the limits of the icing envelope are discussed. The potential application of simulated ice, the NASA LEWICE computer, the Sikorsky Generalized Rotor Performance aerodynamic computer code, and NASA Icing Research Tunnel rotor tests in a rotorcraft certification or qualification program are also discussed. The correlation of these computer codes with tunnel test data is presented, and a procedure or process to use these methods as part of a certification or qualification program is introduced.

Flemming, Robert J.↗
NASA NTRS2011

Cassini Solstice Mission Maneuver Experience: Year One

The Cassini-Huygens spacecraft began its four-year Prime Mission to study Saturn's system in July 2004. Two tour extensions followed: a two-year Equinox Mission beginning in July 2008 and a seven-year Solstice Mission starting in September 2010. This paper highlights Cassini maneuver activities from June 2010 through June 2011, covering the transition from the Equinox to Solstice Mission. This interval included 38 scheduled maneuvers, nine targeted Titan flybys, three targeted Enceladus flybys, and one close Rhea flyby. In addition, beyond the demanding nominal navigation schedule, numerous unforeseen challenges further complicated maneuver operations. These challenges will be discussed in detail.

training↗
NASA NTRS2005

Software Certification and Software Certificate Management Systems

Incremental certification and re-certification of code as it is developed and modified is a prerequisite for applying modem, evolutionary development processes, which are especially relevant for NASA. For example, the Columbia Accident Investigation Board (CAIB) report 121 concluded there is "the need for improved and uniform statistical sampling, audit, and certification processes". Also, re-certification time has been a limiting factor in making changes to Space Shuttle code close to launch time. This is likely to be an even bigger problem with the rapid turnaround required in developing NASA s replacement for the Space Shuttle, the Crew Exploration Vehicle (CEV). Hence, intelligent development processes are needed which place certification at the center of development. If certification tools provide useful information, such as estimated time and effort, they are more likely to be adopted. The ultimate impact of such a tool will be reduced effort and increased reliability.

Denney, Ewen↗