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.

SourceResearch connectionFrom yearThrough year

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

At least 55 records · Page 3

All sources NASA NTRS DOE OSTI

NASA NTRSDate not supplied

SafeDNN: Understanding and Verifying Neural Networks

The SafeDNN project at NASA Ames explores analysis techniques and tools to ensure that systems that use Deep Neural Networks (DNN) are safe, robust and interpretable. Research directions we are pursuing include: symbolic execution for DNN analysis, label-guided clustering to automatically identify input regions that are robust, parallel and compositional approaches to improve formal SMT-based verification, property inference and automated program repair for DNNs, adversarial training and detection, probabilistic reasoning for DNNs. In this talk I will highlight some of the research advances from SafeDNN, that were already published.

Corina Pasareanu↗

NASA NTRS2011

Symbolically Modeling Concurrent MCAPI Executions

Improper use of Inter-Process Communication (IPC) within concurrent systems often creates data races which can lead to bugs that are challenging to discover. Techniques that use Satisfiability Modulo Theories (SMT) problems to symbolically model possible executions of concurrent software have recently been proposed for use in the formal verification of software. In this work we describe a new technique for modeling executions of concurrent software that use a message passing API called MCAPI. Our technique uses an execution trace to create an SMT problem that symbolically models all possible concurrent executions and follows the same sequence of conditional branch outcomes as the provided execution trace. We check if there exists a satisfying assignment to the SMT problem with respect to specific safety properties. If such an assignment exists, it provides the conditions that lead to the violation of the property. We show how our method models behaviors of MCAPI applications that are ignored in previously published techniques.

Fischer, Topher↗

NASA NTRS2007

Decision-Tree Formulation With Order-1 Lateral Execution

A compact symbolic formulation enables mapping of an arbitrarily complex decision tree of a certain type into a highly computationally efficient multidimensional software object. The type of decision trees to which this formulation applies is that known in the art as the Boolean class of balanced decision trees. Parallel lateral slices of an object created by means of this formulation can be executed in constant time considerably less time than would otherwise be required. Decision trees of various forms are incorporated into almost all large software systems. A decision tree is a way of hierarchically solving a problem, proceeding through a set of true/false responses to a conclusion. By definition, a decision tree has a tree-like structure, wherein each internal node denotes a test on an attribute, each branch from an internal node represents an outcome of a test, and leaf nodes represent classes or class distributions that, in turn represent possible conclusions. The drawback of decision trees is that execution of them can be computationally expensive (and, hence, time-consuming) because each non-leaf node must be examined to determine whether to progress deeper into a tree structure or to examine an alternative. The present formulation was conceived as an efficient means of representing a decision tree and executing it in as little time as possible. The formulation involves the use of a set of symbolic algorithms to transform a decision tree into a multi-dimensional object, the rank of which equals the number of lateral non-leaf nodes. The tree can then be executed in constant time by means of an order-one table lookup. The sequence of operations performed by the algorithms is summarized as follows: 1. Determination of whether the tree under consideration can be encoded by means of this formulation. 2. Extraction of decision variables. 3. Symbolic optimization of the decision tree to minimize its form. 4. Expansion and transformation of all nested conjunctive-disjunctive paths to a flattened conjunctive form composed only of equality checks when possible. If each reduced conjunctive form contains only equality checks and all of these forms use the same variables, then the decision tree can be reduced to an order-one operation through a table lookup. The speedup to order one is accomplished by distributing each decision variable over a surface of a multidimensional object by mapping the equality constant to an index

James, Mark↗

NASA NTRSDate not supplied

On the Probabilistic Analysis of Neural Networks

Neural networks are powerful tools for automated decision-making,seeing increased application in safety-critical domains, such as autonomous driving. Due to their black-box nature and large scale,reasoning about their behavior is challenging. Statistical analysis is often used to infer probabilistic properties of a network, such as its robustness to noise and inaccurate inputs. While scalable, statistical methods can only provide probabilistic guarantees on the quality of their results and may underestimate the impact of low probability inputs leading to undesired behavior of the network.We investigate here the use of symbolic analysis and constraint solution space quantification to precisely quantify probabilistic properties in neural networks. We demonstrate the potential of the proposed technique in a case study involving the analysis of ACAS-Xu, a collision avoidance system for unmanned aircraft control.

