Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Symbolic Execution”

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 91 records · Page 5

Toward Automatic Scalability Analysis of Message Passing Programs: A Case Study

Scalability analysis forms an important component of any performance debugging cycle, for massively parallel machines. However, tools that help in performing such analysis for parallel programs are non-existent. The primary reason for lack of such tools is the complexity involved in capturing program dynamics such as communication-computation overlap, communication latencies and memory hierarchy reference patterns. In this paper, we highlight some simple techniques that can be used to study scalability of explicit message-passing parallel programs that consider the above issues. We start from the high level source code and use a methodology for deducing communication characteristics and its impact on the total execution time of the program. The approach is validated with the help of a pipelined method for solving scalar tri-diagonal systems, using both simulations and symbolic cost models on the Intel hypercube.

Sarukkai, Sekhar R.↗

Theorem Proving in Intel Hardware Design

For the past decade, a framework combining model checking (symbolic trajectory evaluation) and higher-order logic theorem proving has been in production use at Intel. Our tools and methodology have been used to formally verify execution cluster functionality (including floating-point operations) for a number of Intel products, including the Pentium(Registered TradeMark)4 and Core(TradeMark)i7 processors. Hardware verification in 2009 is much more challenging than it was in 1999 - today s CPU chip designs contain many processor cores and significant firmware content. This talk will attempt to distill the lessons learned over the past ten years, discuss how they apply to today s problems, outline some future directions.

O'Leary, John↗

SNAP: A computer program for generating symbolic network functions

The computer program SNAP (symbolic network analysis program) generates symbolic network functions for networks containing R, L, and C type elements and all four types of controlled sources. The program is efficient with respect to program storage and execution time. A discussion of the basic algorithms is presented, together with user's and programmer's guides.

Lin, P. M.↗

Working Notes from the 1992 AAAI Spring Symposium on Practical Approaches to Scheduling and Planning

The symposium presented issues involved in the development of scheduling systems that can deal with resource and time limitations. To qualify, a system must be implemented and tested to some degree on non-trivial problems (ideally, on real-world problems). However, a system need not be fully deployed to qualify. Systems that schedule actions in terms of metric time constraints typically represent and reason about an external numeric clock or calendar and can be contrasted with those systems that represent time purely symbolically. The following topics are discussed: integrating planning and scheduling; integrating symbolic goals and numerical utilities; managing uncertainty; incremental rescheduling; managing limited computation time; anytime scheduling and planning algorithms, systems; dependency analysis and schedule reuse; management of schedule and plan execution; and incorporation of discrete event techniques.

Drummond, Mark↗

The scheme machine: A case study in progress in design derivation at system levels

The Scheme Machine is one of several design projects of the Digital Design Derivation group at Indiana University. It differs from the other projects in its focus on issues of system design and its connection to surrounding research in programming language semantics, compiler construction, and programming methodology underway at Indiana and elsewhere. The genesis of the project dates to the early 1980's, when digital design derivation research branched from the surrounding research effort in programming languages. Both branches have continued to develop in parallel, with this particular project serving as a bridge. However, by 1990 there remained little real interaction between the branches and recently we have undertaken to reintegrate them. On the software side, researchers have refined a mathematically rigorous (but not mechanized) treatment starting with the fully abstract semantic definition of Scheme and resulting in an efficient implementation consisting of a compiler and virtual machine model, the latter typically realized with a general purpose microprocessor. The derivation includes a number of sophisticated factorizations and representations and is also deep example of the underlying engineering methodology. The hardware research has created a mechanized algebra supporting the tedious and massive transformations often seen at lower levels of design. This work has progressed to the point that large scale devices, such as processors, can be derived from first-order finite state machine specifications. This is roughly where the language oriented research stops; thus, together, the two efforts establish a thread from the highest levels of abstract specification to detailed digital implementation. The Scheme Machine project challenges hardware derivation research in several ways, although the individual components of the system are of a similar scale to those we have worked with before. The machine has a custom dual-ported memory to support garbage collection. It consists of four tightly coupled processes--processor, collector, allocator, memory--with a very non-trivial synchronization relationship. Finally, there are deep issues of representation for the run-time objects of a symbolic processing language. The research centers on verification through integrated formal reasoning systems, but is also involved with modeling and prototyping environments. Since the derivation algebra is basd on an executable modeling language, there is opportunity to incorporate design animation in the design process. We are looking for ways to move smoothly and incrementally from executable specifications into hardware realization. For example, we can run the garbage collector specification, a Scheme program, directly against the physical memory prototype, and similarly, the instruction processor model against the heap implementation.

