Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “PVS”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

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

At least 91 records · Page 5
All sourcesNASA NTRSDOE OSTI
NASA NTRSDate not supplied

A Formal Verification Framework for Runtime Assurance

The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality, allowing for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

Runtime assurance↗
DOE OSTI2025

Analysis of AC-DC Converters for Grid-tied High Temperature Steam Electrolysis Systems

Grid-tied HTSE systems have the prospects to produce clean hydrogen enabling power and broad energy systems decarbonization. Most commercially available power electronic converter systems (PECS) are designed for batteries, solar PVs, wind, and other well-established renewable energy resources. Standards (such as IEEE 1547, UL 1741, CA Rule-21, HI Rule14) exist for PECS used for renewable energy systems such as battery storage and solar PVs. However, those that consider the dynamic behavior of HTSEs and that can be used for large-scale H2 systems are yet to be developed. This paper investigates the performance of these PECS for the HTSE application that are set up at the Idaho National Laboratory for hydrogen production testing, research and development. In particular, the performance analysis of two grid-tied PECS (A and B) is conducted for a 100 kW solid oxide HTSE system. System A consists of 6 units of 30kW MOSFET-switched bidirectional AC-DC rectifier while system B has a single unit of 150kW thyristor-switched AC-DC rectifier. Both systems are connected to the HTSE stacks via a DC-DC converter. Different operational conditions of the HTSE system are tested to analyze the dynamic response of the HTSE’s PECS. The experimental results show the need to develop advanced control strategies for PECS that incorporates the dynamics of HTSE systems for improved performance.

High temperature steam electrolysis↗
NASA NTRSDate not supplied

Formal Verification of the Interaction Between Semi-Algebraic Sets and Real Analytic Functions

Semi-algebraic sets and real analytic functions are fundamental concepts in Real Algebraic Geometry and Real Analysis, respectively. These concepts interact in the study of Differential Equations, where the real analytic solution to a differential equation is known to enter or exit a semi-algebraic set in a predicable way. Motivated to enhance the capability to reason about differential equations in the Prototype Verification System (PVS), a formalization of multivariate polynomials, semi-algebraic sets, and real analytic functions is developed. The favorable way that a real analytic function enters and exits a semi-algebraic set is proven. It is further shown that if the function is assumed to be smooth, a slightly weaker assumption than real analytic, these favorable interactions with semi-algebraic sets may fail.

Real analytic functions↗
NASA NTRSDate not supplied

Applying Formal Methods to Safety-Critical Systems

How do you know a proof is correct? Traditionally, mathematical proofs are socially verified – at least one human, following a set of implicit rules of natural language and logic, determines if the proof is believable. If the proof becomes overly tedious and/or is essential to some safety- or mission-critical application, it becomes necessary to determine the soundness to a higher standard. 'Formal methods' refer to mathematically rigorous techniques and tools that enable specification, design, and verification of hardware and software systems. The specification used in formal methods are statements in a mathematical logic while the formal verifications are deductions in that logic. Formal methods can be difficult or time/resource intensive, but offer a higher level of assurance than standard verification through testing or handwritten proofs. This talk will introduce formal methods, motivated by applications of interest to NASA, including uncrewed aircraft operations in the national airspace, urban air environments, and wildfire areas. The audience will be given a crash course in mechanically verified proofs in the Prototype Verification System (PVS), an interactive theorem prover.

Formal Methods↗
NASA NTRSDate not supplied

A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts

The NASA DAIDALUS library provides formal definitions for Detect-and-Avoid avionics concepts such as when an aircraft is well-clear with respect to the surrounding air traffic, i.e., it does not operate in such proximity to create a collision hazard. While several properties are proven correct for DAIDALUS assuming ideal real number arithmetic, an actual implementation that uses floating-point numbers may behave unexpectedly because of round-off errors and run-time exceptions. This paper presents an experience report on the application of a formal methods toolchain to extract and verify floating-point C code from a real-valued specification of the well-clear module of DAIDALUS. This toolchain comprises the PVS theorem prover, the PRECiSA floating-point analyzer and code generator, and the Frama-C analysis suite. The generated code is automatically instrumented to detect when the control flow of the floating-point program may diverge from the ideal real number specification, and it is annotated with contracts that state the maximum accumulated round-off error. The absence of overflows is also formally verified for the generated code. In order to apply the toolchain to an industrial case study such as DAIDALUS, a formally verified pre-processing of the input specification is performed, which includes a program slicing and several semantic-preserving simplifications.

Program verification↗
DOE OSTI2026

