Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “SMT”

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 19 records
All sourcesNASA NTRSDOE OSTI
NASA NTRS2014

Rewriting Modulo SMT and Open System Analysis

This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze infinite-state open systems, i.e., systems that interact with a non-deterministic environment. Such systems exhibit both internal non-determinism, which is proper to the system, and external non-determinism, which is due to the environment. In a reflective formalism, such as rewriting logic, rewriting modulo SMT can be reduced to standard rewriting. Hence, rewriting modulo SMT naturally extends rewriting-based reachability analysis techniques, which are available for closed systems, to open systems. The proposed technique is illustrated with the formal analysis of: (i) a real-time system that is beyond the scope of timed-automata methods and (ii) automatic detection of reachability violations in a synchronous language developed to support autonomous spacecraft operations.

Rocha, Camilo↗
NASA NTRS2013

Rewriting Modulo SMT

Combining symbolic techniques such as: (i) SMT solving, (ii) rewriting modulo theories, and (iii) model checking can enable the analysis of infinite-state systems outside the scope of each such technique. This paper proposes rewriting modulo SMT as a new technique combining the powers of (i)-(iii) and ideally suited to model and analyze infinite-state open systems; that is, systems that interact with a non-deterministic environment. Such systems exhibit both internal non-determinism due to the system, and external non-determinism due to the environment. They are not amenable to finite-state model checking analysis because they typically are infinite-state. By being reducible to standard rewriting using reflective techniques, rewriting modulo SMT can both naturally model and analyze open systems without requiring any changes to rewriting-based reachability analysis techniques for closed systems. This is illustrated by the analysis of a real-time system beyond the scope of timed automata methods.

Rocha, Camilo↗
NASA NTRS1996

Quality and Reliability of BGA and SMT Components

Spacecraft electronics including those used at the Jet Propulsion Laboratory (JPL), demand production of highly reliable assemblies. More than 400 test vehicles were assembled using ceramic and plastic ball grid arrays (BGAs), LCCs, J-leads, and gull wing components.

BGA components SMT components BGA SMT spacecraft e↗
NASA NTRS1999

Manufacturing Robustness of CSP in SMT Line

In this paper, the assembly process flow, solder paste for different stencil design, manufacturing defects, X-ray inspection results, and ultrasonic characterizations are reported.

electronic assembly SMT CSP fine pitch microvia te↗
NASA NTRS2018

Maximum Sample Temperature for Mars Sample Return: A Historical Perspective

Since the first Mars Sample Return (MSR) report published by the Jet Propulsion Laboratory (JPL) in 1974 [1], a series of panels, reports, and white papers have recognized the importance of sample temperature and offered an informed sample maximum temperature (henceforth SMT) limit for returning martian samples to Earth. The Mars Sample Handling and Requirements Panel (MSHARP, 1999) stated that "[t]he main issue in sample preservation is temperature" [2]. More recently, the Mars Exploration Program Analysis Group (MEPAG)'s "Science Priorities for Mars Sample Return" report (2008), declared that "[s]ignificant loss, particularly to biological studies, occurs if samples reach +50C for three hours", whereby "scientific objectives related to life goals could be seriously compromised" [3]. By contrast, the Mars 2020 mission has adopted a SMT of +60C as spelled out in Beaty et al., 2016 [4]. Samples will be collected and then deposited on the surface in sealed tubes for possible retrieval and return to Earth. Beaty et al. [4] calculates that the samples will experience maximum temperatures of ~+30 to +60C, depending on latitude. At present, there is no mission requirement for the measurement/data logging of sample temperature during this period. We will explore the history of martian SMTs, as they have been recorded since 1974 [1], effectively representing input across multiple generations of Mars scientists. Ten separate publications present SMTs for MSR samples [1-10]. One report [10] is for a mission concept specifically designed to exclude life detection investigations, and recommended an SMT of 50C. Another did not specify a temperature, recommending "Mars ambient temperature" [5]. Of the remaining eight, SMTs are given as: -30C [1], -20C [3], 60C [4], -73 to 41C depending on sample type [6], -40C [7], -43 to 13C depending on type [2,8], and -33C [9]. If we restrict the temperatures to samples highlighted in the Mars 2020 mission goals, i.e. organics-bearing and sedimentary rocks, then the average SMT is -28+/-39C (n=8). Applying a Dixon's Q Test at P=0.05 (two-tailed), the 60C SMT [4] fails with Q=0.602 versus Qcrit=0.526. Excluding the outlier produces an average SMT of -40+/-17C (n=7). Therefore, the average SMT expressed by the Mars science community over the past 44 years (two generations) is a sample temperature no greater than -40C. The difference in chemical reaction rates between this average SMT and Beaty et al [4] can be estimated using the Arrhenius equation. Assuming a generic chemical reaction with an activation energy of 50 kJ/mol and a pre-exponential factor invariant with temperature, this reaction will proceed 2300x faster at 60C than at -40C. To illustrate the effects of the increased reaction rate, consider 10 ppb of alanine in a Mars 2020 cache, and assume that it becomes unmeasurable if it degrades to 1 ppb, as per the Mars 2020 Organic Contamination Panel contamination limits [11]. If we illustrate the effect with an arbitrary degradation rate such that the alanine will become undetectable in ten years at -40C, then the same 10 ppb alanine degrades beyond detectability in only 38 days at 60C. Further research is required to quantify expected analyte losses in the cached samples due to thermal processing.

