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 253 records · Page 14
All sourcesNASA NTRSDOE OSTI
DOE OSTI2020

DEEP Solar: Data DrivEn Modeling and Analytics for Enhanced System Layer ImPlementation

Realizing the SETO 2030 mission of reducing solar energy costs to 3-5 c/kWh will require innovative enabling research on effective, cost-efficient integration of local PV within distribution systems. However, the intermittent and variable nature of PVs compels operators to impose conservative hosting capacity constraints. Given the extremely high variability of (intermittent and unpredictable) solar energy generation, relaxing the capacity constraints (which are currently around 15%) and achieving 100% or greater integration of renewables will require a fundamental transformation of the power grid via the utilization of exponentially larger amounts of AMI enabled fine-grained data. To address the challenges in increasing the penetration of renewable energy based DERs, this project envisions an Enhanced System Layer (ESL) at the distribution network level that is reliable, cost-effective and scalable to millions of Distributed Energy Resources (DERs)/devices. This includes developing: 1) Transformative and highly scalable machine learning based predictive analytics tools that plug into distribution system planning and provide real-time situational awareness at the distribution level for short and long-term operational planning. The tools will be built using novel data-driven energy models of millions of active nodes with AMI, 2) Adaptive stochastic analysis and optimization algorithms for real-time grid operations, 3) Dynamic Scenario Analysis using parallel Cloudenabled implementations with < 1 minute computational cycle times.

14 SOLAR ENERGY↗
DOE OSTI2021

Dynamic Building Load Control to Facilitate High Penetration of Solar Photovoltaic Generation (Final Technical Report)

Solar photovoltaic (PV) resources are the most common form of distributed generation in residential and commercial customer premises within electric distribution networks. A higher penetration of PV generation in distribution circuits will impose challenges on maintaining service voltages within the range of industry standards, power quality, and power flow. Buildings consume 74% of the electricity produced in the United States, and a significant portion of the building load is dispatchable, making them responsive to electrical grid needs. Oak Ridge National Laboratory—in collaboration with Southern Company; the University of Tennessee, Knoxville; and the Georgia Institute of Technology—is examining the PV integration issues in distribution-level electrical grids and developing integrated demand-side control and communication systems to enable responsive loads. The proposed responsive loads mechanism performs renewable generation following to increase the penetration of solar PV within each feeder. The specific objectives of this project are to (1) examine distribution-level PV integration scenarios to understand requirements, (2) undertake an end-to-end simulation-based design of a distributed control strategy of loads geographically near the PV generation asset to minimize the effect on the distribution feeder, (3) deploy and demonstrate the control technology developed in partnership with utilities, and (4) perform a scalability analysis at the utility scale. This 3-year integrated project aims to develop, demonstrate, and validate demand-side control technology to enable increased the penetration of renewables while mitigating challenges that arise due to their intermittency. Activities in Budget Period (BP) 1 focused on a literature review and the formal design of a control system for integrating local distribution with generation and loads. The team used modeling and simulation to evaluate the impact of varying buildings loads, variable PV generation, and power flow dynamics on the distribution circuit. The dynamic models developed in BP 1 were used in BP 2 to develop a model-based control design and a test bed. The test bed has enabled the simulation-based testing and comparison of different control designs and formulations applied to different configurations of the distribution grid, PVs, and building loads. The control approaches developed in BP 2 were implemented in BP 3 in the form of hardware deployed at the Central Baptist Church (CBC) in Knoxville, Tennessee, for testing and evaluation. The outcome of this project was the development and demonstration of open-source, low-cost, low-touch sensing and control retrofits to distributed PV generation and building loads that, in a coordinated fashion, provide the load-shaping response needed to integrate high levels of renewable penetration. This research addresses the target metrics by dynamically controlling a load with solar generation variability to minimize the extent of two-way power flow, enhance reliability, facilitate high PV penetration (>100% of peak load in a line segment), and generate scalable software and hardware solutions adaptable to any penetration levels. The research and development activities are focused and designed to be impactful within the relevant 2020 targets time frame.An accurate open-source integration simulation framework for end-to-end control design was developed and deployed at the CBC facility for testing and evaluation. This final report provides a detailed review of the technical results achieved during this 3-year integrated project. A novel spectral analysis of PV data is demonstrated to derive the requirements of the control design. A detailed simulation-based analysis of PV integration at increasing penetration levels is presented using 1 year of PV data to demonstrate the impact on the distribution circuits. Two different control strategies were developed and demonstrated via simulation to track variable PV generation with adaptive load dispatch. The report concludes with a summary of accomplishments and recommendations for a path forward.