Demonstration of GaAs-Based Photovoltaics on Acoustically Spalled Surfaces Grown by MOCVD

This study demonstrates the potential of sonic lift-off (SLO) technology for repeatable substrate reuse in gallium arsenide (GaAs)–based photovoltaics (PVs), offering a pathway toward cost effective production for terrestrial PV applications. Single-junction GaAs solar cells fabricated on acoustically spalled substrates achieved performance metrics comparable with those grown on standard commercial substrates, exhibiting short-circuit current densities (J sc ) of approximately 26.2–26.4 mA/cm 2 , open-circuit voltages (V oc ) around 1001 mV, fill factors (FFs) of 84%, and AM1.5G efficiencies near 22%. These results confirm that one reuse cycle can be realized without a performance penalty, offering a direct pathway to reducing substrate cost in fabrication. Furthermore, subsequent reuse of the substrates highlighted critical challenges, as devices fabricated from reused substrates showed significant degradation in performance (J sc of 15.5 mA/cm 2 , V oc of 748 mV, FF of 72%, and efficiency of 8%), primarily due to degradation of the epitaxial structure resulting from repeated spalling cycles.

Acoustic Spalling↗
DOE OSTI2025

Forecast for a growth-rate measurement using peculiar velocities from LSST supernovae

We investigate whether the cosmic growth-rate parameter fσ 8 can be measured using peculiar velocities (PVs) derived from type Ia supernovae (SNe Ia) in the Vera C. Rubin Observatory’s Legacy Survey of Space and Time (LSST). We produced simulations of different SN types using a realistic LSST observing strategy that incorporated noise, a photometric detection from the difference-image analysis (DIA) pipeline, and a PV field modeled from the Uchuu universe machine simulations. We tested three different observational scenarios that ranged from ideal conditions with spectroscopic host galaxy redshifts and spectroscopic SN typing to realistic photometric typing that resulted in a contamination with non-Ia SNe. Using a maximum likelihood technique, we showed that the LSST can measure fσ 8 with a precision of 10% in the redshift range 0.02 < z < 0.14 for our most realistic scenario. In three tomographic bins, the LSST will be able to constrain the growth-rate parameter with errors below 18% up to redshift z = 0.14. We also tested the contamination effect on the maximum likelihood method and found that for a contamination fraction below ∼2%, we recovered unbiased measurements. The results of this analysis highlight that the LSST SN sample is expected to complement traditional redshift-space distortion measurements at high redshift. This will provide a novel avenue for testing general relativity and different dark energy models.

Rosselli, D↗
DOE OSTI2026

Safe Deep Reinforcement Learning for Active Distribution System Model Predictive Control with EVs and DERs

The temporal and spatial mismatch between PV generation and electric vehicle (EV) charging and discharging may cause voltage violations in active distribution networks. Despite the widespread use of deep reinforcement learning (DRL) in power system optimization and control, it lacks guarantees on constraint satisfaction during both training and deployment. This paper proposes a Lagrangian-based safe DRL approach for model predictive control (MPC) of active distribution systems with large-scale integration of PVs, EVs, and energy storage systems (ESSs). A Transformer-LSTM time-series model is proposed to forecast EV charging demand, which is then formulated as a constraint to ensure charging requirements are met. Using this prediction, a Lagrangian-based safe soft actor-critic (SAC) framework is developed for real-time control in a three-phase unbalanced distribution system, enforcing voltage safety constraints while optimizing the cumulative net reward. By integrating the forecasting model with multi-period constraints, the proposed framework jointly coordinates PV systems, EV charging and discharging, and ESS scheduling within the MPC horizon. Numerical experiments on a modified IEEE 123-bus system with real-world data show that, under a high PV penetration scenario, the proposed method increases the net reward by 30.74% and reduces average voltage violations from 0.0011 p.u. to 0.0002 p.u. compared with standard SAC. Compared with the optimal power flow (OPF) approach, it achieves similar voltage security while yielding lower line losses. It also maintains real-time control capability, reducing operation latency to 53.21 ms per 15-minute control interval. The proposed method remains effective under varying PV/EV penetrations and load conditions.

24 POWER TRANSMISSION AND DISTRIBUTION↗
DOE OSTI2024

Modeling Diurnal and Annual Ethylene Generation from Solar-Driven Electrochemical CO 2 Reduction Devices

