Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “pele”

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 37 records · Page 2
All sourcesNASA NTRSDOE OSTI
NASA NTRS1978

The effect of prefilter design on sample rate selection in digital flight control systems

The effect of prefilters on sample rate selection is examined and design procedures are determined for obtaining the best combination of prefilter breakpoint and sample rate. The employed approach involves a quantitative comparison of the output noise response of systems originating from the same basic plant and designed over a wide range of prefilters and sample rates. Each system design was carefully tailored so that it exhibited approximately identical responses to commands. The results presented augment the criteria for sample rate selection which have been discussed by Powell and Katz (1975). Attention is given to system characteristics, an integrator as a plant, and the short period motion of the F-8 aircraft.

Peled, U.↗
NASA NTRS1990

Capacity decline of ambient temperature secondary Li-TiS2 cells

The main objective of the study described was to identify the causes responsible for the capacity losses observed during cycling of secondary Li-TiS2 cells. Experimental Li-TiS2 cells were fabricated and tested for their cycle life performance. The open circuit voltage of the cells was monitored during the rest period between the charging and discharging. The polarization at the Li and TiS2 electrodes was also monitored during cycling. Cycled cells were disassembled and the cathodes were analyzed by various analytical techniques. The results of the study indicate that the observed capacity loss is almost entirely due to the increased polarization of the TiS2 electrode with cycling. The electrolyte was found to degrade during cycling and the degradation products were found to deposit at the TiS2 electrode, which probably lead to the higher polarization.

Subbarao, S.↗
NASA NTRS1993

Effect of cycling on the lithium/electrolyte interface in organic electrolytes

Nondestructive methods such as ac impedance spectroscopy and microcalorimetry are used to study the effect of cell cycling on the lithium/electrolyte interface. The reactivity of both uncycled and cycled lithium towards various electrolytes is examined by measuring the heat evolved from the cells under open-circuit conditions at 25 C by microcalorimetry. Cycled cells at the end of charge/discharge exhibited considerably higher heat output compared with the uncycled cells. After 30 d of storage, the heat output of the cycled cells is similar to that of the uncycled cells. The cell internal resistance increases with cycling, and this is attributed to the degradation of the electrolyte with cycling.

Surampudi, S.↗
NASA NTRS1994

Composite Solid Electrolyte For Lithium Cells

Composite solid electrolyte material consists of very small particles, each coated with thin layer of Lil, bonded together with polymer electrolyte or other organic binder. Material offers significant advantages over other solid electrolytes in lithium cells and batteries. Features include high ionic conductivity and strength. Composite solid electrolyte expected to exhibit flexibility of polymeric electrolytes. Polymer in composite solid electrolyte serves two purposes: used as binder alone, conduction taking place only in AI2O3 particles coated with solid Lil; or used as both binder and polymeric electrolyte, providing ionic conductivity between solid particles that it binds together.

Peled, Emmanuel↗
NASA NTRS1993

Composite Solid Electrolyte for Li Battery Applications

The electrochemical, bulk and interfacial properties of the polyethylene oxide (PEO) based composite solid electrolyte (CSE) comprising LiI, PEO, and Al2O3 have been evaluated for Li battery applications. The bulk interfacial and transport properties of the CSEs seem to strongly depend on the alumina particle size. For the CSE films with 0.05 micron alumina while the bulk conductivity is around 10(exp -4) (mho/cm) at 103 C, the Li ion transport number seems to be close to unity at the same temperature. Compared to the PEO electrolyte this polymer composite electrolyte seems to exhibit robust mechanical and interfacial properties. We have studied three different films with three different alumina sizes in the range 0.01-0.3 micron. Effects of Al2O3 particle size on the electrochemical performance of polymer composite electrolyte is discussed. With TiS2 as cathode a 10 mAh small capacity cell was charged and discharged at C/40 and C/20 rates respectively.

Nagasubramanian, G.↗
NASA NTRS1999

Single-shot diffusion measurement in laser-polarized Gas