14 SOLAR ENERGY↗
DOE OSTI2022

Cross-Cutting Metrology Tools for In Operando Characterization of Carrier Dynamics in Photovoltaic Devices (Final Technical Report)

Understanding the nature of recombination and its dependence on defects and interfaces is essential for engineering materials and contacts for higher V oc and photovoltaic (PV) efficiency. Time-resolved photoluminescence (TRPL) has conventionally been used to evaluate recombination, but not all materials are strongly emissive or otherwise suitable. Time-resolved terahertz spectroscopy is a pump – probe method that presents valuable complementary information, wherein an optical pump pulse photoexcites carriers within the absorber and the transient photoconductivity is probed with a terahertz pulse. Until now, experimental constraints have prohibited the use of terahertz probes to interrogate full device stacks, and measurements were instead made on exfoliated films or films grown on unconventional substrates. However, interfaces are critical to the behavior of photoexcited carriers in solar cells, and the substrates themselves often influence the film growth and bulk properties. Therefore, it is important to probe the behavior of PV absorbers as close as possible to their normal operating conditions. Here we have developed cross-cutting metrology that enable in operando characterization of carrier dynamics and recombination mechanisms in working PV devices. Through a combination of complementary non-contact TRTS and TRPL experiments and modeling, we have obtained key parameters including photoexcited carrier bulk lifetime and interface and back surface recombination velocities with greater precision and accuracy than can be achieved with conventional TRPL alone. By varying pulsed photoexcitation conditions, the contributions of interface and bulk recombination mechanisms can be determined. We have developed and refined this characterization approach by investigating CdTe PVs, which is a well-established technology but with significant margin for further improvements in efficiency. Results were published in Journal of Applied Physics (DOI: 10.1063/5.0064730) and Proceedings of the IEEE PVSC (DOI: 10.1109/PVSC43889.2021.9518559). After validating the approach, we have applied it to correlate recombination rates to processing conditions and material properties, including composition and defects as well as interfaces and surface treatments. Such feedback can inform processing and design choices to enable higher PV efficiency, not only for CdTe, but also CdSe x Te 1-x , CIGS, perovskites, kesterites, and future technologies. A perspective on predicting solar cell performance from terahertz spectroscopy was published in Advanced Energy Materials (DOI: 10.1002/aenm.202102776). The cross-cutting metrology tools developed here will enable determination of the locus and mechanism of performance-limiting recombination in thin film PV devices. This feedback can guide the engineering of PV devices with higher V oc and efficiency, thereby leading to reductions in levelized cost of electricity to meet the SunShot 2030 target of $0.03/kWh for utility-scale PV. Lower costs will enable rapid expansion of renewable electricity generation that is nearly free of carbon emissions. Reducing carbon emissions of the electricity sector is one of the most important solutions to climate change. The project’s specific focus on CdTe PV can benefit First Solar, the US company that is the global leader in CdTe technology, through both technology and workforce development.

14 SOLAR ENERGY↗
DOE OSTI2019

Electric Vehicles as Flexibility Management Strategy for the Electricity System—A Comparison between Different Regions of Europe

