SEARCH · Engineering Papers
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.
PVSio is a conservative extension to the PVS prelude library that provides basic input/output capabilities to the PVS ground evaluator. It supports rapid prototyping in PVS by enhancing the specification language with built-in constructs for string manipulation, floating point arithmetic, and input/output operations.
We develop a formalization of floating-point numbers in PVS based on a well-known formalization in Coq. We first describe the definitions of all the needed notions, e.g., floating-point number, format, rounding modes, etc.; then, we present an application to polynomial evaluation for elementary function evaluation. The application already existed in Coq, but our formalization shows a clear improvement in the quality of the result due to the automation provided by PVS. We finally integrate our formalization into a PVS hardware-level formalization of the IEEE-854 standard previously developed at NASA.
The batch execution modes of PVS are powerful, but highly technical, features of the system that are mostly accessible to expert users. This paper presents a PVS tool, called ProofLite, that extends the theorem prover interface with a batch proving utility and a proof scripting notation. ProofLite enables a semi-literate proving style where specification and proof scripts reside in the same file. The goal of ProofLite is to provide batch proving and proof scripting capabilities to regular, non-expert, users of PVS.
Bluespec SystemVerilog (BSV) is a Hardware Description Language based on the guarded action model of concurrency. It has an elegant semantics, which makes it well suited for formal reasoning. To date, a number of BSV designs have been verified with hand proofs, but little work has been conducted on the application of automated reasoning. We present a prototype shallow embedding of BSV in the PVS theorem prover. Our embedding is compatible with the PVS model checker, which can automatically prove an important class of theorems, and can also be used in conjunction with the powerful proof strategies of PVS to verify a broader class of properties than can be achieved with model checking alone.
This paper reports the development of a proof strategy that integrates the MetiTarski theorem prover as a trusted external decision procedure into the PVS theorem prover. The strategy automatically discharges PVS sequents containing real-valued formulas, including transcendental and special functions, by translating the sequents into first order formulas and submitting them to MetiTarski. The new strategy is considerably faster and more powerful than other strategies for nonlinear arithmetic available to PVS.
In order to solve the voltage violations caused by high penetration distributed photovoltaics (PVs), this paper proposes a decentralized voltage optimization method for distribution networks. Through the optimal dispatch of distributed PVs and reactive power resources, it realizes the voltage security and economic operation of distribution systems and facilitates the integration of massive distributed PVs. The proposed method is inspired by the idea of locational marginal price (LMP) and feasible cutting plane. It separates the optimization of boundary bus voltage and power flow in adjacent regions and uses the interaction of boundary variables’ marginal prices to obtain the optimal solution. The effectiveness and accuracy of the proposed method are demonstrated via simulation test on a practical l0kV feeder in China.
This paper proposes a multi-fidelity learning approach for distribution voltage probabilistic analysis with high penetration of PVs. Unlike the existing machine learning-based approaches that require a large number of high fidelity data to achieve satisfactory results, our approach strategically leverage massive low fidelity data from inaccurate model simulations and limited high fidelity historical data. The key idea is to use low-fidelity data to establish an initial model and then the high-fidelity data to calibrate and correct the constructed low-fidelity model. This allows us to fuse low- and high-fidelity data, yielding a high fidelity prediction model. Results obtained from a realistic feeder in US with 80% penetration of PVs show that the proposed approach can achieve a similar accuracy to the one with a large number of high fidelity data. This significantly highlights the advantages of the proposed method as compared to existing data-hungry machine learning methods. Different levels of fidelity data and their impacts are also investigated.
This paper proposes an analytic neural network Gaussian process (NNGP)-based chance-constrained real-time voltage regulation method for active distribution systems with photovoltaics (PVs), batteries, and electric vehicles (EVs). NNGP can utilize historical measurement data to achieve real-time probabilistic node voltage estimation through Bayesian inference. Then, NNGP is fully analytically embedded into the optimal power flow model to perform voltage regulation and adapt to various topological changes. The uncertainties of voltage estimations are easily considered via the chance constraint, and it has been shown that the adoption of this chance constraint can significantly improve the reliability of voltage regulation under various scenarios. The comparison results with other methods, carried out on a real 759-node distribution system located in western Colorado, U.S., show that the proposed method can achieve accurate voltage estimation across different topologies and reliably perform voltage regulation considering PVs, batteries, and EVs.
This paper proposes a novel model-free/data-driven centralized training and decentralized execution multi-agent deep reinforcement learning (MADRL) framework for distribution system voltage control with high penetration of PVs. The proposed MADRL can coordinate both the real and reactive power control of PVs with existing static var compensators and battery storage systems. Unlike the existing DRL-based voltage control methods, our proposed method does not rely on a system model during both the training and execution stages. This is achieved by developing a new interaction scheme between the surrogate modeling of the original system and the multi-agent soft actor critic (MASAC) MADRL algorithm. In particular, the sparse pseudo-Gaussian process with a few-shots of measurements is utilized to construct the surrogate model of the original environment, i.e., power flow model. This is a data-driven process and no model parameters are needed. Furthermore, the MASAC enabled MADRL allows to achieve better scalability by dividing the original system into different voltage control regions with the aid of real and reactive power sensitivities to voltage, where each region is treated as an agent. This also serves as the foundation for the centralized training and decentralized execution, thus significantly reducing the communication requirements as only local measurements are required for control. Comparative results with other alternatives on the IEEE 123-nodes and 342-nodes systems demonstrate the superiority of the proposed method.
Consider a collection of data generated by sensors from a set of aircraft. Data association is the process of connecting each sensor measurement with its corresponding aircraft. Furthermore once the data association has taken place, the state of the aircraft can be approximated using a Kalman filter. This talk aims to explore formal specification and verification of data association in the Prototype Verification System (PVS). Formal specification and verification of data association includes development of Kalman filters, Mahalanobis distance, and other topics of matrix analysis in PVS.
This paper describes a bitvectors library that has been developed for PVS. The library defines a bitvector as a function from a subrange of the integers into (0,1). The library provides functions that interpret a bitvector as a natural number, as a 2's complement number, as a vector of logical values and as a 2's complement fraction. The library provides a concatenation operator and an extractor. Shift, extend and rotate operations are also, defined. Fundamental properties of each of these operations have been proved in PVS.
The development of Programmable Logic Devices (PLDs) has introduced programming as a primary tool in the development of digital circuits. This work attempts to create a generic verification environment in which designs can be specified and verified using the Prototype Verification System (PVS). This is accomplished by providing library support for general hardware constructs. The environment is intended for use with any PLD and any PLD programming language. The goal of the environment is to allow the easy translation of digital designs to PVS and provide sufficient support to make verification possible without a great deal of effort.
The purpose of this task was to provide a mechanism for theory interpretations in a prototype verification system (PVS) so that it is possible to demonstrate the consistency of a theory by exhibiting an interpretation that validates the axioms. The mechanization makes it possible to show that one collection of theories is correctly interpreted by another collection of theories under a user-specified interpretation for the uninterpreted types and constants. A theory instance is generated and imported, while the axiom instances are generated as proof obligations to ensure that the interpretation is valid. Interpretations can be used to show that an implementation is a correct refinement of a specification, that an axiomatically defined specification is consistent, or that a axiomatically defined specification captures its intended models. In addition, the theory parameter mechanism has been extended with a notion of theory as parameter so that a theory instance can be given as an actual parameter to an imported theory. Theory interpretations can thus be used to refine an abstract specification or to demonstrate the consistency of an axiomatic theory. In this report we describe the mechanism in detail. This extension is a part of PVS version 3.0, which will be publicly released in mid-2001.
The purpose of this document is to ensure the structural integrity of PVS through implementation of a minimum set of requirements for ground-based PVS in accordance with this document, NASA Policy Directive (NPD) 8710.5, NASA Safety Policy for Pressure Vessels and Pressurized Systems, NASA Procedural Requirements (NPR) 8715.3, NASA General Safety Program Requirements, applicable Federal Regulations, and national consensus codes and standards (NCS).
The purpose of this project is to understand dynamic phenomena by designing dynamic models of utility-sale solar photovoltaic (PV) power plants and their interactions with grids; and construct effective coordination strategies for stability enhancement for solar PVs to respond to rapidly changing grid conditions.
The increasing penetration of behind-the-meter PVs causes challenges to maintain voltage security due to the lack of distribution system visibility. This paper proposes a nonlinear autoregressive Gaussian process (NARGP) approach to fuse limited number of SCADA/AMI data together with historical pseudo measurements for distribution node voltage probabilistic estimation. The high-fidelity SCADA data are fused with the low-fidelity AMI and pseudo measurements by the autoregressive algorithm embedded in the Gaussian process. This allows us to use multi-fidelity data to achieve entire distribution system voltage visibility. Numerical results carried out on the IEEE 123node system demonstrate that the NARGP method is able to obtain high accuracy in estimating bus voltage and quantifying estimation uncertainties as compared to other approaches.
This paper documents the NASA Langley PVS graph theory library. The library provides fundamental definitions for graphs, subgraphs, walks, paths, subgraphs generated by walks, trees, cycles, degree, separating sets, and four notions of connectedness. Theorems provided include Ramsey's and Menger's and the equivalence of all four notions of connectedness.
We describe an approach to strategy-based proving for improved interactive deduction in specialized domains. An experimental package of strategies (tactics) and support functions called Manip has been developed for PVS to reduce the tedium of arithmetic manipulation. Included are strategies aimed at algebraic simplification of real-valued expressions. A general deduction architecture is described in which domain-specific strategies, such as those for algebraic manipulation, are supported by more generic features, such as term-access techniques applicable in arbitrary settings. An extended expression language provides access to subterms within a sequent.