neural nets↗

NASA NTRS1990

Evolution and advanced technology

The NASREM architecture with its standard interfaces permits development and evolution of the Flight Telerobotic Servicer to greater autonomy. Technologies in control strategies for an arm with seven DOF, including a safety system containing skin sensors for obstacle avoidance, are being developed. Planning and robotic execution software includes symbolic task planning, world model data bases, and path planning algorithms. Research over the last five years has led to the development of laser scanning and ranging systems, which use coherent semiconductor laser diodes for short range sensing. The possibility of using a robot to autonomously assemble space structures is being investigated. A control framework compatible with NASREM is being developed that allows direct global control of the manipulator. Researchers are developing systems that permit an operator to quickly reconfigure the telerobot to do new tasks safely.

Ollendorf, Stanford↗

NASA NTRS2006

Symbolic Constraint Maintenance Grid

Version 3.1 of Symbolic Constraint Maintenance Grid (SCMG) is a software system that provides a general conceptual framework for utilizing pre-existing programming techniques to perform symbolic transformations of data. SCMG also provides a language (and an associated communication method and protocol) for representing constraints on the original non-symbolic data. SCMG provides a facility for exchanging information between numeric and symbolic components without knowing the details of the components themselves. In essence, it integrates symbolic software tools (for diagnosis, prognosis, and planning) with non-artificial-intelligence software. SCMG executes a process of symbolic summarization and monitoring of continuous time series data that are being abstractly represented as symbolic templates of information exchange. This summarization process enables such symbolic- reasoning computing systems as artificial- intelligence planning systems to evaluate the significance and effects of channels of data more efficiently than would otherwise be possible. As a result of the increased efficiency in representation, reasoning software can monitor more channels and is thus able to perform monitoring and control functions more effectively.

James, Mark↗

NASA NTRS1977

Proving the correctness of the flight director program EADIFD, volume 1

EADIFD is written in symbolic assembly language for execution on the C4000 airborne computer. It is a subprogram of an aircraft navigation and guidance program and is used to generate pitch and roll command signals for use in terminal airspace. The proof of EADIFD was carried out by an inductive assertion method consisting of two parts, a verification condition generator and a source language independent proof checker. With the specifications provided by NASA, EADIFD was proved correct. The termination of the program is guaranteed and the program contains no instructions that can modify it under any conditions.

Lee, F. J.↗

NASA NTRS1980

Automated flow-chart system

Program produces flow chart of any program written in FORTRAN. Each FORTRAN statement is printed with symbol representing actions required during execution. Flow chart is generated on line-printer. This program is in COBOL for batch execution on IBM 370-series computer.

Woodford, W.↗

NASA NTRS1992

Digital tracking loops for a programmable digital modem

In this paper, an analysis and hardware emulation of the tracking loops for a very flexible programmable digital modem (PDM) will be presented. The modem is capable of being programmed for 2, 4, 8, 16-PSK, 16-QAM, MSK, and Offset-QPSK modulation schemes over a range of data rates from 2.34 to 300 Mbps with programmable spectral occupancy from 1.2 to 1.8 times the symbol rate; these operational parameters are executable in burst or continuous mode. All of the critical processing in both the modulator and demodulator is done at baseband with very high-speed digital hardware and memory. Quadrature analog front-ends are used for translation between baseband and the IF center frequency. The modulator is based on a table lookup approach, where precomputed samples are stored in memory and clocked out according to the incoming data pattern. The sample values are predistorted to counteract the effects of the other filtering functions in the link as well as any transmission impairments. The demodulator architecture was adapted from a joint estimator-detector (JED) mathematical analysis. Its structure is applicable to most signalling formats that can be represented in a two-dimensional space. The JED realization uses interdependent, mutually aiding tracking loops with post-detection data feedback. To expedite and provide for more reliable synchronization, initial estimates for these loops are computed in a parallel acquisition processor. The cornerstone of the demodulator realization is the pre-averager received data filter which allows operation over a broad range of data rates without any hardware changes and greatly simplifies the implementation complexity. The emulation results confirmed tracking loop operation over the entire range of operational parameters listed above, as well as the capability of achieving and maintaining synchronization at BER's in excess of 10(exp -1). The emulation results also showed very close agreement with the tracking loop analysis, and validated the resolution apportionment of the various hardware elements in the tracking loops.

