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.

SourceResearch connectionFrom yearThrough year

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

At least 163 records · Page 9

All sources NASA NTRS DOE OSTI

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↗

NASA NTRSDate not supplied

Formal Verification of Termination Criteria for First-Order Recursive Functions

This paper presents a formalization of several termination criteria for first-order recursive functions. The formalization, which is developed in the Prototype Verification System (PVS), includes the specification and proof of equivalence of semantic termination, Turing termination, size change principle, calling context graphs, and matrix-weighted graphs. These termination criteria are defined on a computational model that consists of a basic functional language called PVS0, which is an embedding of recursive first-order functions. Through this embedding, the native mechanism for checking termination of recursive functions in PVS could be soundly extended with semi-automatic termination criteria such as calling contexts graphs. As a proof of concept, this paper illustrates how such an extension can be implemented using proof strategies based on computational reflection.

Formal Verification↗

NASA NTRSDate not supplied

Formal Verification of Termination Criteria for First-Order Recursive Functions

This talk presents a formalization of several termination criteria for first-order recursive functions. The formalization, which is developed in the Prototype Verification System (PVS), includes the specification and proof of equivalence of semantic termination, Turing termination, size change principle, calling context graphs, and matrix-weighted graphs. These termination criteria are defined on a computational model that consists of a basic functional language called PVS0, which is an embedding of recursive first-order functions. Through this embedding, the native mechanism for checking termination of recursive functions in PVS could be soundly extended with semi-automatic termination criteria such as calling contexts graphs.

Termination↗

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↗

NASA NTRSDate not supplied

A Formal Verification Framework for Runtime Assurance

Runtime assurance↗

DOE OSTI2022

Performance Evaluation of Distributed Energy Resource Management Algorithm in Large Distribution Networks

This paper presents performance evaluation of hierarchical optimization and control for distributed energy resource management system (DERMS) in large distribution networks via an advanced hardware-in-the-loop (HIL) platform. The HIL platform provides realistic testing in a laboratory envi-ronment, including the accurate modeling of a full-scale dis-tribution system of 11,000 nodes, the DERMS software con-troller, and 90 power hardware photovoltaics (PVs) and bat-tery inverters. The applied DERMS algorithm is designed based on a real-time optimal power flow algorithm and im-plemented with acceleration design that performs fast dis-patch of simulated PVs and real physical hardware DER devices every 4 seconds.

distributed energy management system (DERMS)↗

DOE OSTI2022

Assessing the Optimality of LinDist3Flow for Optimal Tap Selection of Step Voltage Regulators in Unbalanced Distribution Networks: Preprint

The adoption of distributed energy resources such as photovoltaics (PVs) has increased dramatically during the previous decade. The increased penetration of PVs into distribution networks (DNs) can cause voltage fluctuations that have to be mitigated. One of the key utility assets employed to this end are step-voltage regulators (SVRs). It is desirable to include tap selection of SVRs in optimal power flow (OPF) routines, a task that turns out to be challenging because the resultant OPF problem is nonconvex with added complexities stemming from accurate SVR modeling. While several convex relaxations based on semi-definite programming (SDP) have been presented in the literature for optimal tap selection, SDP based schemes do not scale well and are challenging to implement in large-scale planning or operational frameworks. This paper deals with the optimal tap selection (OPTS) problem for wye-connected SVRs using linear approximations of power flow equations. Specifically, the LinDist3Flow model is adopted and the effective SVR ratio is assumed to be continuous–enabling the formulation of a problem called LinDist3Flow-OPTS, which amounts to a linear program. The scalability and optimality gap of LinDist3Flow-OPTS are evaluated with respect to existing SDP-based and nonlinear programming techniques for optimal tap selection in three standard feeders, namely, the IEEE 13-bus, 123-bus, and 8500-node DNs. For all DNs considered, LinDist3Flow-OPTS achieves an optimality gap of approximately 1% or less while significantly lowering the computational burden.

linear approximations↗

DOE OSTI2024

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 Rule-14) 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 ACDC 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.

08 - HYDROGEN↗

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↗

DOE OSTI2021

Feed-Forward Compensation for Model Predictive Control in Tri-port Current-Source Medium-Voltage String Inverters for PV-Plus-Storage Farms