Johnson, Steven D.↗

Synthesizing information-update functions using off-line symbolic processing

This paper explores the synthesis of programs that track dynamic conditions in their environment. An approach is proposed in which the designer specifies, in a declarative language, aspects of the environment in which the program will be embedded. This specification is then automatically compiled into a program that, when executed, updates internal data structures so as to maintain as an invariant a desired correspondence between internal data structures and states of the external environment. This approach retains much of the flexibility of declarative programming while guaranteeing a hard bound on the execution time of information-update functions.

Rosenschein, Stanley J.↗

Assessments of Physiology and Cognition in Hybrid-Reality Environments (APACHE)

NASA is planning to return to the Moon in the mid-2020s as a stepping stone to Mars missions in the 2030s. Spacewalks, or extravehicular activities (EVAs), performed on the Moon and Mars will differ in a variety of ways from those that have been performed in decades past. NASA has identified multiple risks to human health and performance associated with a crewed mission to Mars, especially those associated with exploration EVAs which are expected to be a primary mission activity. Crew may be expected to conduct up to 24 hours of EVA per person per week, where the likelihood of injury and/or mental mistakes are increased compared to ground-based training or current microgravity EVAs and the consequences of which can be catastrophic. Current test environments for exploration EVA research and technology development are large, costly facilities that are limited in their availability or capabilities. Spacesuit testing in a reduced gravity environment such as NASA’s Neutral Buoyancy Laboratory, while a good representation of the crew’s physical workload during exploration EVAs, typically has small datasets and is difficult to integrate physiological sensors or other types of crew performance measures. Meanwhile, scientific field-based testing such as NASA’s Desert Research and Technology Studies offers an operationally relevant environment for exploration EVAs, particularly for cognitive workload, but is also limited by small datasets, lack of a pressurized spacesuit, and obtrusive measures. The limitations of current analogs for exploration EVAs identify a need for a new test environment that can approximate both the physical and cognitive demands associated with exploration EVAs to enable rapid, controlled, and repeatable evaluations of human health and performance risks of exploration missions. In response, the Human Physiology, Performance, Protection, and Operations Laboratory (H-3PO) at NASA Johnson Space Center has developed a hybrid reality exploration EVA analog named the Assessments of Physiology And Cognition in Hybrid-reality Environments (APACHE) to address these limitations using a combination of virtual, physical, and hybrid reality techniques. The APACHE facility resides at NASA Johnson Space Center and serves as a large “sandbox” for EVA research and simulation. At its center is a roughly 15x20ft space surrounded by a 14” tall sandbox partially filled with lunar regolith simulant to emulate the physical feeling of walking on a planetary surface and to allow for simulated geology operations. Nearby, a curved passive treadmill (Skillmill Connect, Technogym, Fairfield, NJ) and an omnidirectional treadmill (Infinadeck, Infinadeck, Rocklin, CA) are included to enable exploration of these large virtual environments while also imposing the physical demands, representative timelines, and cognitive burdens required to navigate and traverse these distances during exploration EVA. A 6DOF motion platform is used to simulate rover operations and supports various human performance evaluations and associated risks. Lastly, APACHE can support two extravehicular (EV) crewmembers working in tandem. A computer workstation is located nearby and also supports an intravehicular (IV) crewmember as part of a full mission simulation. The IV crewmember has direct video and audio communication with the EV crew in VR to provide operational and procedural support. The software used in APACHE was created by the JSC Engineering Directorate, in partnership with Buendea, powered by a custom Unreal Engine 5 (UE5.3, Epic Games) project. APACHE currently utilizes the HTC Vive Pro Eye in a wireless configuration for VR simulations. There are two virtual environments that subjects can explore within APACHE, a Lunar and Martian surface. The virtual Lunar surface was created from LIDAR data of the Lunar South Pole to create roughly 16 sq km of explorable terrain. The virtual Martian surface contains roughly 400 sq km of explorable terrain derived from Mars Reconnaissance Orbiter LIDAR data of the Jezero Crater. The immersion and related cognitive burdens of conducting a planetary EVA is simulated through a series of EVA-relevant tasks performed in the VR environment, using these high-fidelity visual representations. Additionally, APACHE includes biosensor driven informatics, such as real-time heart rate monitoring and/or derived values from model simulations, for active monitoring by the EV crew and added cognitive demand. A “Wizard of Oz” control panel enables test operators to activate contingency events such as simulated spacesuit malfunctions, loss of communications, and/or limited visibility. Embedded performance measures such as accuracy, completeness, and execution time have been developed for various exploration tasks to objectively quantify crew performance during an EVA and compare impacts to performance when different environmental stressors, both physical and cognitive, are added to or removed from the simulation. Additionally, validated cognitive and operational performance measures such as the Digit Symbol Substitution Task have been recreated and embedded in VR for direct and relatively unobtrusive measurement of motor perception. The APACHE environment currently supports multiple research studies at NASA. Examples include the CHAPEA project, a series of simulated year-long missions on Mars by a 4-person crew; and the CO2 Contingency Walk Back Study, an investigation of elevated CO2 exposure on crew performance during a contingency EVA scenario. APACHE also provides a test environment to support the development of the Crew State and Risk Model, which is a collection of individualized, mathematical models of crew physical and cognitive state; and the Personalized EVA Informatics and Decision Support system, an operational tool for flight controllers, and eventually a self-reliant Martian crew, to make biomedically-informed decisions in real-time to optimize the EVA planning and execution with respect to crew health and performance. Some technical challenges associated with developing the APACHE environment, as well as current limitations, include VR limitless natural walking with a hybrid spacesuit simulator, optimizing performance for wireless PC VR streaming while maintaining a high degree of visual fidelity, and the integration of various physiological (metabolic masks) and psychometric (eye tracking) sensors with the VR headset.