Integrated solar fuels devices for CO 2 reduction (CO 2 R) are a promising technology class towards achieving net-negative carbon emissions. Designing integrated CO 2 R solar fuels devices requires careful co-design of electrochemical and photovoltaic components as well as consideration of the diurnal and seasonal effects of solar irradiance, temperature, and other meteorological factors expected for ‘on-sun’ deployment. Here, using a photovoltaic-electrochemical (PV-EC) platform, we developed a temperature and potential-dependent diurnal and annual model using experimental CO 2 R performance of Cu-based electrocatalysts, local meteorological data from the National Solar Radiation Database (NSRD), and modeled performance of commercial c-Si PVs. We simulated diurnal product outputs with and without the effects of ambient temperature to determine gaseous product temperature sensitivity. From these outputs, we observed seasonal variation in gaseous product generation, with up to two-fold increases in ethylene productivity between the Winter and Summer, analyzed the consequences of dynamic cloud coverage, and identified periods where device cooling/heating mechanisms could be implemented to maximize ethylene generation. Finally, we modeled the annual ethylene generation for a scaled 1 MW solar farm at three different locations (Beijing, CN; Sydney, AUS; Barstow, CA) to determine the consequences of local meteorological climates on PV-EC CO 2 R product output, recording a maximum ethylene output of 18.5 tonne/yr at Barstow. Overall, this model presents a critical tool for streamlining the translation of experimental solar-driven electrochemical research to real-world implementation.

Yap, Kyra M. K.↗
DOE OSTI2024

Dynamic Temporal Graph Sequence Data for Resilience-Oriented Distribution Network Reconfiguration

This dataset comprises temporal dynamic graph sequences generated from power grid simulations focused on grid reconfiguration to enhance resilience. The simulations model failure propagation under varying conditions, with nodes assigned distinct failure probabilities. For each time step, the dataset captures the evolution of node states (functional or failed) and features critical to grid operations, such as pv_output, load_profile, load_dispatch, dg_output, loss, and voltage. Node types include sources, normal loads, and nodes with specific equipment like PVs, micro turbines, or shunt capacitors. The dataset is structured to support the training of dynamic graph neural networks, facilitating research on node feature prediction and edge dynamics under failure scenarios. Three distinct configurations are included, providing a robust foundation for modeling power grid resilience.

29 ENERGY PLANNING, POLICY, AND ECONOMY↗
DOE OSTI2024

Halide Perovskite Solar Photovoltaics

Technological progress in photovoltaic (PV) technologies provides hope that a comprehensive and desperately needed decarbonization of the energy sector is possible. Commercially successful PV technologies based predominantly on silicon wafer technology are reliable and cost-effective, but remain capital- and carbon-intensive. In this context, emerging PV technologies, such as metal-halide perovskites (MHPs), could further catalyze the energy transition by providing technological opportunities for even lower-cost, mass-producible, high-efficiency solar cells with a significantly reduced "carbon footprint." This themed issue of MRS Bulletin on "Halide perovskite solar photovoltaics summarizes the current state of the art, challenges, and opportunities of perovskite photovoltaics with contributions and perspectives from six expert teams worldwide. The topics covered provide a status update on perovskite PV, remaining hurdles to their deployment, and challenges to realizing the potential of this technology to impact climate goals. Articles in this collection address scalability of perovskite PV and prospects for industrial manufacturing; perovskite PV as an add-on technology on top of commercial silicon PV; environmental and sustainability considerations; and durability and reliability considerations. Further considerations include prospects of automation, coupled to artificial intelligence and machine learning, for accelerating material-based solutions to these outstanding challenges including the possibilities of discovering new absorber and device component materials to enable success and ultimately deployment of these next-generation PVs.

metal-halide perovskites↗
DOE OSTI2026

The Interactions Between Shading and Organic Fertilizer Application on Dry-farmed Tomato Grown Between Photovoltaic Panels