This study considers whether electric vehicles (EVs) can be exploited as a flexibility management strategy to stimulate investments in and operation of renewable electricity under stringent CO 2 constraints in four regions with different conditions for renewable electricity (Sweden, Germany, the UK, and Spain). The study applies a cost-minimisation investment model and an electricity dispatch model of the European electricity system, assuming three types of charging strategies for EVs. The results show that vehicle-to-grid (V2G), i.e., the possibility to discharging the EV batteries back to grid, facilitates an increase in investments and generation from solar photovoltaics (PVs) compare to the scenario without EVs, in all regions except Sweden. Without the possibility to store electricity in EV batteries across different days, which is a technical limitation of this type of model, EVs increase the share of wind power by only a few percentage points in Sweden, even if Sweden is a region with good conditions for wind power. Full electrification of the road transport sector, including also dynamic power transfer for trucks and buses, would decrease the need for investments in peak power in all four regions by at least 50%, as compared to a scenario without EVs or with uncontrolled charging of EVs, provided that an optimal charging strategy and V2G are implemented for the passenger vehicles.

25 ENERGY STORAGE↗
DOE OSTI2016

The Energy and Environmental Performance of Ground-Mounted Photovoltaic Systems—A Timely Update

Given photovoltaics’ (PVs) constant improvements in terms of material usage and energy efficiency, this work provides a timely update on their life-cycle energy and environmental performance. Single-crystalline Si (sc-Si), multi-crystalline Si (mc-Si), cadmium telluride (CdTe) and copper indium gallium diselenide (CIGS) systems are analysed, considering the actual country of production and adapting the input electricity mix accordingly. Energy pay-back time (EPBT) results for fixed-tilt ground mounted installations range from 0.5 years for CdTe PV at high-irradiation (2300 kWh/(m 2 ·yr)) to 2.8 years for sc-Si PV at low-irradiation (1000 kWh/(m 2 ·yr)), with corresponding quality-adjusted energy return on investment (EROI PE-eq ) values ranging from over 60 to ~10. Global warming potential (GWP) per kWh el averages out at ~30 g(CO 2 -eq), with lower values (down to ~10 g) for CdTe PV at high irradiation, and up to ~80 g for Chinese sc-Si PV at low irradiation. In general, results point to CdTe PV as the best performing technology from an environmental life-cycle perspective, also showing a remarkable improvement for current production modules in comparison with previous generations. Finally, we determined that one-axis tracking installations can improve the environmental profile of PV systems by approximately 10% for most impact metrics.

14 SOLAR ENERGY↗
DOE OSTI2021

Improving Prediction of Peroxide Value of Edible Oils Using Regularized Regression Models

We present four unique prediction techniques, combined with multiple data pre-processing methods, utilizing a wide range of both oil types and oil peroxide values (PV) as well as incorporating natural aging for peroxide creation. Samples were PV assayed using a standard starch titration method, AOCS Method Cd 8-53, and used as a verified reference method for PV determination. Near-infrared (NIR) spectra were collected from each sample in two unique optical pathlengths (OPLs), 2 and 24 mm, then fused into a third distinct set. All three sets were used in partial least squares (PLS) regression, ridge regression, LASSO regression, and elastic net regression model calculation. While no individual regression model was established as the best, global models for each regression type and pre-processing method show good agreement between all regression types when performed in their optimal scenarios. Furthermore, small spectral window size boxcar averaging shows prediction accuracy improvements for edible oil PVs. Best-performing models for each regression type are: PLS regression, 25 point boxcar window fused OPL spectral information RMSEP = 2.50; ridge regression, 5 point boxcar window, 24 mm OPL, RMSEP = 2.20; LASSO raw spectral information, 24 mm OPL, RMSEP = 1.80; and elastic net, 10 point boxcar window, 24 mm OPL, RMSEP = 1.91. The results show promising advancements in the development of a full global model for PV determination of edible oils.

