Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Static analysis”

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 217 records · Page 12
All sourcesNASA NTRSDOE OSTI
NASA NTRS1990

A generic interface between COSMIC/NASTRAN and PATRAN (R)

Despite its powerful analytical capabilities, COSMIC/NASTRAN lacks adequate post-processing adroitness. PATRAN, on the other hand is widely accepted for its graphical capabilities. A nonproprietary, public domain code mnemonically titled CPI (for COSMIC/NASTRAN-PATRAN Interface) is designed to manipulate a large number of files rapidly and efficiently between the two parent codes. In addition to PATRAN's results file preparation, CPI also prepares PATRAN's P/PLOT data files for xy plotting. The user is prompted for necessary information during an interactive session. Current implementation supports NASTRAN's displacement approach including the following rigid formats: (1) static analysis, (2) normal modal analysis, (3) direct transient response, and (4) modal transient response. A wide variety of data blocks are also supported. Error trapping is given special consideration. A sample session with CPI illustrates its simplicity and ease of use.

Roschke, Paul N.↗
NASA NTRS1990

An improved fully stressed design algorithm for plate/shell structures

The stress-ratio algorithm associated with fully stressed design philosophy has been used as a convenient tool to achieve minimum weight design of strength-limited structures. The algorithm is effective and converges quickly for many cases. However, it presents extremely slow oscillatory iteration histories for plate-thickness design problems that involve transverse bending loads. Modification of the basic algorithm presented in this paper provides an effective remedy to this problem when both membrane and bending loads are present. The modified resizing algorithm requires numerical solutions of a fourth-order algebraic equation. No additional data, beyond the ordinary static analysis results, are required.

Miura, H.↗
NASA NTRS1989

Efficient ICCG on a shared memory multiprocessor

Different approaches are discussed for exploiting parallelism in the ICCG (Incomplete Cholesky Conjugate Gradient) method for solving large sparse symmetric positive definite systems of equations on a shared memory parallel computer. Techniques for efficiently solving triangular systems and computing sparse matrix-vector products are explored. Three methods for scheduling the tasks in solving triangular systems are implemented on the Sequent Balance 21000. Sample problems that are representative of a large class of problems solved using iterative methods are used. We show that a static analysis to determine data dependences in the triangular solve can greatly improve its parallel efficiency. We also show that ignoring symmetry and storing the whole matrix can reduce solution time substantially.

Hammond, Steven W.↗
NASA NTRS1992

Split torque transmission load sharing

Split torque transmissions are attractive alternatives to conventional planetary designs for helicopter transmissions. The split torque designs can offer lighter weight and fewer parts but have not been used extensively for lack of experience, especially with obtaining proper load sharing. Two split torque designs that use different load sharing methods have been studied. Precise indexing and alignment of the geartrain to produce acceptable load sharing has been demonstrated. An elastomeric torque splitter that has large torsional compliance and damping produces even better load sharing while reducing dynamic transmission error and noise. However, the elastomeric torque splitter as now configured is not capable over the full range of operating conditions of a fielded system. A thrust balancing load sharing device was evaluated. Friction forces that oppose the motion of the balance mechanism are significant. A static analysis suggests increasing the helix angle of the input pinion of the thrust balancing design. Also, dynamic analysis of this design predicts good load sharing and significant torsional response to accumulative pitch errors of the gears.

Krantz, T. L.↗
NASA NTRS1992

Structural optimization of thin shells using finite element method

The objective of the present work was the structural optimization of thin shell structures that are subjected to stress and displacement constraints. In order to accomplish this, the structural optimization computer program DESAP1 was modified and improved. In the static analysis part of the DESAP1 computer program the torsional spring elements, which are used to analyze thin, shallow shell structures, were eliminated by modifying the membrane stiffness matrix of the triangular elements in the local coordinate system and adding a fictitious rotational stiffness matrix. This simplified the DESAP1 program input, improved the accuracy of the analysis, and saved computation time. In the optimization part of the DESAP1 program the stress ratio formula, which redesigns the thickness of each finite element of the structure, was solved by an analytical method. This scheme replaced the iterative solution that was previously used in the DESAP1 program, thus increasing the accuracy and speed of the design. The modified program was used to design a thin, cylindrical shell structure with optimum weight, and the results are reported in this paper.

Gotsis, Pascal K.↗
NASA NTRS1992

A teleoperation training simulator with visual and kinesthetic force virtual reality

A force-reflecting teleoperation training simulator with a high-fidelity real-time graphics display has been developed for operator training. A novel feature of this simulator is that it enables the operator to feel contact forces and torques through a force-reflecting controller during the execution of the simulated peg-in-hole task, providing the operator with the feel of visual and kinesthetic force virtual reality. A peg-in-hole task is used in our simulated teleoperation trainer as a generic teleoperation task. A quasi-static analysis of a two-dimensional peg-in-hole task model has been extended to a three-dimensional model analysis to compute contact forces and torques for a virtual realization of kinesthetic force feedback. The simulator allows the user to specify force reflection gains and stiffness (compliance) values of the manipulator hand for both the three translational and the three rotational axes in Cartesian space. Three viewing modes are provided for graphics display: single view, two split views, and stereoscopic view.