Human Performance↗

On-orbit flight control algorithm description

Algorithms are presented for rotational and translational control of the space shuttle orbiter in the orbital mission phases, which are external tank separation, orbit insertion, on-orbit and de-orbit. The program provides a versatile control system structure while maintaining uniform communications with other programs, sensors, and control effectors by using an executive routine/functional subroutine format. Software functional requirements are described using block diagrams where feasible, and input--output tables, and the software implementation of each function is presented in equations and structured flow charts. Included are a glossary of all symbols used to define the requirements, and an appendix of supportive material.

Source record↗

SYMBOD - A computer program for the automatic generation of symbolic equations of motion for systems of hinge-connected rigid bodies

A computer program is described that can automatically generate symbolic equations of motion for systems of hinge-connected rigid bodies with tree topologies. The dynamical formulation underlying the program is outlined, and examples are given to show how a symbolic language is used to code the formulation. The program is applied to generate the equations of motion for a four-body model of the Galileo spacecraft. The resulting equations are shown to be a factor of three faster in execution time than conventional numerical subroutines.

Macala, G. A.↗

Knowledge-based reasoning in the Paladin tactical decision generation system

A real-time tactical decision generation system for air combat engagements, Paladin, has been developed. A pilot's job in air combat includes tasks that are largely symbolic. These symbolic tasks are generally performed through the application of experience and training (i.e. knowledge) gathered over years of flying a fighter aircraft. Two such tasks, situation assessment and throttle control, are identified and broken out in Paladin to be handled by specialized knowledge based systems. Knowledge pertaining to these tasks is encoded into rule-bases to provide the foundation for decisions. Paladin uses a custom built inference engine and a partitioned rule-base structure to give these symbolic results in real-time. This paper provides an overview of knowledge-based reasoning systems as a subset of rule-based systems. The knowledge used by Paladin in generating results as well as the system design for real-time execution is discussed.

Chappell, Alan R.↗

AI tools in computer based problem solving

The use of computers to solve value oriented, deterministic, algorithmic problems, has evolved a structured life cycle model of the software process. The symbolic processing techniques used, primarily in research, for solving nondeterministic problems, and those for which an algorithmic solution is unknown, have evolved a different model, much less structured. Traditionally, the two approaches have been used completely independently. With the advent of low cost, high performance 32 bit workstations executing identical software with large minicomputers and mainframes, it became possible to begin to merge both models into a single extended model of computer problem solving. The implementation of such an extended model on a VAX family of micro/mini/mainframe systems is described. Examples in both development and deployment of applications involving a blending of AI and traditional techniques are given.