A single-shot pulsed gradient stimulated echo sequence is introduced to address the challenges of diffusion measurements of laser polarized 3He and 129Xe gas. Laser polarization enhances the NMR sensitivity of these noble gases by >10(3), but creates an unstable, nonthermal polarization that is not readily renewable. A new method is presented which permits parallel acquisition of the several measurements required to determine a diffusive attenuation curve. The NMR characterization of a sample's diffusion behavior can be accomplished in a single measurement, using only a single polarization step. As a demonstration, the diffusion coefficient of a sample of laser-polarized 129Xe gas is measured via this method. Copyright 1999 Academic Press.

Non-NASA Center↗
NASA NTRS1998

Pulsed-field-gradient measurements of time-dependent gas diffusion

Pulsed-field-gradient NMR techniques are demonstrated for measurements of time-dependent gas diffusion. The standard PGSE technique and variants, applied to a free gas mixture of thermally polarized xenon and O2, are found to provide a reproducible measure of the xenon diffusion coefficient (5.71 x 10(-6) m2 s-1 for 1 atm of pure xenon), in excellent agreement with previous, non-NMR measurements. The utility of pulsed-field-gradient NMR techniques is demonstrated by the first measurement of time-dependent (i.e., restricted) gas diffusion inside a porous medium (a random pack of glass beads), with results that agree well with theory. Two modified NMR pulse sequences derived from the PGSE technique (named the Pulsed Gradient Echo, or PGE, and the Pulsed Gradient Multiple Spin Echo, or PGMSE) are also applied to measurements of time dependent diffusion of laser polarized xenon gas, with results in good agreement with previous measurements on thermally polarized gas. The PGMSE technique is found to be superior to the PGE method, and to standard PGSE techniques and variants, for efficiently measuring laser polarized noble gas diffusion over a wide range of diffusion times. Copyright 1998 Academic Press.

NASA Discipline Environmental Health↗
NASA NTRS1997

NMR of laser-polarized 129Xe in blood foam

Laser-polarized 129Xe dissolved in a foam preparation of fresh human blood was investigated. The NMR signal of 129Xe dissolved in blood was enhanced by creating a foam in which the dissolved 129Xe exchanged with a large reservoir of gaseous laser-polarized 129Xe. The dissolved 129Xe T1 in this system was found to be significantly shorter in oxygenated blood than in deoxygenated blood. The T1 of 129Xe dissolved in oxygenated blood foam was found to be approximately 21 (+/-5) s, and in deoxygenated blood foam to be greater than 40 s. To understand the oxygenation trend, T1 measurements were also made on plasma and hemoglobin foam preparations. The measurement technique using a foam gas-liquid exchange interface may also be useful for studying foam coarsening and other liquid physical properties.

Non-NASA Center↗
NASA NTRS2018

Refining the Safety - Liveness Classification of Temporal Properties According to Monitorability

Runtime verification is the topic of analyzing execution traces using formal techniques. It includes monitoring the execution of a system against temporal properties, commonly to detect violations. Not every temporal property is fully monitorable however: in some cases, the correctness of the execution does not depend on any finite prefix. We study the connection between monitorability and Lamport’s classification of properties to safety and liveness and their dual classes.We refine the definition of monitorability and provide algorithms to check which verdicts can be expected, a priori and during runtime verification.

Peled, Doron↗
NASA NTRS2018

Runtime Verification: From Propositional to First-Order Temporal Logic

Runtime Verification is a branch of formal methods concerned with analysis of execution traces for the purpose of determining the state or general quality of the executing system. The field covers numerous approaches, one of which is specification-based runtime verification, where execution traces are checked against formal specifications. The paper presents syntax, semantics, and monitoring algorithms for respectively propositional and first-order temporal logics. In propositional logics the observed events in the execution trace are represented using atomic propositions, while first-order logic allows universal and existential quantification over data occurring as arguments in events. Monitoring of the first-order case is drastically more challenging than the propositional case, and we present a solution for this problem based on BDDs. We furthermore discuss monitorability of temporal properties by dividing them into different classes representing different degrees of monitorability.

Peled, Doron↗
NASA NTRS2018

