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 73 records · Page 4
All sourcesNASA NTRSDOE OSTI
DOE OSTI2025

A Two-Stage Approach for PV Inverter Engagement in Power Factor Correction and Voltage Regulation

The rapid integration of distributed energy resources, like solar photovoltaics (PVs), can lead to overvolt-age challenges due to reverse power flow and a noticeable decrease in power factor at the substation interface. While existing literature extensively explores utilizing smart inverter capabilities for reactive power flexibility using a volt-var curve (VVC), obtaining time-varying operating points of such curves in real-time is challenging due to computational demands and communication requirements. Similarly, employing optimization-based approaches for reactive power control and active voltage regulation in large-scale distribution feeders is difficult due to the complexity of the problem and the challenges in effectively engaging customer-owned resources. This paper proposes a two-stage strategy to harness smart inverters for reactive power support. The first stage formulates short-term planning by optimally designing VVCs (on a daily or hourly basis) for large-scale solar PVs based on projected system needs and communicating optimal curves to smart inverters in advance. Subsequently, the second stage employs a transactive-based method to involve customer-owned PVs for reactive power support, effectively enhancing overall system performance and addressing real-time demands. In conclusion, the efficacy of this approach will be demonstrated using real-world distribution circuits provided by Vermont Electric Power Company (VELCO) and Vermont Electric Cooperative (VEC).

