SEARCH · Search NASA
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.
Digital computer programs determine steady-state performance characteristics of active and passive linear circuits. The ac analysis program solves the basic circuit parameters. The compiler program solves these circuit parameters and in addition provides a more versatile program by allowing the user to perform mathematical and logical operations.
Circuit features, variational capabilities, input-output capabilities, and transient analysis of NET-2 circuit program
The NASA/MSFC high speed CMOS/SOS standard cell family, designed to be compatible with the PR2D (Place, Route in 2-Dimensions) automatic layout program, is described. Standard cell data sheets show the logic diagram, the schematic, the truth table, and propagation delays for each logic cell.
Two expert systems were written in OPS5 by the expert, a Ph.D. astronomer with no prior experience in artificial intelligence or expert systems, without the use of a knowledge engineer. The first system was built from scratch and uses 146 rules to check for duplication of scientific information within a pool of prospective observations. The second system was grafted onto another expert system and uses 149 additional rules to estimate the spacecraft and ground resources consumed by a set of prospective observations. The small vocabulary, the IF this occurs THEN do that logical structure of OPS5, and the ability to follow program execution allowed the expert to design and implement these systems with only the data structures and rules of another OPS5 system as an example. The modularity of the rules in OPS5 allowed the second system to modify the rulebase of the system onto which it was grafted without changing the code or the operation of that system. These experiences show that experts are able to develop their own expert systems due to the ease of programming and code reusability in OPS5.
This annual review reports the center's activities and findings on very large scale integration (VLSI) systems design for 1990, including project status, financial support, publications, the NASA Space Engineering Research Center (SERC) Symposium on VLSI Design, research results, and outreach programs. Processor chips completed or under development are listed. Research results summarized include a design technique to harden complementary metal oxide semiconductors (CMOS) memory circuits against single event upset (SEU); improved circuit design procedures; and advances in computer aided design (CAD), communications, computer architectures, and reliability design. Also described is a high school teacher program that exposes teachers to the fundamentals of digital logic design.
An observation of Charged Lepton Flavor Violation (CLFV) would be unambiguous evidence for physics beyond the Standard Model. The Mu2e and COMET experiments, under construction, are designed to push the sensitivity to CLFV in the mu to e conversion process to unprecedented levels. Whether conversion is observed or not, there is a strong case to be made for further improving sensitivity, or for examining the process on additional target materials. Mu2e-II is a proposed upgrade to Mu2e, with at least an additional order of magnitude in sensitivity to the conversion rate over Mu2e. The approach and challenges for this proposal are summarized. Mu2e-II may be regarded as the next logical step in a continued high-intensity muon program at FNAL.
Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and mission-critical applications. This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and dL’s proof calculus. The formalization embeds dL into the PVS logic, resulting in a version of dL whose proof calculus is not only formally verified, but is also available for the verification of hybrid programs within PVS itself. This embedding, called Plaidypvs (Properly Assured Implementation of dL for Hybrid Program Verification and Specification), supports standard dL style proofs, but further leverages the capabilities of PVS to allow reasoning about entire classes of hybrid programs. The embedding also allows the user to import the well-established definitions and mathematical theories available in PVS.
The Hoare approach to program verification relies on the construction and discharge of verification conditions (VCs) but offers no support to trace, analyze, and understand the VCs themselves. We describe a systematic extension of the Hoare rules by labels so that the calculus itself can be used to build up explanations of the VCs. The labels are maintained through the different processing steps and rendered as natural language explanations. The explanations can easily be customized and can capture different aspects of the VCs; here, we focus on their structure and purpose. The approach is fully declarative and the generated explanations are based only on an analysis of the labels rather than directly on the logical meaning of the underlying VCs or their proofs. Keywords: program verification, Hoare calculus, traceability.
Supercomputing applications are increasingly adopting the MPI+threads programming model over the traditional "MPI everywhere" approach to better handle the disproportionate increase in the number of cores compared with other on-node resources. In practice, however, most applications observe a slower performance with MPI+threads primarily because of poor communication performance. Recent research efforts on MPI libraries address this bottleneck by mapping logically parallel communication, that is, operations that are not subject to MPI's ordering constraints to the underlying network parallelism. Domain scientists, however, typically do not expose such communication independence information because the existing MPI-3.1 standard's semantics can be limiting. Researchers had initially proposed user-visible endpoints to combat this issue, but such a solution requires intrusive changes to the standard (new APIs). The upcoming MPI-4.0 standard, on the other hand, allows applications to relax unneeded semantics and provides them with many opportunities to express logical communication parallelism. Here in this article, we show how MPI+threads applications can achieve high performance with logically parallel communication. Through application case studies, we compare the capabilities of the new MPI-4.0 standard with those of the existing one and user-visible endpoints (upper bound). Logical communication parallelism can boost the overall performance of an application by over 2x.
A synthesis method and new VLSI architecture are introduced to realize sequential circuits that have the ability to implement any state machine having N states and m inputs, regardless of the actual sequence specified in the flow table. A design method is proposed that utilizes BTS logic to implement regular and dense circuits. A given state sequence can be programmed with power supply connections or dynamically reallocated if stored in a register. Arbitrary flow table sequences can be modified or programmed to dynamically alter the function of the machine. This allows VLSI controllers to be designed with the programmability of a general purpose processor but with the compact size and performance of dedicated logic.
This paper summarizes a joint NASA/Air Force Full Scale Engine Research (FSER) program conducted with the F100 engine during the period 1974 through 1979. The program mechanism is described and the F100 test vehicles utilized are illustrated. Technology items which have been addressed in the areas of swirl augmentation, flutter phenomenon, advanced electronic control logic theory, strain gage technology, and distortion sensitivity are identified and the associated test programs conducted at the NASA-Lewis Research Center are described. Results presented show that the FSER approach, which utilizes existing state-of-the-art engine hardware to evaluate advanced technology concepts and problem areas, can contribute a significant data base for future system applications. Aerodynamic phenomenon previously not considered by current design systems have been identified and incorporated into current industry design tools.
A document presents additional information on the means of implementing a capability for wide tuning of microwave receiver and transmitter frequencies in the development reported in the immediately preceding article, VCO PLL Frequency Synthesizers for Spacecraft Transponders (NPO- 42909). The reference frequency for a PLL-based frequency synthesizer is derived from a numerically controlled oscillator (NCO) implemented in digital logic, such that almost any reference frequency can be derived from a fixed crystal reference oscillator with microhertz precision. The frequency of the NCO is adjusted to track the received signal, then used to create another NCO frequency used to synthesize the transmitted signal coherent with, and at a specified frequency ratio to, the received signal. The frequencies can be changed, even during operation, through suitable digital programming. The NCOs and the related tracking loops and coherent turnaround logic are implemented in a field-programmable gate array (FPGA). The interface between the analog microwave receiver and transmitter circuits and the FPGA includes analog-to-digital and digital-toanalog converters, the sampling rates of which are chosen to minimize spurious signals and otherwise optimize performance. Several mixers and filters are used to properly route various signals.
This paper presents the open source runtime verification tool MESA (MEssage-based System Analysis), implemented in Scala, which supports concurrent monitors using the Actor model. Furthermore, the tool supports indexing (slicing) on the data values occurring in data-carrying events, for each individual monitor. The tool is generic in the sense that any monitoring system can be used for creating monitors. In this paper, we use the internal Scala DSL Daut for programming such in data parameterized state machines and temporal logic. To illustrate MESA/Daut, we present a case study that monitors flights from live U.S. airspace data streams, verifying that they conform to planned routes. With base in the case study, we then perform an extensive empirical study of the potential benefits from monitoring slices of a single property in concurrently executing actors. Due to the overhead of scheduling “small” actors (one for each slice or a small number of slices), it is not obvious that concurrent execution of such is beneficial. However, as a main result, we demonstrate that concurrent monitoring of slices to handle data-carrying events can provide considerable speed gains.
A document intended to serve as a User's Manual and a Programmer's Manual for the Mask Analysis Program is presented. The first portion of the document is devoted to the user. It contains all of the information required to execute MAP. The remainder of the document describes the details of MAP software logic. Although the information in this portion is not required to run the program, it is recommended that every user review it to gain an appreciation for the program functions.
A generalized covariance analysis technique which permits the study of the sensitivity of linear estimation algorithms to errors in a priori statistics has been developed and programed. Several sample cases are presented to illustrate the use of this technique. Modifications to the Simulated Trajectories Error Analysis Program (STEAP) to enable targeting a multiprobe mission of the Planetary Explorer type are discussed. The logic for the mini-probe targeting is presented. Finally, the initial phases of the conversion of the Viking mission Lander Trajectory Reconstruction (LTR) program for use on Venus missions is discussed. An integrator instability problem is discussed and a solution proposed.
The LSI standard cell array technique was used in the fabrication of more than 20 CMOS custom arrays. This technique consists of a series of computer programs and design automation techniques referred to as the Computer Aided Design And Test (CADAT) system that automatically translate a partitioned logic diagram into a set of instructions for driving an automatic plotter which generates precision mask artwork for complex LSI arrays of CMOS standard cells. The standard cell concept for producing LSI arrays begins with the design, layout, and validation of a group of custom circuits called standard cells. Once validated, these cells are given identification or pattern numbers and are permanently stored. To use one of these cells in a logic design, the user calls for the desired cell by pattern number. The Place, Route in Two Dimension (PR2D) computer program is then used to automatically generate the metalization and/or tunnels to interconnect the standard cells into the required function. Data sheets that describe the function, artwork, and performance of each of the standard cells, the general procedure for implementation of logic in CMOS standard cells, and additional detailed design information are presented.
We propose a hierarchical architecture for building “logical” Majorana zero modes using “physical” Majorana zero modes at the Y-junctions of a hexagonal network of semiconductor nanowires. Each Y-junction contains three “physical” Majoranas, which hybridize when placed in close proximity, yielding a single effective Majorana mode near zero energy. The hybridization of effective Majorana modes on neighboring Y-junctions is controlled by applied gate voltages on the links of the honeycomb network. This gives rise to a tunable tight-binding model of effective Majorana modes. We show that selecting the gate voltages that generate a Kekule vortex pattern in the set of hybridization amplitudes yields an emergent “logical” Majorana zero mode bound to the vortex core. The position of a logical Majorana can be tuned adiabatically, without moving any of the “physical” Majoranas or closing any energy gaps, by programming the values of the gate voltages to change as functions of time. Furthermore, a nanowire network supporting multiple such “logical” Majorana zero modes provides a physical platform for performing adiabatic non-Abelian braiding operations in a fully controllable manner.
Differential dynamic logic is a formal framework to specify and reason about hybrid programs (HPs). The core of dL is a proof calculus that contains a collection of axioms and rules for the rigorous verification of properties of HPs. Recently, dL has been embedded within the theorem prover Prototype Verification System (PVS) resulting in the tool Plaidypvs2. The integration of dL into PVS expands its expressive power; user defined functions, such as trigonometric and other transcendental functions, can be used inside the dL framework, and meta-reasoning about HPs can be performed, including reasoning about entire classes of HPs, specified using dependent types in PVS. The differential temporal dynamic logic (dTL2) extends dL with temporal logic operators to reason about all the states reachable during the execution of an HP. This paper presents a work in progress focusing on embedding dTL2 in PVS as an extension of Plaidypvs. Plaidypvs is expanded with the formalization of a trace semantics for HPs, the definition of the LTL temporal operators eventually and globally, and the implementation of the proof calculus for dTL2. This new embedding has the same capabilties as Plaidypvs, which allows user defined functions and meta-reasoning of properties of HPs. To the best of the authors’ knowledge this is the first implementation of dTL2.