Beane, Arthur J.↗

Improving and Expanding NASA Software Cost Estimation Methods

Estimators and analysts are increasingly being tasked to develop better models and reliable cost estimates in support of program planning and execution. While there has been extensive work on improving parametric methods for cost estimation, there is very little focus on the use of cost models based on analogy and clustering algorithms. In this paper we summarize the results of our research in developing an analogy method for estimating NASA spacecraft flight software using spectral clustering on system characteristics (symbolic nonnumerical data) and evaluate its performance by comparing it to a number of the most commonly used estimation methods. The strengths and weaknesses of each method based on their performance are also discussed. The paper concludes with an overview of the analogy estimation tool (ASCoT) developed for use within NASA that implements the recommended analogy algorithm.

Hihn, Jairus↗

An Efficient Scheme for Updating Sparse Cholesky Factors

Raghavan had earlier developed the software package DCSPACK which can be used for solving sparse linear systems where the coefficient matrix is symmetric and positive definite (this project was not funded by NASA but by agencies such as NSF). DSCPACK-S is the serial code and DSCPACK-P is a parallel implementation suitable for multiprocessors or networks-of-workstations with message passing using MCI. The main algorithm used is the Cholesky factorization of a sparse symmetric positive positive definite matrix A = LL(T). The code can also compute the factorization A = LDL(T). The complexity of the software arises from several factors relating to the sparsity of the matrix A. A sparse N x N matrix A has typically less that cN nonzeroes where c is a small constant. If the matrix were dense, it would have O(N2) nonzeroes. The most complicated part of such sparse Cholesky factorization relates to fill-in, i.e., zeroes in the original matrix that become nonzeroes in the factor L. An efficient implementation depends to a large extent on complex data structures and on techniques from graph theory to reduce, identify, and manage fill. DSCPACK is based on an efficient multifrontal implementation with fill-managing algorithms and implementation arising from earlier research by Raghavan and others. Sparse Cholesky factorization is typically a four step process: (1) ordering to compute a fill-reducing numbering, (2) symbolic factorization to determine the nonzero structure of L, (3) numeric factorization to compute L, and, (4) triangular solution to solve L(T)x = y and Ly = b. The first two steps are symbolic and are performed using the graph of the matrix. The numeric factorization step is of dominant cost and there are several schemes for improving performance by exploiting the nested and dense structure of groups of columns in the factor. The latter are aimed at better utilization of the cache-memory hierarchy on modem processors to prevent cache-misses and provide execution rates (operations/second) that are close to the peak rates for dense matrix computations. Currently, EPISCOPACY is being used in an application at NASA directed by J. Newman and M. James. We propose the implementation of efficient schemes for updating the LL(T) or LDL(T) factors computed in DSCPACK-S to meet the computational requirements of their project. A brief description is provided in the next section.

Raghavan, Padma↗

Implementing embedded artificial intelligence rules within algorithmic programming languages

Most integrations of artificial intelligence (AI) capabilities with non-AI (usually FORTRAN-based) application programs require the latter to execute separately to run as a subprogram or, at best, as a coroutine, of the AI system. In many cases, this organization is unacceptable; instead, the requirement is for an AI facility that runs in embedded mode; i.e., is called as subprogram by the application program. The design and implementation of a Prolog-based AI capability that can be invoked in embedded mode are described. The significance of this system is twofold: Provision of Prolog-based symbol-manipulation and deduction facilities makes a powerful symbolic reasoning mechanism available to applications programs written in non-AI languages. The power of the deductive and non-procedural descriptive capabilities of Prolog, which allow the user to describe the problem to be solved, rather than the solution, is to a large extent vitiated by the absence of the standard control structures provided by other languages. Embedding invocations of Prolog rule bases in programs written in non-AI languages makes it possible to put Prolog calls inside DO loops and similar control constructs. The resulting merger of non-AI and AI languages thus results in a symbiotic system in which the advantages of both programming systems are retained, and their deficiencies largely remedied.

Feyock, Stefan↗

A Formal Algorithm for Routing Traces on a Printed Circuit Board