Fries, Marc↗
NASA NTRS2010

Decision Engines for Software Analysis Using Satisfiability Modulo Theories Solvers

The area of software analysis, testing and verification is now undergoing a revolution thanks to the use of automated and scalable support for logical methods. A well-recognized premise is that at the core of software analysis engines is invariably a component using logical formulas for describing states and transformations between system states. The process of using this information for discovering and checking program properties (including such important properties as safety and security) amounts to automatic theorem proving. In particular, theorem provers that directly support common software constructs offer a compelling basis. Such provers are commonly called satisfiability modulo theories (SMT) solvers. Z3 is a state-of-the-art SMT solver. It is developed at Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories such as arithmetic, bit-vectors, lists, records and arrays. The talk describes some of the technology behind modern SMT solvers, including the solver Z3. Z3 is currently mainly targeted at solving problems that arise in software analysis and verification. It has been applied to various contexts, such as systems for dynamic symbolic simulation (Pex, SAGE, Vigilante), for program verification and extended static checking (Spec#/Boggie, VCC, HAVOC), for software model checking (Yogi, SLAM), model-based design (FORMULA), security protocol code (F7), program run-time analysis and invariant generation (VS3). We will describe how it integrates support for a variety of theories that arise naturally in the context of the applications. There are several new promising avenues and the talk will touch on some of these and the challenges related to SMT solvers. Proceedings

Bjorner, Nikolaj↗
NASA NTRS2015

Implementing NASA's Capability-Driven Approach: Insight into NASA's Processes for Maturing Exploration Systems

NASA is engaged in transforming human spaceflight. The Agency is shifting from an exploration-based program with human activities focused on low Earth orbit (LEO) and targeted robotic missions in deep space to a more sustainable and integrated pioneering approach. Through pioneering, NASA seeks to address national goals to develop the capacity for people to work, learn, operate, live, and thrive safely beyond the Earth for extended periods of time. However, pioneering space involves more than the daunting technical challenges of transportation, maintaining health, and enabling crew productivity for long durations in remote, hostile, and alien environments. This shift also requires a change in operating processes for NASA. The Agency can no longer afford to engineer systems for specific missions and destinations and instead must focus on common capabilities that enable a range of destinations and missions. NASA has codified a capability driven approach, which provides flexible guidance for the development and maturation of common capabilities necessary for human pioneers beyond LEO. This approach has been included in NASA policy and is captured in the Agency's strategic goals. It is currently being implemented across NASA's centers and programs. Throughout 2014, NASA engaged in an Agency-wide process to define and refine exploration-related capabilities and associated gaps, focusing only on those that are critical for human exploration beyond LEO. NASA identified 12 common capabilities ranging from Environmental Control and Life Support Systems to Robotics, and established Agency-wide teams or working groups comprised of subject matter experts that are responsible for the maturation of these exploration capabilities. These teams, called the System Maturation Teams (SMTs) help formulate, guide and resolve performance gaps associated with the identified exploration capabilities. The SMTs are defining performance parameters and goals for each of the 12 capabilities, developing maturation plans and roadmaps for the identified performance gaps, specifying the interfaces between the various capabilities, and ensuring that the capabilities mature and integrate to enable future pioneering missions. By managing system development through the SMTs instead of traditional NASA programs and projects, the Agency is shifting from mission-driven development to a more flexible, capability-driven development. The process NASA uses to establish, integrate, prioritize, and manage the SMTs and associated capabilities is iterative. NASA relies on the Human Exploration and Operation Mission Directorate's SMT Integration Team within Advanced Exploration Systems to coordinate and facilitate the SMT process. The SMT Integration team conducts regular reviews and coordination meetings among the SMTs and has developed a number of tools to help the Agency implement capability driven processes. The SMT Integration team is uniquely positioned to help the Agency coordinate the SMTs and other processes that are making the capability-driven approach a reality. This paper will introduce the SMTs and the 12 key capabilities they represent. The role of the SMTs will be discussed with respect to Agency-wide processes to shift from mission-focused exploration to a capability-driven pioneering approach. Specific examples will be given to highlight systems development and testing within the SMTs. These examples will also show how NASA is using current investments in the International Space Station and future investments to develop and demonstrate capabilities. The paper will conclude by describing next steps and a process for soliciting feedback from the space exploration community to refine NASA's process for developing common exploration capabilities.

Williams-Byrd, Julie↗
NASA NTRS1991

An application specific integrated circuit based multi-anode microchannel array readout system

Size reduction of two new multi-anode microchannel array (MAMA) readout systems is described. The systems are based on two analog and one digital application specific integrated circuits (ASICs). The new readout systems reduce volume over previous discrete designs by 80 percent while improving electrical performance on virtually every significant parameter. Emphasis is made on the packaging used to achieve the volume reduction. Surface mount technology (SMT) is combined with modular construction for the analog portion of the readout. SMT reliability concerns and the board area impact of MIL SPEC SMT components is addressed. Package selection for the analog ASIC is discussed. Future sytems will require even denser packaging and the volume reduction progression is shown.

Smeins, Larry G.↗
NASA NTRS1993

TAB interconnects for space concentrator solar cell arrays

The Boeing Company has evaluated the use of Tape Automated Bonding (TAB) and Surface Mount Technology (SMT) for a highly reliable, low cost interconnect for concentrator solar cell arrays. TAB and SMT are currently used in the electronics industry for chip interconnects and printed circuit board assembly. TAB tape consists of sixty-four 3-mil/1-oz tin-plated copper leads on 8-mil centers. The leads are thermocompression gang bonded to GaAs concentrator solar cell with silver contacts. This bond, known as an Inner Lead Bond (ILB), allows for pretesting and sorting capability via nondestruct wire bond pull and flash testing. Destructive wire pull tests resulted in preferred mid-span failures. Improvements in fill factor were attributed to decreased contact resistance on TAB bonded cells. Preliminary thermal cycling and aging tests were shown excellent bond strength and metallurgical results. Auger scans of bond sites reveals an Ag-Cu-Tin composition. Improper bonds are identified through flash testing as a performance degradation. On going testing of cells are underway at Lewis Research Center. SMT techniques are utilized to excise and form TAB leads post ILB. The formed leads' shape isolates thermal mismatches between the cells and the flex circuit they are mounted on. TABed cells are picked and placed with a gantry x-y-z positioning system with pattern recognition. Adhesives are selected to avoid thermal expansion mismatch and promote thermal transfer to the flex circuit. TAB outer lead bonds are parallel gap welded (PGW) to the flex circuit to finish the concentrator solar cell subassembly.

Avery, J.↗
NASA NTRS1995

High Reliability, High Mix, Ultralow Volume Surface Mount Technology for Space Applications

For the past two years, JPL has been working to introduce surface mount technology (SMT) for high reliability space applications. The thrust has centered around four research and development projects, the aim of which is to facilitate the use of SMT for designing, producing, inspecting, and quantifying surface mount printed wiring assemblies for ultralow volume, long life space applications. This paper explores the current approach being pursued at JPL and some of the problems peculiar to applying SMT to spacecraft applications.

volume long life↗
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 NTRS2016

Graphical Visualization of Human Exploration Capabilities

NASA's pioneering space strategy will require advanced capabilities to expand the boundaries of human exploration on the Journey to Mars (J2M). The Evolvable Mars Campaign (EMC) architecture serves as a framework to identify critical capabilities that need to be developed and tested in order to enable a range of human exploration destinations and missions. Agency-wide System Maturation Teams (SMT) are responsible for the maturation of these critical exploration capabilities and help formulate, guide and resolve performance gaps associated with the EMC-identified capabilities. Systems Capability Organization Reporting Engine boards (SCOREboards) were developed to integrate the SMT data sets into cohesive human exploration capability stories that can be used to promote dialog and communicate NASA's exploration investments. Each SCOREboard provides a graphical visualization of SMT capability development needs that enable exploration missions, and presents a comprehensive overview of data that outlines a roadmap of system maturation needs critical for the J2M. SCOREboards are generated by a computer program that extracts data from a main repository, sorts the data based on a tiered data reduction structure, and then plots the data according to specified user inputs. The ability to sort and plot varying data categories provides the flexibility to present specific SCOREboard capability roadmaps based on customer requests. This paper presents the development of the SCOREboard computer program and shows multiple complementary, yet different datasets through a unified format designed to facilitate comparison between datasets. Example SCOREboard capability roadmaps are presented followed by a discussion of how the roadmaps are used to: 1) communicate capability developments and readiness of systems for future missions, and 2) influence the definition of NASA's human exploration investment portfolio through capability-driven processes. The paper concludes with a description of planned future work to modify the computer program to include additional data and of alternate capability roadmap formats currently under consideration.