37 INORGANIC, ORGANIC, PHYSICAL, AND ANALYTICAL CH↗
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↗
NASA NTRS2000

Inference System Integration Via Logic Morphisms

This is a final report on the accomplishments during the period of the NASA grant. The work on inference servers accomplished the integration of the SLANG logic (Specware's default specification logic) with a number of inference servers in order to make their complementary strengths available. These inverence servers are (1) SNARK. (2) Gandalf, Setheo, and Spass, (3) the Prototype Verification System (PVS) from SRI. (4) HOL98. We designed and implemented MetaSlang, an ML-like language, which we are using to specify and implement all our logic morphisms.

Bjorner, Nikolaj S.↗
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 NTRS2001

Real Automation in the Field

We provide a package of strategies for automation of non-linear arithmetic in PVS. In particular, we describe a simplication procedure for the field of real numbers and a strategy for cancellation of common terms.

Munoz, Cesar↗
NASA NTRS2002

Modular Certification

Airplanes are certified as a whole: there is no established basis for separately certifying some components, particularly software-intensive ones, independently of their specific application in a given airplane. The absence of separate certification inhibits the development of modular components that could be largely "precertified" and used in several different contexts within a single airplane, or across many different airplanes. In this report, we examine the issues in modular certification of software components and propose an approach based on assume-guarantee reasoning. We extend the method from verification to certification by considering behavior in the presence of failures. This exposes the need for partitioning, and separation of assumptions and guarantees into normal and abnormal cases. We then identify three classes of property that must be verified within this framework: safe function, true guarantees, and controlled failure. We identify a particular assume-guarantee proof rule (due to McMillan) that is appropriate to the applications considered, and formally verify its soundness in PVS.

Rushby, John↗
NASA NTRS2004

Formal Modeling and Analysis of a Preliminary Small Aircraft Transportation System (SATS)Concept

New concepts for automating air traffic management functions at small non-towered airports raise serious safety issues associated with the software implementations and their underlying key algorithms. The criticality of such software systems necessitates that strong guarantees of the safety be developed for them. In this paper we present a formal method for modeling and verifying such systems using the PVS theorem proving system. The method is demonstrated on a preliminary concept of operation for the Small Aircraft Transportation System (SATS) project at NASA Langley.

Carrreno, Victor A.↗
NASA NTRS2004

Abstract Model of the SATS Concept of Operations: Initial Results and Recommendations

An abstract mathematical model of the concept of operations for the Small Aircraft Transportation System (SATS) is presented. The Concept of Operations consist of several procedures that describe nominal operations for SATS, Several safety properties of the system are proven using formal techniques. The final goal of the verification effort is to show that under nominal operations, aircraft are safely separated. The abstract model was written and formally verified in the Prototype Verification System (PVS).

Dowek, Gilles↗
NASA NTRS2004

Formal Verification of a Conflict Resolution and Recovery Algorithm

New air traffic management concepts distribute the duty of traffic separation among system participants. As a consequence, these concepts have a greater dependency and rely heavily on on-board software and hardware systems. One example of a new on-board capability in a distributed air traffic management system is air traffic conflict detection and resolution (CD&R). Traditional methods for safety assessment such as human-in-the-loop simulations, testing, and flight experiments may not be sufficient for this highly distributed system as the set of possible scenarios is too large to have a reasonable coverage. This paper proposes a new method for the safety assessment of avionics systems that makes use of formal methods to drive the development of critical systems. As a case study of this approach, the mechanical veri.cation of an algorithm for air traffic conflict resolution and recovery called RR3D is presented. The RR3D algorithm uses a geometric optimization technique to provide a choice of resolution and recovery maneuvers. If the aircraft adheres to these maneuvers, they will bring the aircraft out of conflict and the aircraft will follow a conflict-free path to its original destination. Veri.cation of RR3D is carried out using the Prototype Verification System (PVS).

Maddalon, Jeffrey↗