Poklemba, John J.↗

NASA NTRS1990

Run-time parallelization and scheduling of loops

Run time methods are studied to automatically parallelize and schedule iterations of a do loop in certain cases, where compile-time information is inadequate. The methods presented involve execution time preprocessing of the loop. At compile-time, these methods set up the framework for performing a loop dependency analysis. At run time, wave fronts of concurrently executable loop iterations are identified. Using this wavefront information, loop iterations are reordered for increased parallelism. Symbolic transformation rules are used to produce: inspector procedures that perform execution time preprocessing and executors or transformed versions of source code loop structures. These transformed loop structures carry out the calculations planned in the inspector procedures. Performance results are presented from experiments conducted on the Encore Multimax. These results illustrate that run time reordering of loop indices can have a significant impact on performance. Furthermore, the overheads associated with this type of reordering are amortized when the loop is executed several times with the same dependency structure.

Saltz, Joel H.↗

NASA NTRS1991

Run-time parallelization and scheduling of loops

Run-time methods are studied to automatically parallelize and schedule iterations of a do loop in certain cases where compile-time information is inadequate. The methods presented involve execution time preprocessing of the loop. At compile-time, these methods set up the framework for performing a loop dependency analysis. At run-time, wavefronts of concurrently executable loop iterations are identified. Using this wavefront information, loop iterations are reordered for increased parallelism. Symbolic transformation rules are used to produce: inspector procedures that perform execution time preprocessing, and executors or transformed versions of source code loop structures. These transformed loop structures carry out the calculations planned in the inspector procedures. Performance results are presented from experiments conducted on the Encore Multimax. These results illustrate that run-time reordering of loop indexes can have a significant impact on performance.

Saltz, Joel H.↗

NASA NTRS1987

Execution environment for intelligent real-time control systems

Modern telerobot control technology requires the integration of symbolic and non-symbolic programming techniques, different models of parallel computations, and various programming paradigms. The Multigraph Architecture, which has been developed for the implementation of intelligent real-time control systems is described. The layered architecture includes specific computational models, integrated execution environment and various high-level tools. A special feature of the architecture is the tight coupling between the symbolic and non-symbolic computations. It supports not only a data interface, but also the integration of the control structures in a parallel computing environment.

Sztipanovits, Janos↗

NASA NTRS1990

Concurrent Image Processing Executive (CIPE). Volume 3: User's guide

CIPE (the Concurrent Image Processing Executive) is both an executive which organizes the parameter inputs for hypercube applications and an environment which provides temporary data workspace and simple real-time function definition facilities for image analysis. CIPE provides two types of user interface. The Command Line Interface (CLI) provides a simple command-driven environment allowing interactive function definition and evaluation of algebraic expressions. The menu interface employs a hierarchical screen-oriented menu system where the user is led through a menu tree to any specific application and then given a formatted panel screen for parameter entry. How to initialize the system through the setup function, how to read data into CIPE symbols, how to manipulate and display data through the use of executive functions, and how to run an application in either user interface mode, are described.

Lee, Meemong↗

NASA NTRS1991

Programmable digital modem

The design of the Programmable Digital Modem (PDM) is outlined. The PDM will be capable of operating with numerous modulation techniques including: 2-, 4-, 8- and 16-ary phase shift keying (PSK), minimum shift keying (MSK), and 16-ary quadrature amplitude modulation (QAM), with spectral occupancy from 1.2x to 2x the data symbol rate. It will also be programmable for transmission rates ranging from 2.34 to 300 Mbit/s, where the maximum symbol rate is 75 Msymbol/s. Furthermore, these parameters will be executable in independent burst, dependent burst, or continuous mode. In dependent burst mode the carrier and clock oscillator sources are common from burst to burst. To achieve as broad a set of requirements as these, it is clear that the essential signal processing must be digital. In addition, to avoid hardware changes when the operational parameters are changed, a fixed interface to an analog intermediate frequency (IF) is necessary for transmission; and, common system level architectures are necessary for the modulator and demodulator. Lastly, to minimize size and power, as much of the design as possible will be implemented with application specific integrated circuit (ASIC) chips.