Rodgers, Erica M.↗
NASA NTRS2024

Will MSR Samples Cached on the Martian Surface Experience Significantly Greater Thermal Degradation than Samples Retained in the Rover?

Since the first Mars Sample Return (MSR)-related report published by the Jet Propulsion Laboratory (JPL) in 1974, a series of panels, reports, and white papers have recognized the importance of sample temperature in meeting mission goals and defined a sample maximum temperature (henceforth SMT) limit. The Mars Sample Handling and Requirements Panel (MSHARP, 1999) flatly stated that “[t]he main issue in sample preservation is temperature”. The Mars Exploration Program Analysis Group (MEPAG)’s “Science Priorities for Mars Sample Return” report (2008), declared that “[s]ignificant loss, particularly to biological studies, occurs if samples reach +50°C for three hours ” whereby “scientific objectives related to life goals could be seriously compromised”. Overall, a total of seven panels, white papers, and conference reports adopted a SMT of -40±17°C to preserve samples sufficiently to confidently achieve success in studies of past or present Martian life (see more detail in [5]). In contrast, the Mars 2020 rover (M2020) mission adopted a SMT of +60°C for samples stored on the Martian surface and +50°C for samples retained inside the rover, as stated in a conference poster presented by Beaty et al., 2016. M2020 is currently collecting samples for MSR in tubes. Half of those tubes will be retained within the M2020 rover body (hereafter rover samples, or RS) and half will be deposited on the Martian surface (cached samples or CS), with a currently undetermined number of each collected up to ten years later for return to Earth. CS samples can be expected to experience significantly higher temperatures than RS samples based on their exposed location in sunlight. This work will explore differences in deleterious chemical reaction rates due to thermal environment of both tube types. The findings here should be debated openly and considered when deciding which samples to return to Earth.