Kim, Won S.↗
NASA NTRS1993

Integrating interface slicing into software engineering processes

Interface slicing is a tool which was developed to facilitate software engineering. As previously presented, it was described in terms of its techniques and mechanisms. The integration of interface slicing into specific software engineering activities is considered by discussing a number of potential applications of interface slicing. The applications discussed specifically address the problems, issues, or concerns raised in a previous project. Because a complete interface slicer is still under development, these applications must be phrased in future tenses. Nonetheless, the interface slicing techniques which were presented can be implemented using current compiler and static analysis technology. Whether implemented as a standalone tool or as a module in an integrated development or reverse engineering environment, they require analysis no more complex than that required for current system development environments. By contrast, conventional slicing is a methodology which, while showing much promise and intuitive appeal, has yet to be fully implemented in a production language environment despite 12 years of development.

Beck, Jon↗
NASA NTRS1992

An improved plate theory of order (1,2) for thick composite laminates

A new (1,2)-order theory is proposed for the linear elasto-static analysis of laminated composite plates. The basic assumptions are those concerning the distribution through the laminate thickness of the displacements, transverse shear strains and the transverse normal stress, with these quantities regarded as some weighted averages of their exact elasticity theory representations. The displacement expansions are linear for the inplane components and quadratic for the transverse component, whereas the transverse shear strains and transverse normal stress are respectively quadratic and cubic through the thickness. The main distinguishing feature of the theory is that all strain and stress components are expressed in terms of the assumed displacements prior to the application of a variational principle. This is accomplished by an a priori least-square compatibility requirement for the transverse strains and by requiring exact stress boundary conditions at the top and bottom plate surfaces. Equations of equilibrium and associated Poisson boundary conditions are derived from the virtual work principle. It is shown that the theory is particularly suited for finite element discretization as it requires simple C(sup 0)- and C(sup -1)-continuous displacement interpolation fields. Analytic solutions for the problem of cylindrical bending are derived and compared with the exact elasticity solutions and those of our earlier (1,2)-order theory based on the assumed displacements and transverse strains.

Tessler, A.↗
NASA NTRS1999

The Formal Semantics of PVS

A specification language is a medium for expressing what is computed rather than how it is computed. Specification languages share some features with programming languages but are also different in several important ways. For our purpose, a specification language is a logic within which the behavior of computational systems can be formalized. Although a specification can be used to simulate the behavior of such systems, we mainly use specifications to state and prove system properties with mechanical assistance. We present the formal semantics of the specification language of SRI's Prototype Verification System (PVS). This specification language is based on the simply typed lambda calculus. The novelty in PVS is that it contains very expressive language features whose static analysis (e.g., typechecking) requires the assistance of a theorem prover. The formal semantics illuminates several of the design considerations underlying PVS, the interaction between theorem proving and typechecking.

Owre, Sam↗
NASA NTRS2001

Examining Reuse in LaSRS++-Based Projects

NASA Langley Research Center (LaRC) developed the Langley Standard Real-Time Simulation in C++ (LaSRS++) to consolidate all software development for its simulation facilities under one common framework. A common framework promised a decrease in the total development effort for a new simulation by encouraging software reuse. To judge the success of LaSRS++ in this regard, reuse metrics were extracted from 11 aircraft models. Three methods that employ static analysis of the code were used to identify the reusable components. For the method that provides the best estimate, reuse levels fall between 66% and 95% indicating a high degree of reuse. Additional metrics provide insight into the extent of the foundation that LaSRS++ provides to new simulation projects. When creating variants of an aircraft, LaRC developers use object-oriented design to manage the aircraft as a reusable resource. Variants modify the aircraft for a research project or embody an alternate configuration of the aircraft. The variants inherit from the aircraft model. The variants use polymorphism to extend or redefine aircraft behaviors to meet the research requirements or to match the alternate configuration. Reuse level metrics were extracted from 10 variants. Reuse levels of aircraft by variants were 60% - 99%.

Madden, Michael M.↗
NASA NTRS2002

Backtracking and Re-execution in the Automatic Debugging of Parallelized Programs

In this work we describe a new approach using relative debugging to find differences in computation between a serial program and a parallel version of th it program. We use a combination of re-execution and backtracking in order to find the first difference in computation that may ultimately lead to an incorrect value that the user has indicated. In our prototype implementation we use static analysis information from a parallelization tool in order to perform the backtracking as well as the mapping required between serial and parallel computations.

Matthews, Gregory↗
NASA NTRS2002

Program Model Checking as a New Trend

This paper introduces a special section of STTT (International Journal on Software Tools for Technology Transfer) containing a selection of papers that were presented at the 7th International SPIN workshop, Stanford, August 30 - September 1, 2000. The workshop was named SPIN Model Checking and Software Verification, with an emphasis on model checking of programs. The paper outlines the motivation for stressing software verification, rather than only design and model verification, by presenting the work done in the Automated Software Engineering group at NASA Ames Research Center within the last 5 years. This includes work in software model checking, testing like technologies and static analysis.