This paper addresses the classical problem of printed circuit board routing: that is, the problem of automatic routing by a computer other than by brute force that causes the execution time to grow exponentially as a function of the complexity. Most of the present solutions are either inexpensive but not efficient and fast, or efficient and fast but very costly. Many solutions are proprietary, so not much is written or known about the actual algorithms upon which these solutions are based. This paper presents a formal algorithm for routing traces on a print- ed circuit board. The solution presented is very fast and efficient and for the first time speaks to the question eloquently by way of symbolic statements.

Hedgley, David R., Jr.↗

SOLON: An autonomous vehicle mission planner

The State-Operator Logic Machine (SOLON) Planner provides an architecture for effective real-time planning and replanning for an autonomous vehicle. The highlights of the system, which distinguish it from other AI-based planners that have been designed previously, are its hybrid application of state-driven control architecture and the use of both schematic representations and logic programming for the management of its knowledge base. SOLON is designed to provide multiple levels of planning for a single autonomous vehicle which is supplied with a skeletal, partially-specified mission plan at the outset of the vehicle's operations. This mission plan consists of a set of objectives, each of which will be decomposable by the planner into tasks. These tasks are themselves comparatively complex sets of actions which are executable by a conventional real-time control system which does not perform planning but which is capable of making adjustments or modifications to the provided tasks according to constraints and tolerances provided by the Planner. The current implementation of the SOLON is in the form of a real-time simulation of the Planner module of an Intelligent Vehicle Controller (IVC) on-board an autonomous underwater vehicle (AUV). The simulation is embedded within a larger simulator environment known as ICDS (Intelligent Controller Development System) operating on a Symbolics 3645/75 computer.

Dudziak, M. J.↗

Identifying Trends in Deep Space Network Monitor Data

A computer program has been developed that analyzes Deep Space Network monitor data, looking for changes of trends in critical parameters. This program represents a significant improvement over the previous practice of manually plotting data and visually inspecting the resulting graphs to identify trends. This program uses proven numerical techniques to identify trends. When a statistically significant trend is detected, then it is characterized by means of a symbol that can be used by pre-existing model-based reasoning software. The program can perform any of the following functions: Given an expectation that data in a given list should exhibit an upward, downward, constant, or unknown trend, it can determine whether the data do or do not follow such a trend. Given a list of data, it can identify which of the aforementioned trends the data follow. Given two lists of data, it can determine whether or not both follow the same trend. This program can be executed on a variety of computers. It can be distributed in either source code or binary code form. It must be run in conjunction with any one of a number of Lisp compilers that are available commercially or as shareware.

James, Mark↗

NASA Tech Briefs, August 2008

Customizable Digital Receivers for Radar Two-Camera Acquisition and Tracking of a Flying Target Visual Data Analysis for Satellites A Data Type for Efficient Representation of Other Data Types Hand-Held Ultrasonic Instrument for Reading Matrix Symbols Broadband Microstrip-to-Coplanar Strip Double-Y Balun A Topographical Lidar System for Terrain-Relative Navigation Programmable Low-Voltage Circuit Breaker and Tester Electronic Switch Arrays for Managing Microbattery Arrays Topics covered include: Lower-Dark-Current, Higher-Blue-Response CMOS Imagers; Fabricating Large-Area Sheets of Single-Layer Graphene by CVD; Support for Diagnosis of Custom Computer Hardware; Providing Goal-Based Autonomy for Commanding a Spacecraft; Dynamic Method for Identifying Collected Sample Mass; Optimal Planning and Problem-Solving; Attitude-Control Algorithm for Minimizing Maneuver Execution Errors; Grants Document-Generation System; Heat-Storage Modules Containing LiNO3 3H2O and Graphite Foam; Precipitation-Strengthened, High-Temperature, High-Force Shape Memory Alloys; Improved Relief Valve Would Be Less Susceptible to Failure; Safety Modification of Cam-and-Groove Hose Coupling; Using Composite Materials in a Cryogenic Pump; Using Electronic Noses to Detect Tumors During Neurosurgery; Producing Newborn Synchronous Mammalian Cells; Smaller, Lower-Power Fast-Neutron Scintillation Detectors; Rotationally Vibrating Electric-Field Mill; Estimating Hardness from the USDC Tool-Bit Temperature Rise; Particle-Charge Spectrometer; Automated Production of Movies on a Cluster of Computers; FIDO-Class Development Rover; and Tone-Based Command of Deep Space Probes Using Ground Antennas.

Source record↗