M Fries↗
NASA NTRS1984

A New Generation of Sub Mm Telescopes, Made of Carbon Fiber Reinforced Plastic

Carbon fiber reinforced plastic (CFRP) appears to be the material most suited for the construction of submillimeter telescopes (SMT) not only for ground-based use but also for space applications. The accuracy of the CFRP reflectors needs to be improved beyond value of the 17 micron rms envisaged for the 10 m SMT.

Mezger, P.↗
NASA NTRS2010

Advanced Flip Chips in Extreme Temperature Environments

The use of underfill materials is necessary with flip-chip interconnect technology to redistribute stresses due to mismatching coefficients of thermal expansion (CTEs) between dissimilar materials in the overall assembly. Underfills are formulated using organic polymers and possibly inorganic filler materials. There are a few ways to apply the underfills with flip-chip technology. Traditional capillary-flow underfill materials now possess high flow speed and reduced time to cure, but they still require additional processing steps beyond the typical surface-mount technology (SMT) assembly process. Studies were conducted using underfills in a temperature range of -190 to 85 C, which resulted in an increase of reliability by one to two orders of magnitude. Thermal shock of the flip-chip test articles was designed to induce failures at the interconnect sites (-40 to 100 C). The study on the reliability of flip chips using underfills in the extreme temperature region is of significant value for space applications. This technology is considered as an enabling technology for future space missions. Flip-chip interconnect technology is an advanced electrical interconnection approach where the silicon die or chip is electrically connected, face down, to the substrate by reflowing solder bumps on area-array metallized terminals on the die to matching footprints of solder-wettable pads on the chosen substrate. This advanced flip-chip interconnect technology will significantly improve the performance of high-speed systems, productivity enhancement over manual wire bonding, self-alignment during die joining, low lead inductances, and reduced need for attachment of precious metals. The use of commercially developed no-flow fluxing underfills provides a means of reducing the processing steps employed in the traditional capillary flow methods to enhance SMT compatibility. Reliability of flip chips may be significantly increased by matching/tailoring the CTEs of the substrate material and the silicon die or chip, and also the underfill materials. Advanced packaging interconnects technology such as flip-chip interconnect test boards have been subjected to various extreme temperature ranges that cover military specifications and extreme Mars and asteroid environments. The eventual goal of each process step and the entire process is to produce components with 100 percent interconnect and satisfy the reliability requirements. Underfill materials, in general, may possibly meet demanding end use requirements such as low warpage, low stress, fine pitch, high reliability, and high adhesion.