Agrivoltaic systems are mixed systems of solar photovoltaic (PV) panels and agricultural production, where shade from the panels can result in lower evapotranspiration for crops, which is of particular interest for dryland agriculture. Dry-farmed tomato (Solanum lycopersicum) production in the Willamette Valley of Oregon has lower total yields and higher rates of blossom-end rot (BER) than irrigated tomato production, resulting in reduced marketable yields. To determine how dry-farmed ‘Early Girl’ tomato performed in an agrivoltaics system, a trial was conducted at the Valley Creek Solar Project (Salem, OR, USA) in 2020, using three different amendment treatments and three levels of shading from the panels. Amendment treatments were 0N (receiving no fertilizer), 84N (receiving 84 kg·ha −1 N), and 168N (receiving 168 kg·ha −1 N), applied as processed chicken manure. Plants were estimated to receive an irradiance factor of 30%, 76%, and 89% for full-shade, partial-shade, and full-sun treatments respectively. There was an interaction between amendment treatments and shading treatments in their effects on unblemished yield (yield of fruit without BER or sunscald). The optimum fertilizer application for full-shade and partial-shade rows was 84N, the optimum for full-sun rows was 0N. Fertilizing these rows at these rates resulted in an unblemished yield for the aisle of 11.1 t·ha −1 , which was lower than unblemished yields reported in previous experiments and trials in open fields. However, these results are from a single location and a single year, and other solar sites may behave more similar to open-field conditions. Shading from the panels increased average fruit weight and decreased incidence of BER and sunscald, suggesting that crops were less drought stressed. This resulted in similar unblemished yields for the full-shade and full-sun plots at 84N and 168N. Applying fertilizer resulted in higher total yields, smaller average fruit weight, increased BER incidence, and decreased sunscald incidence. The results suggest a possible synergy between dry-farmed tomato production and agrivoltaics, although several concerns remain, including difficulties managing the vegetation under panels, rules restricting PVs on high-value agricultural soils, and the possibility of soil compaction during PV installation.

14 SOLAR ENERGY↗
NASA NTRS1977

Dynamic response of some tentative compliant wall structures to convected turbulence fields

Some tentative compliant wall structures designed for possible skin friction drag reduction are investigated. Among the structural models considered is a ribbed membrane backed by polyurethane or PVS plastisol. This model is simplified as a beam placed on a viscoelastic foundation as well as on a set of evenly spaced supports. The total length of the beam may be either finite or infinite, and the supports may be either rigid or elastic. Another structural model considered is a membrane mounted over a series of pretensioned wires, also evenly spaced, and the entire membrane is backed by an air cavity. The forcing pressure field is idealized as a frozen random pattern convected downstream at a characteristic velocity. The results are given in terms of the frequency response functions of the system, the spectral density of the structural motion, and the spectral density of the boundary layer pressure including the effect of structural motion. These results are used in a parametric study of structural configurations capable of generating favorable wave lengths, wave amplitudes, and wave speeds in the structural motion for potential drag reduction.

Nijim, H. H.↗
NASA NTRS1995

The formal verification used for the AAMP5 and AAMP-FV

The main goal of the project was two-fold: First, to investigate the feasibility of formally specifying and verifying a complex commercial microprocessor that was not expressly designed for formal verification. Second, to explore effective ways to transfer the technology to an industrial setting. The choice of the AAMP5 satisfied the first goal since the AAMP5 was not designed for formal verification, but to provide a more than threefold performance improvement while remaining object-code-compatible with the earlier AAMP2, which is used in numerous avionics applications, including the Boeing 737, 747, 757, and 767. To satisfy the technology transfer objective, we had to develop a suitable verification methodology and a formal infrastructure to make the technology usable by practicing engineers. This infrastructure includes techniques for decomposing the microcompressor verification problem into a st of verification conditions that the engineers can formulate and strategies to automate the proof of the verification conditions. The development of the infrastructure was one of the key accomplishments of the project. Most of the infrastructure and methodology are general enough to be reused for other microprocessors, certainly in the verification of another member of the AAMP family. This methodology was used to formally specify the entire microarchitecture and more than half of the instruction set and to verify a core set of eleven AAMP5 instructions representative of several instruction classes. However, the methodology and the formal machinery developed are adequate to cover most of the remaining AAMP5 instructions. Although PVS was the vehicle of the experiment, the methodology is applicable to other sufficiently powerful theorem provers.

Srivas, Mandayam↗
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 NTRS1998

A Formal Model of Partitioning for Integrated Modular Avionics

The aviation industry is gradually moving toward the use of integrated modular avionics (IMA) for civilian transport aircraft. An important concern for IMA is ensuring that applications are safely partitioned so they cannot interfere with one another. We have investigated the problem of ensuring safe partitioning and logical non-interference among separate applications running on a shared Avionics Computer Resource (ACR). This research was performed in the context of ongoing standardization efforts, in particular, the work of RTCA committee SC-182, and the recently completed ARINC 653 application executive (APEX) interface standard. We have developed a formal model of partitioning suitable for evaluating the design of an ACR. The model draws from the mathematical modeling techniques developed by the computer security community. This report presents a formulation of partitioning requirements expressed first using conventional mathematical notation, then formalized using the language of SRI'S Prototype Verification System (PVS). The approach is demonstrated on three candidate designs, each an abstraction of features found in real systems.

DiVito, Ben L.↗
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↗