Havelund, Klaus↗
NASA NTRS2003

Design for Verification: Enabling Verification of High Dependability Software-Intensive Systems

Strategies to achieve confidence that high-dependability applications are correctly implemented include testing and automated verification. Testing deals mainly with a limited number of expected execution paths. Verification usually attempts to deal with a larger number of possible execution paths. While the impact of architecture design on testing is well known, its impact on most verification methods is not as well understood. The Design for Verification approach considers verification from the application development perspective, in which system architecture is designed explicitly according to the application's key properties. The D4V-hypothesis is that the same general architecture and design principles that lead to good modularity, extensibility and complexity/functionality ratio can be adapted to overcome some of the constraints on verification tools, such as the production of hand-crafted models and the limits on dynamic and static analysis caused by state space explosion.

Mehlitz, Peter C.↗
NASA NTRS2003

Automatic Relative Debugging of OpenMP Programs

In this work we show how automatic relative debugging can be used to find differences in computation between a serial program and an OpenMP parallel version of that program. Backtracking and re-execution are used to determine the first OpenMP parallel region that produces a difference in computation that may lead to an incorrect value the user has indicated. Tool-parallelized programs are addressed by utilizing static analysis and directive information from the parallelization tool. Manually-parallelized programs are addressed as well by performing data dependence and directive analysis.

Matthews, Gregory↗
NASA NTRS2003

Experimental Evaluation of Verification and Validation Tools on Martian Rover Software

We report on a study to determine the maturity of different verification and validation technologies (V&V) on a representative example of NASA flight software. The study consisted of a controlled experiment where three technologies (static analysis, runtime analysis and model checking) were compared to traditional testing with respect to their ability to find seeded errors in a prototype Mars Rover. What makes this study unique is that it is the first (to the best of our knowledge) to do a controlled experiment to compare formal methods based tools to testing on a realistic industrial-size example where the emphasis was on collecting as much data on the performance of the tools and the participants as possible. The paper includes a description of the Rover code that was analyzed, the tools used as well as a detailed description of the experimental setup and the results. Due to the complexity of setting up the experiment, our results can not be generalized, but we believe it can still serve as a valuable point of reference for future studies of this kind. It did confirm the belief we had that advanced tools can outperform testing when trying to locate concurrency errors. Furthermore the results of the experiment inspired a novel framework for testing the next generation of the Rover.

Brat, Guillaume↗
NASA NTRS2003

Experimental Evaluation of Verification and Validation Tools on Martian Rover Software

To achieve its science objectives in deep space exploration, NASA has a need for science platform vehicles to autonomously make control decisions in a time frame that excludes intervention from Earth-based controllers. Round-trip light-time is one significant factor motivating autonomy capability, another factor is the need to reduce ground support operations cost. An unsolved problem potentially impeding the adoption of autonomy capability is the verification and validation of such software systems, which exhibit far more behaviors (and hence distinct execution paths in the software) than is typical in current deepspace platforms. Hence the need for a study to benchmark advanced Verification and Validation (V&V) tools on representative autonomy software. The objective of the study was to access the maturity of different technologies, to provide data indicative of potential synergies between them, and to identify gaps in the technologies with respect to the challenge of autonomy V&V. The study consisted of two parts: first, a set of relatively independent case studies of different tools on the same autonomy code, second a carefully controlled experiment with human participants on a subset of these technologies. This paper describes the second part of the study. Overall, nearly four hundred hours of data on human use of three different advanced V&V tools were accumulated, with a control group that used conventional testing methods. The experiment simulated four independent V&V teams debugging three successive versions of an executive controller for a Martian Rover. Defects were carefully seeded into the three versions based on a profile of defects from CVS logs that occurred in the actual development of the executive controller. The rest of the document is structured a s follows. In section 2 and 3, we respectively describe the tools used in the study and the rover software that was analyzed. In section 4 the methodology for the experiment is described; this includes the code preparation, seeding of defects, participant training and experimental setup. Next we give a qualitative overview of how the experiment went from the point of view of each technology; model checking (section 5), static analysis (section 6), runtime analysis (section 7) and testing (section 8). The find section gives some preliminary quantitative results on how the tools compared.

Brat, Guillaume↗
NASA NTRS2004

Adding Assurance to Automatically Generated Code

Code to estimate position and attitude of a spacecraft or aircraft belongs to the most safety-critical parts of flight software. The complex underlying mathematics and abundance of design details make it error-prone and reliable implementations costly. AutoFilter is a program synthesis tool for the automatic generation of state estimation code from compact specifications. It can automatically produce additional safety certificates which formally guarantee that each generated program individually satisfies a set of important safety policies. These safety policies (e.g.. array-bounds, variable initialization) form a core of properties which are essential for high-assurance software. Here we describe the AutoFilter system and its certificate generator and compare our approach to the static analysis tool PolySpace.

Denney, Ewen↗