The DejaVu Runtime Verification Benchmark

In this paper we present a benchmark for evaluating runtime verification tools. It was originally created in order to compare the DEJAVU runtime verification tool1 with another similar tool. DEJAVU’s logic is first-order past time temporal logic. In order to monitor such properties efficiently, Binary Decision Diagrams (BDDs) [1] are used for representing the data observed in a trace. The details on the logic and its algorithm are described in e.g. [2, 3, 4]. The benchmark consists of six properties, formulated in English, and formalized in DEJAVU’s logic. For each property is provided (normally) three traces, of sizes varying from 10,000 events to one million events. Traces are represented in CSV format.

Ulus, Dogan↗
NASA NTRS2017

First Order Temporal Logic Monitoring with BDDs

Runtime verification is aimed at analyzing execution traces stemming from a running program or system. The traditional purpose is to detect the lack of conformance with respect to a formal specification. Numerous efforts in the field have focused on monitoring so-called parametric specifications, where events carry data, and formulas can refer to such. Since a monitor for such specifications has to store observed data, the challenge is to have an efficient representation and manipulation of Boolean operators, quantification, and lookup of data. The fundamental problem is that the actual values of the data are not necessarily bounded or provided in advance. In this work we explore the use of Binary Decision Diagrams (BDDs) for representing observed data. Our experiments show a substantial improvement in performance compared to related work.

Ulus, Dogan↗
NASA NTRS2018

DejaVu: A Monitoring Tool for First-Order Temporal Logic

Runtime Verification (rv) is aimed at analyzing individual execution traces and temporal behaviors observed from running programs and systems. Its traditional purpose is in detecting the lack of conformance with respect to a formal specification. While very early rv systems were based on specifications given in some form of propositional temporal logic, recent efforts have focused on monitoring so-called parametric specifications over events that carry data. Since a monitor for such specifications has to store observed data, the challenge is to have an efficient representation and manipulation of data. The fundamental problem is that the actual values of the data are not necessarily bounded or provided in advance. In this paper, we describe our monitoring tool, DejaVu, which implements our algorithm [HPU17] for monitoring first-order past linear-time temporal logic over a sequence of events that carry data. We propose the use of Binary Decision Diagrams (bdds) [Bry86] for representing and manipulating sets of observed data since (1) bdds provide highly compact representations, (2) operations over bdds, in particular complementation, are very efficient, and (3) the monitor construction for the propositional case shown in [HR02] naturally extends to bdds. Our experiments show a substantial improvement in performance compared to a related tool.

Ulus, Dogan↗
NASA NTRS2018

Efficient Runtime Verification of First-Order Temporal Properties

Runtime verification allows monitoring the execution of a system against a temporal property, raising an alarm if the property is violated. In this paper we present a theory and system for runtime verification of a first-order past time linear temporal logic. The first-order nature of the logic allows a monitor to reason about events with data elements. While runtime verification of propositional temporal logic requires only a fixed amount of memory, the first-order variant has to deal with a number of data values potentially growing unbounded in the length of the execution trace. This requires special compactness considerations in order to allow checking very long executions. In previous work we presented an efficient use of BDDs for such first-order runtime verification, implemented in the tool DEJAVU. We first summarize this previous work. Subsequently, we look at the new problem of dynamically identifying when data observed in the past are no longer needed, allowing to reclaim the data elements used to represent them. We also study the problem of adding relations over data values. Finally, we present parts of the implementation, including a new concept of user defined property macros.

Peled, Doron↗
NASA NTRS2018

BDDs on the Run

Runtime verification (RV) of first-order temporal logic must handle a potentially large amount of data, accumulated during the monitoring of an execution. The DEJAVU RV system represents data elements and relations using BDDs. This achieves a compact representation, which allows monitoring long executions. However, the potentially unbounded, and frequently very large amounts of data value scan,ultimately, limit the executions that can be monitored. We present an automatic method for “forgetting” data values when they no longer affect the RV verdict on an observed execution.We describe the algorithm and illustrate its operation through an example.

Peled, Doron↗