The novel tri-port current-source medium-voltage string inverter (TCS-MVSI) is a promising candidate for large-scale PV-plus-storage (PVS) farms owing to its galvanic isolation, easy storage integration, soft-switching capability across entire load range, controlled low dv/dt and EMI, benign fault tolerance, etc. Due to its low inertia feature, traditional PI-based control cannot manage large transients effectively. Instead, a model-based predictive control (MPC) is proposed to achieve robust and stable operation. As is well known, the control performance of MPC is compromised by the sampling and computational delay during implementation significantly, if not well addressed. This paper analyzed and quantified these delays and then proposes feed-forward compensation (FFC) for the MPC method to compensate the delays and the large parameter variations due to the low-inertia nature. In addition, this method also compensates for the high dc-link ripple within each switching cycle, a unique issue for low-inertia converters. Here, the proposed method requires low computational effort, allowing it to be extended for multiple ports. The effectiveness of the proposed method has been validated in experiments. In 10 kW test, the proposed method decreases the average dc-link current by 17%, leading to ~20% conduction losses and ~0.5% increase in converter efficiency. In addition, the peak dc-link current also decreases by 15%, resulting in reduced transformer size. As a result, an increased power density can be achieved with the proposed method. Similar improvements have been observed across the power range from 2 kW to 10 kW.

30 DIRECT ENERGY CONVERSION↗

DOE OSTI2020

Aging Effect Analysis of PV Inverter Semiconductors for Ancillary Services Support

PV inverters can provide reactive power while generating active power. An ongoing microgrid implementation at Duke Energy actively engages non-utility PVs to generate/absorb reactive power in support of ancillary services to increase microgrid resiliency during extreme events. PV systems are requested to provide reactive power support: 1) in response to grid voltage variation to better regulate the local voltage; or 2) in response to utility incentives, such as following Transactive Energy System (TES) incentives. However, providing ancillary services might shorten the lifetime expectation of PV inverter semiconductors. This paper summarizes the potential impacts on a PV inverter semiconductor's lifetime when providing ancillary services. The analysis presented in this research work shows that providing reactive power support will increase the mean junction temperature and the junction temperature variation of the inverter diodes. This increased junction temperature will eventually lead to shorter diode lifetime. The lifetime estimation of semiconductors is briefly reviewed. The power losses of PV inverter semiconductors are derived as a support analysis to the junction temperature calculation. In addition, the impact of the filtering inductor on the semiconductor current distribution is discussed. The theoretical analysis presented in this research work is supported by simulation results.

14 SOLAR ENERGY↗

DOE OSTI2022

Multi-Agent Deep Reinforcement Learning for Realistic Distribution System Voltage Control Using PV Inverters

Over the last few decades, the deployment of distributed solar photovoltaic (PV) systems has increased consistently. High PV penetration could cause adverse effects on the grid, such as voltage violations. This paper proposes a new distributed soft actor-critic based multi-agent deep reinforcement learning (SAC-MADRL) control solution to minimize the PV real power curtailment while keeping the grid voltage in an acceptable range. New reward functions have been designed to coordinate different agents during the learning process, yielding improved convergence. Comparison results with other control methods on a real feeder in western Colorado U.S. with 80% penetration of PVs demonstrate that the proposed method has better capability of effectively regulating voltage while minimizing the PV real power curtailment.

distribution system↗

DOE OSTI2023

Large Angle Deviation in Grid-Following IBRs Upon Grid Voltage Dip

In the 2021 Texas Odessa large-scale solar PV tripping events, phase-locked-loop (PLL) loss of synchronism is identified as a major cause of solar PV tripping. When solar PVs detected a large phase angle deviation (e.g., 10 degrees), tripping commands were initiated. Here, the large phase angle deviation was triggered by a transmission line fault 200 miles away, which in turn led to approximately 30% voltage drop in the 345-kV system. This paper offers a plausible reason why grid-following inverter-based resources (IBRs) may experience a large angle deviation upon grid voltage dip. Critical operating conditions contributing to such phenomena are identified via analysis and their effects are demonstrated using electromagnetic transient (EMT) simulation. Furthermore, the effect of converter control, e.g., grid-following control vs. grid-forming control, is examined. It is found from EMT simulation results that frequency and voltage control are helpful in mitigating angle deviation. Furthermore, linear block diagrams are derived to examine why frequency control can effectively suppress large angle deviation.

14 SOLAR ENERGY↗

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↗