Ramesham, Rajeshuni↗
NASA NTRS2015

The Evolution of Volatile Production in Comet C-2009 P1(Garradd) During its 2011-2012 Apparition

We report observations at millimeter and submillimeter wavelengths of comet C/2009 P1 (Garradd) from 2011 December 28 to 2012 April 24, using the Arizona Radio Observatory submillimeter telescope (SMT) and the James Clerk Maxwell Telescope (JCMT). Garradd is a dynamically young long-period comet from the Oort Cloud, with a periodicity of 127,000 years, that reached perihelion on 2011 December 23 (at Heliocentric distance (Rh) = 1.55 Astronomical Units and delta = 20.1 Astronomical Units ) and made its closest approach to the Earth on 2012 March 05 (at Heliocentric distance (Rh) = 1.84 Astronomical Units and delta = 1.26 Astronomical Units). We obtained gas production rates, and molecular abundances relative to water for HCN, ortho-H2CO, CS, CO and CH3OH. A rotational temperature, T (sub rot) approximately equal to 50 degrees Kelvin, was determined by observing multiple methanol lines with the JCMT. By averaging the abundance ratio relative to water from the SMT and the JCMT we derive: CO: 7.03 plus or minus 1.84 percent, HCN: 0.04 plus or minus 0.01 percent, ortho H2CO: 0.14 plus or minus 0.03 percent as a parent molecule (and 0.28 plus or minus 0.06 percent as an extended source), CS: 0.03 plus or minus 0.01 percent and CH3OH: 3.11 for a range from plus 1:86 to minus 0.51 percent. We concluded that Garradd is normal in CH3OH, depleted in HCN, ortho-H2CO and CS and slightly enriched in CO with respect to typically observed cometary mixing ratios. We also studied the temporal evolution of HCN and CO and find that the production of HCN has a trend similar to water (but with short-term variation), with a decrease after perihelion, while that of CO shows contrary behavior: remaining constant or increasing after perihelion.

Comets: individual↗
NASA NTRS2018

Advanced Symbolic Analysis Tools for Fault-Tolerant Integrated Distributed Systems

The project aims to develop advanced model-checking algorithms and tools to automate the verification of fault-tolerant distributed systems for avionics. We present a new method called Property-Directed K-Induction (PD-KIND) for synthesizing K-inductive invariants of state-transition systems. PD-KIND builds upon Satifiability Modulo Theories (SMT) to generalize Bradley's IC3 method and its variants. This method is implemented in a new tool called SALLY. Case studies show that PD-KIND can automatically verify fault-tolerant algorithms under a variety of fault models and that SALLY is competitive with other SMT-based model checkers.

Dutertre, Bruno↗