Poudel, Shiva [Pacific Northwest National Laborato↗
NASA NTRS2020

Formal Verification of a Solution to the n-Queens Problem

This report describes a formal verification of a concise algorithm that computes a solution to the n-Queens problem for all natural numbers n, such that n > 3. The formal proof of the algorithm is completed in the Prototype Verification System (PVS) theorem prover. This verification effort serves two purposes. First, it is presented as a pedagogical example for learning a theorem prover, such as PVS, and second, as a candidate benchmark for comparing other formal methods tools to PVS.

Mahyar R Malekpour↗
DOE OSTI2024

Triple Effect Economics: How Do Electric Vehicles, Solar Photovoltaics, and Work-from-Home Transform Household Electricity Cost?

Solutions for deep decarbonization need to be affordable as well as sustainable to garner widespread adoption. The past two decades have seen the introduction of new technologies and paradigms such as electric vehicles (EVs), solar photovoltaics (PVs), and increased work-from-home (WFH), which impact a household's overall energy consumption and cost in different ways. However, much attention has not been paid to explore the joint impact these technologies have on a household's electricity cost burden. Leveraging the 2020 Residential Energy Consumption Survey (RECS), this study presents an integrated model to unravel the extent to which the bundled adoption of EV-PV and stay-at-home decisions impact the total electricity cost of households. National level RECS data revealed that, compared to the baseline (i.e., households that did not own any of these technologies), households that own EVs, PVs, and engage in WFH observed a 13.5% decline in their electricity bills, despite a 25% increase in electricity consumption. The model results indicated that bundled adoption of EVs-PVs reduces electricity costs more significantly for a household, compared to the increased costs imposed by more household members staying at home. This holistic assessment presents an opportunity for decision makers to contextualize the changing energy costs and design effective strategies to foster a sustainable and cost saving mechanism. Policies such as bundled incentivization to motivate co-adoption, education about energy-management strategies, and add-on subsidies to adopt energy-efficient appliances, will not only accelerate decarbonization but increase household financial savings.

ADVANCED PROPULSION SYSTEMS,ENERGY PLANNING, POLIC↗
DOE OSTI2024

Metal Oxide vs Organic Semiconductor Charge Extraction Layers for Halide Perovskite Indoor Photovoltaics

Halide perovskite indoor photovoltaics (PVs) are highly promising to autonomously power the billions of microelectronic sensors in the emerging and disruptive technology of the Internet of Things (IoT). However, how the wide range of different types of hole extraction layers (HELs) impacts the indoor light harvesting of perovskite solar cells is still elusive, which hinders the material selection and industrial–scale fabrication of indoor perovskite photovoltaics. In the present study, new insights are provided regarding the judicial selection of HELs at the buried interface of halide perovskite indoor photovoltaics. This study unravels the detrimental and severe light–soaking effect of metal oxide transport layer–based PV devices under the indoor lighting effect for the first time, which then necessitates the interface passivation/engineering for their reliant performance. This is not a stringent criterion under 1 sun illumination. By systematically investigating the charge carrier dynamics and sequence of measurements from dark, light–soaked, interlayer–passivated device, the bulk and interface defects are decoupled and reveal the gradual defect passivation from shallow to deep level traps. Thus, the present study puts forward a useful design strategy to overcome the deleterious effect of metal oxide HELs and employ them in halide perovskite indoor PVs.

14 SOLAR ENERGY↗
DOE OSTI2024

Sustainability pathways for perovskite photovoltaics

Solar energy is the fastest-growing source of electricity generation globally. As deployment increases, photovoltaic (PV) panels need to be produced sustainably. Therefore, the resource utilization rate and the rate at which those resources become available in the environment must be in equilibrium while maintaining the well-being of people and nature. Metal halide perovskite (MHP) semiconductors could revolutionize PV technology due to high efficiency, readily available/accessible materials and low-cost production. Here we outline how MHP-PV panels could scale a sustainable supply chain while appreciably contributing to a global renewable energy transition. Further, we evaluate the critical material concerns, embodied energy, carbon impacts and circular supply chain processes of MHP-PVs. The research community is in an influential position to prioritize research efforts in reliability, recycling and remanufacturing to make MHP-PVs one of the most sustainable energy sources on the market.

14 SOLAR ENERGY↗
DOE OSTI2024

Benchmark High-Fidelity EMT Models for Power Grid with PV Plants

In recent times electromagnetic transient (EMT) modeling tools have been identified as one of the most important requirements in replicating, analyzing, and investigating the dynamics of the power grid with photovoltaic (PV) plants. However, there are no benchmark models for power grid with PVs to investigate emerging challenges with higher penetration of PVs (like trips and momentary cessations during faults from a region far away). To this end, in this paper, synthetic benchmark high-fidelity EMT dynamic models of power grid with large-scale PV plants are presented. The models are developed in PSCAD and PSCAD/Fortran. Simulation results for different use cases (events) and scenarios are presented.

Marthi, Phani Ratna Vanamali↗
DOE OSTI2025

Anomaly Identification of Synchronized Voltage Waveform for Situational Awareness of Low Inertia Systems

Inverter-based resources (IBRs) such as photovoltaics (PVs), wind turbines, and battery energy storage systems (BESSs) are widely deployed in low-carbon power systems. However, these resources typically do not provide the inertia needed for grid stability, resulting in a low-inertia power system. IBRs and lack of inertia have been known to cause anomalies such as waveform distortions and wideband oscillations in power systems due to the limited inertia level, leading to increased generation trips and load shedding. Here, to achieve effective anomaly identification, this paper proposes a synchro-waveform-based algorithm utilizing real-time synchronized voltage waveform measurements from waveform measurement units (WMUs). In the proposed method, different physical characteristics, as well as statistical features, are extracted from synchronized voltage waveform measurements to filter anomalies. Then, the anomaly identification approach based on the random forest is developed and deployed into the FNET/GridEye system considering trade-offs among accuracy, computational burden, and deployment cost. Moreover, four WMUs are specially designed and deployed on Kauai Island to receive instantaneous synchronized voltage waveform measurements. To verify the performance of the proposed algorithm, different experiments are carried out with collected field test data. The result demonstrates that the performance of the proposed synchro-waveform-based anomaly categorization algorithm can accurately identify anomalies 95.35% of the time, which has comparable performance among benchmarking algorithms.

Situational awareness↗
NASA NTRS1993

A formally verified algorithm for interactive consistency under a hybrid fault model

Consistent distribution of single-source data to replicated computing channels is a fundamental problem in fault-tolerant system design. The 'Oral Messages' (OM) algorithm solves this problem of Interactive Consistency (Byzantine Agreement) assuming that all faults are worst-cass. Thambidurai and Park introduced a 'hybrid' fault model that distinguished three fault modes: asymmetric (Byzantine), symmetric, and benign; they also exhibited, along with an informal 'proof of correctness', a modified version of OM. Unfortunately, their algorithm is flawed. The discipline of mechanically checked formal verification eventually enabled us to develop a correct algorithm for Interactive Consistency under the hybrid fault model. This algorithm withstands $a$ asymmetric, $s$ symmetric, and $b$ benign faults simultaneously, using $m+1$ rounds, provided $n is greater than 2a + 2s + b + m$, and $m\geg a$. We present this algorithm, discuss its subtle points, and describe its formal specification and verification in PVS. We argue that formal verification systems such as PVS are now sufficiently effective that their application to fault-tolerance algorithms should be considered routine.

Lincoln, Patrick↗
NASA NTRS1995

Formal verification of an avionics microprocessor

Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This report discusses a project undertaken to answer some of these questions, the formal verification of the AAMPS microprocessor. This project consisted of formally specifying in the PVS language a rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show that the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification.

Srivas, Mandayam, K.↗
NASA NTRS1995

Formal methods demonstration project for space applications

The Space Shuttle program is cooperating in a pilot project to apply formal methods to live requirements analysis activities. As one of the larger ongoing shuttle Change Requests (CR's), the Global Positioning System (GPS) CR involves a significant upgrade to the Shuttle's navigation capability. Shuttles are to be outfitted with GPS receivers and the primary avionics software will be enhanced to accept GPS-provided positions and integrate them into navigation calculations. Prior to implementing the CR, requirements analysts at Loral Space Information Systems, the Shuttle software contractor, must scrutinize the CR to identify and resolve any requirements issues. We describe an ongoing task of the Formal Methods Demonstration Project for Space Applications whose goal is to find an effective way to use formal methods in the GPS CR requirements analysis phase. This phase is currently under way and a small team from NASA Langley, ViGYAN Inc. and Loral is now engaged in this task. Background on the GPS CR is provided and an overview of the hardware/software architecture is presented. We outline the approach being taken to formalize the requirements, only a subset of which is being attempted. The approach features the use of the PVS specification language to model 'principal functions', which are major units of Shuttle software. Conventional state machine techniques form the basis of our approach. Given this background, we present interim results based on a snapshot of work in progress. Samples of requirements specifications rendered in PVS are offered to illustration. We walk through a specification sketch for the principal function known as GPS Receiver State processing. Results to date are summarized and feedback from Loral requirements analysts is highlighted. Preliminary data is shown comparing issues detected by the formal methods team versus those detected using existing requirements analysis methods. We conclude by discussing our plan to complete the remaining activities of this task.

Divito, Ben L.↗
NASA NTRS1997

Fourth NASA Langley Formal Methods Workshop

This publication consists of papers presented at NASA Langley Research Center's fourth workshop on the application of formal methods to the design and verification of life-critical systems. Topic considered include: Proving properties of accident; modeling and validating SAFER in VDM-SL; requirement analysis of real-time control systems using PVS; a tabular language for system design; automated deductive verification of parallel systems. Also included is a fundamental hardware design in PVS.

Holloway, C. Michael↗
NASA NTRS1999

Formal Verification of the AAMP-FV Microcode

This report describes the experiences of Collins Avionics & Communications and SRI International in formally specifying and verifying the microcode in a Rockwell proprietary microprocessor, the AAMP-FV, using the PVS verification system. This project built extensively on earlier experiences using PVS to verify the microcode in the AAMP5, a complex, pipelined microprocessor designed for use in avionics displays and global positioning systems. While the AAMP5 experiment demonstrated the technical feasibility of formal verification of microcode, the steep learning curve encountered left unanswered the question of whether it could be performed at reasonable cost. The AAMP-FV project was conducted to determine whether the experience gained on the AAMP5 project could be used to make formal verification of microcode cost effective for safety-critical and high volume devices.

Miller, Steven P.↗
NASA NTRS1998

Cooperation Among Theorem Provers

This is a final report, which supports NASA's PECSEE (Persistent Cognizant Software Engineering Environment) effort and complements the Kestrel Institute project "Inference System Integration via Logic Morphism". The ultimate purpose of the project is to develop a superior logical inference mechanism by combining the diverse abilities of multiple cooperating theorem provers. In many years of research, a number of powerful theorem-proving systems have arisen with differing capabilities and strengths. Resolution theorem provers (such as Kestrel's KITP or SRI's, SNARK) deal with first-order logic with equality but not the principle of mathematical induction. The Boyer-Moore theorem prover excels at proof by induction but cannot deal with full first-order logic. Both are highly automated but cannot accept user guidance easily. The PVS system (from SRI) in only automatic within decidable theories, but it has well-designed interactive capabilities: furthermore, it includes higher-order logic, not just first-order logic. The NuPRL system from Cornell University and the STeP system from Stanford University have facilities for constructive logic and temporal logic, respectively - both are interactive. It is often suggested - for example, in the anonymous "QED Manifesto"-that we should pool the resources of all these theorem provers into a single system, so that the strengths of one can compensate for the weaknesses of others, and so that effort will not be duplicated. However, there is no straightforward way of doing this, because each system relies on its own language and logic for its success. Thus. SNARK uses ordinary first-order logic with equality, PVS uses higher-order logic. and NuPRL uses constructive logic. The purpose of this project, and the companion project at Kestrel, has been to use the category-theoretic notion of logic morphism to combine systems with different logics and languages. Kestrel's SPECWARE system has been the vehicle for the implementation.

Waldinger, Richard J.↗
NASA NTRS2004

Model Checking Failed Conjectures in Theorem Proving: A Case Study

Interactive mechanical theorem proving can provide high assurance of correct design, but it can also be a slow iterative process. Much time is spent determining why a proof of a conjecture is not forthcoming. In some cases, the conjecture is false and in others, the attempted proof is insufficient. In this case study, we use the SAL family of model checkers to generate a concrete counterexample to an unproven conjecture specified in the mechanical theorem prover, PVS. The focus of our case study is the ROBUS Interactive Consistency Protocol. We combine the use of a mechanical theorem prover and a model checker to expose a subtle flaw in the protocol that occurs under a particular scenario of faults and processor states. Uncovering the flaw allows us to mend the protocol and complete its general verification in PVS.

Pike, Lee↗
NASA NTRS2009

A Test Generation Framework for Distributed Fault-Tolerant Algorithms

Heavyweight formal methods such as theorem proving have been successfully applied to the analysis of safety critical fault-tolerant systems. Typically, the models and proofs performed during such analysis do not inform the testing process of actual implementations. We propose a framework for generating test vectors from specifications written in the Prototype Verification System (PVS). The methodology uses a translator to produce a Java prototype from a PVS specification. Symbolic (Java) PathFinder is then employed to generate a collection of test cases. A small example is employed to illustrate how the framework can be used in practice.

Goodloe, Alwyn↗
NASA NTRS2009

From Verified Models to Verifiable Code

Declarative specifications of digital systems often contain parts that can be automatically translated into executable code. Automated code generation may reduce or eliminate the kinds of errors typically introduced through manual code writing. For this approach to be effective, the generated code should be reasonably efficient and, more importantly, verifiable. This paper presents a prototype code generator for the Prototype Verification System (PVS) that translates a subset of PVS functional specifications into an intermediate language and subsequently to multiple target programming languages. Several case studies are presented to illustrate the tool's functionality. The generated code can be analyzed by software verification tools such as verification condition generators, static analyzers, and software model-checkers to increase the confidence that the generated code is correct.

Lensink, Leonard↗
NASA NTRS2010

Proceedings of the Second NASA Formal Methods Symposium

This publication contains the proceedings of the Second NASA Formal Methods Symposium sponsored by the National Aeronautics and Space Administration and held in Washington D.C. April 13-15, 2010. Topics covered include: Decision Engines for Software Analysis using Satisfiability Modulo Theories Solvers; Verification and Validation of Flight-Critical Systems; Formal Methods at Intel -- An Overview; Automatic Review of Abstract State Machines by Meta Property Verification; Hardware-independent Proofs of Numerical Programs; Slice-based Formal Specification Measures -- Mapping Coupling and Cohesion Measures to Formal Z; How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project; A Machine-Checked Proof of A State-Space Construction Algorithm; Automated Assume-Guarantee Reasoning for Omega-Regular Systems and Specifications; Modeling Regular Replacement for String Constraint Solving; Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol; Can Regulatory Bodies Expect Efficient Help from Formal Methods?; Synthesis of Greedy Algorithms Using Dominance Relations; A New Method for Incremental Testing of Finite State Machines; Verification of Faulty Message Passing Systems with Continuous State Space in PVS; Phase Two Feasibility Study for Software Safety Requirements Analysis Using Model Checking; A Prototype Embedding of Bluespec System Verilog in the PVS Theorem Prover; SimCheck: An Expressive Type System for Simulink; Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness; Software Model Checking of ARINC-653 Flight Code with MCP; Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B; Formal Verification of Large Software Systems; Symbolic Computation of Strongly Connected Components Using Saturation; Towards the Formal Verification of a Distributed Real-Time Automotive System; Slicing AADL Specifications for Model Checking; Model Checking with Edge-valued Decision Diagrams; and Data-flow based Model Analysis.

Munoz, Cesar↗
NASA NTRSDate not supplied

Intelligent Lemma Selection for Formal Methods Proofs

To help in formally verifying the correctness of various systems, NASA constructs mathematical proofs using the proof assistant PVS (Prototype Verification System). Throughout this effort, NASA has amassed a library of tens of thousands of proven lemmas. While these lemmas can often be applied to new problems, their abundance can make lemma selection a non-trivial task. This project focuses on creating a lemma selector for use in PVS based on existing systems MePo, MaSh, and MeSh, which were written for other proof assistants. An initial benchmark system makes selections based on symbol-level similarity while the final lemma selector is a hybrid system, combining the classical approach used in the benchmark with a machine learning approach which leverages the lemmas' past usage.

Connor T Baumler↗