Poklemba, John J.↗

NASA NTRS2009

A Comparative Study of Randomized Constraint Solvers for Random-Symbolic Testing

The complexity of constraints is a major obstacle for constraint-based software verification. Automatic constraint solvers are fundamentally incomplete: input constraints often build on some undecidable theory or some theory the solver does not support. This paper proposes and evaluates several randomized solvers to address this issue. We compare the effectiveness of a symbolic solver (CVC3), a random solver, three hybrid solvers (i.e., mix of random and symbolic), and two heuristic search solvers. We evaluate the solvers on two benchmarks: one consisting of manually generated constraints and another generated with a concolic execution of 8 subjects. In addition to fully decidable constraints, the benchmarks include constraints with non-linear integer arithmetic, integer modulo and division, bitwise arithmetic, and floating-point arithmetic. As expected symbolic solving (in particular, CVC3) subsumes the other solvers for the concolic execution of subjects that only generate decidable constraints. For the remaining subjects the solvers are complementary.

Takaki, Mitsuo↗

NASA NTRS1990

Automating symbolic analysis with CLIPS

Symbolic Analysis is a methodology first applied as an aid in selecting and generating test cases for 'white box' type testing of computer software programs. The feasibility of automating this analysis process has recently been demonstrated through the development of a CLIPS-based prototype tool. Symbolic analysis is based on separating the logic flow diagram of a computer program into its basic elements, and then systematically examining those elements and their relationships to provide a detailed static analysis of the process that those diagrams represent. The basic logic flow diagram elements are flow structure (connections), predicates (decisions), and computations (actions). The symbolic analysis approach supplies a disciplined step-by-step process to identify all executable program paths and produce a truth table that defines the input and output domains for each path identified. The resulting truth table is the tool that allows software test cases to be generated in a comprehensive manner to achieve total program path, input domain, and output domain coverage. Since the manual application of symbolic analysis is extremely labor intensive and is itself error prone, automation of the process is highly desirable. Earlier attempts at automation, utilizing conventional software approaches, had only limited success. This paper briefly describes the automation problems, the symbolic analysis expert's problem solving heuristics, and the implementation of those heuristics as a CLIPS based prototype, and the manual augmentation required. A simple application example is also provided for illustration purposes. The paper concludes with a discussion of implementation experiences, automation limitations, usage experiences, and future development suggestions.

Morris, Keith E.↗

NASA NTRS2011

Symbol Tables and Branch Tables: Linking Applications Together

This document explores the computer techniques used to execute software whose parts are compiled and linked separately. The computer techniques include using a branch table or indirect address table to connect the parts. Methods of storing the information in data structures are discussed as well as differences between C and C++.

Handler, Louis M.↗

NASA NTRS1991

Parallel processing and expert systems

Whether it be monitoring the thermal subsystem of Space Station Freedom, or controlling the navigation of the autonomous rover on Mars, NASA missions in the 1990s cannot enjoy an increased level of autonomy without the efficient implementation of expert systems. Merely increasing the computational speed of uniprocessors may not be able to guarantee that real-time demands are met for larger systems. Speedup via parallel processing must be pursued alongside the optimization of sequential implementations. Prototypes of parallel expert systems have been built at universities and industrial laboratories in the U.S. and Japan. The state-of-the-art research in progress related to parallel execution of expert systems is surveyed. The survey discusses multiprocessors for expert systems, parallel languages for symbolic computations, and mapping expert systems to multiprocessors. Results to date indicate that the parallelism achieved for these systems is small. The main reasons are (1) the body of knowledge applicable in any given situation and the amount of computation executed by each rule firing are small, (2) dividing the problem solving process into relatively independent partitions is difficult, and (3) implementation decisions that enable expert systems to be incrementally refined hamper compile-time optimization. In order to obtain greater speedups, data parallelism and application parallelism must be exploited.

Lau, Sonie↗