Formal Methods Tool Qualification

NASA Technical Reports Server (NTRS)

Wagner, Lucas G.; Cofer, Darren; Slind, Konrad; Tinelli, Cesare; Mebsout, Alain

2017-01-01

Formal methods tools have been shown to be effective at finding defects in safety-critical digital systems including avionics systems. The publication of DO-178C and the accompanying formal methods supplement DO-333 allows applicants to obtain certification credit for the use of formal methods without providing justification for them as an alternative method. This project conducted an extensive study of existing formal methods tools, identifying obstacles to their qualification and proposing mitigations for those obstacles. Further, it interprets the qualification guidance for existing formal methods tools and provides case study examples for open source tools. This project also investigates the feasibility of verifying formal methods tools by generating proof certificates which capture proof of the formal methods tool's claim, which can be checked by an independent, proof certificate checking tool. Finally, the project investigates the feasibility of qualifying this proof certificate checker, in the DO-330 framework, in lieu of qualifying the model checker itself.

Experience report: Using formal methods for requirements analysis of critical spacecraft software

NASA Technical Reports Server (NTRS)

Lutz, Robyn R.; Ampo, Yoko

1994-01-01

Formal specification and analysis of requirements continues to gain support as a method for producing more reliable software. However, the introduction of formal methods to a large software project is difficult, due in part to the unfamiliarity of the specification languages and the lack of graphics. This paper reports results of an investigation into the effectiveness of formal methods as an aid to the requirements analysis of critical, system-level fault-protection software on a spacecraft currently under development. Our experience indicates that formal specification and analysis can enhance the accuracy of the requirements and add assurance prior to design development in this domain. The work described here is part of a larger, NASA-funded research project whose purpose is to use formal-methods techniques to improve the quality of software in space applications. The demonstration project described here is part of the effort to evaluate experimentally the effectiveness of supplementing traditional engineering approaches to requirements specification with the more rigorous specification and analysis available with formal methods.

Formal methods demonstration project for space applications

NASA Technical Reports Server (NTRS)

Divito, Ben L.

1995-01-01

The Space Shuttle program is cooperating in a pilot project to apply formal methods to live requirements analysis activities. As one of the larger ongoing shuttle Change Requests (CR's), the Global Positioning System (GPS) CR involves a significant upgrade to the Shuttle's navigation capability. Shuttles are to be outfitted with GPS receivers and the primary avionics software will be enhanced to accept GPS-provided positions and integrate them into navigation calculations. Prior to implementing the CR, requirements analysts at Loral Space Information Systems, the Shuttle software contractor, must scrutinize the CR to identify and resolve any requirements issues. We describe an ongoing task of the Formal Methods Demonstration Project for Space Applications whose goal is to find an effective way to use formal methods in the GPS CR requirements analysis phase. This phase is currently under way and a small team from NASA Langley, ViGYAN Inc. and Loral is now engaged in this task. Background on the GPS CR is provided and an overview of the hardware/software architecture is presented. We outline the approach being taken to formalize the requirements, only a subset of which is being attempted. The approach features the use of the PVS specification language to model 'principal functions', which are major units of Shuttle software. Conventional state machine techniques form the basis of our approach. Given this background, we present interim results based on a snapshot of work in progress. Samples of requirements specifications rendered in PVS are offered to illustration. We walk through a specification sketch for the principal function known as GPS Receiver State processing. Results to date are summarized and feedback from Loral requirements analysts is highlighted. Preliminary data is shown comparing issues detected by the formal methods team versus those detected using existing requirements analysis methods. We conclude by discussing our plan to complete the remaining

Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems

NASA Technical Reports Server (NTRS)

Munoz, Cesar A.

2015-01-01

As the technological and operational capabilities of unmanned aircraft systems (UAS) continue to grow, so too does the need to introduce these systems into civil airspace. Unmanned Aircraft Systems Integration in the National Airspace System is a NASA research project that addresses the integration of civil UAS into non-segregated airspace operations. One of the major challenges of this integration is the lack of an onboard pilot to comply with the legal requirement that pilots see and avoid other aircraft. The need to provide an equivalent to this requirement for UAS has motivated the development of a detect and avoid (DAA) capability to provide the appropriate situational awareness and maneuver guidance in avoiding and remaining well clear of traffic aircraft. Formal methods has played a fundamental role in the development of this capability. This talk reports on the formal methods work conducted under NASA's Safe Autonomous System Operations project in support of the development of DAA for UAS. This work includes specification of low-level and high-level functional requirements, formal verification of algorithms, and rigorous validation of software implementations. The talk also discusses technical challenges in formal methods research in the context of the development and safety analysis of advanced air traffic management concepts.

A Formal Methods Approach to the Analysis of Mode Confusion

NASA Technical Reports Server (NTRS)

Butler, Ricky W.; Miller, Steven P.; Potts, James N.; Carreno, Victor A.

2004-01-01

The goal of the new NASA Aviation Safety Program (AvSP) is to reduce the civil aviation fatal accident rate by 80% in ten years and 90% in twenty years. This program is being driven by the accident data with a focus on the most recent history. Pilot error is the most commonly cited cause for fatal accidents (up to 70%) and obviously must be given major consideration in this program. While the greatest source of pilot error is the loss of situation awareness , mode confusion is increasingly becoming a major contributor as well. The January 30, 1995 issue of Aviation Week lists 184 incidents and accidents involving mode awareness including the Bangalore A320 crash 2/14/90, the Strasbourg A320 crash 1/20/92, the Mulhouse-Habsheim A320 crash 6/26/88, and the Toulouse A330 crash 6/30/94. These incidents and accidents reveal that pilots sometimes become confused about what the cockpit automation is doing. Consequently, human factors research is an obvious investment area. However, even a cursory look at the accident data reveals that the mode confusion problem is much deeper than just training deficiencies and a lack of human-oriented design. This is readily acknowledged by human factors experts. It seems that further progress in human factors must come through a deeper scrutiny of the internals of the automation. It is in this arena that formal methods can contribute. Formal methods refers to the use of techniques from logic and discrete mathematics in the specification, design, and verification of computer systems, both hardware and software. The fundamental goal of formal methods is to capture requirements, designs and implementations in a mathematically based model that can be analyzed in a rigorous manner. Research in formal methods is aimed at automating this analysis as much as possible. By capturing the internal behavior of a flight deck in a rigorous and detailed formal model, the dark corners of a design can be analyzed. This paper will explore how formal

Formalizing Space Shuttle Software Requirements

NASA Technical Reports Server (NTRS)

Crow, Judith; DiVito, Ben L.

1996-01-01

This paper describes two case studies in which requirements for new flight-software subsystems on NASA's Space Shuttle were analyzed, one using standard formal specification techniques, the other using state exploration. These applications serve to illustrate three main theses: (1) formal methods can complement conventional requirements analysis processes effectively, (2) formal methods confer benefits regardless of how extensively they are adopted and applied, and (3) formal methods are most effective when they are judiciously tailored to the application.

Application of Lightweight Formal Methods to Software Security

NASA Technical Reports Server (NTRS)

Gilliam, David P.; Powell, John D.; Bishop, Matt

2005-01-01

Formal specification and verification of security has proven a challenging task. There is no single method that has proven feasible. Instead, an integrated approach which combines several formal techniques can increase the confidence in the verification of software security properties. Such an approach which species security properties in a library that can be reused by 2 instruments and their methodologies developed for the National Aeronautics and Space Administration (NASA) at the Jet Propulsion Laboratory (JPL) are described herein The Flexible Modeling Framework (FMF) is a model based verijkation instrument that uses Promela and the SPIN model checker. The Property Based Tester (PBT) uses TASPEC and a Text Execution Monitor (TEM). They are used to reduce vulnerabilities and unwanted exposures in software during the development and maintenance life cycles.

What can formal methods offer to digital flight control systems design

NASA Technical Reports Server (NTRS)

Good, Donald I.

1990-01-01

Formal methods research begins to produce methods which will enable mathematic modeling of the physical behavior of digital hardware and software systems. The development of these methods directly supports the NASA mission of increasing the scope and effectiveness of flight system modeling capabilities. The conventional, continuous mathematics that is used extensively in modeling flight systems is not adequate for accurate modeling of digital systems. Therefore, the current practice of digital flight control system design has not had the benefits of extensive mathematical modeling which are common in other parts of flight system engineering. Formal methods research shows that by using discrete mathematics, very accurate modeling of digital systems is possible. These discrete modeling methods will bring the traditional benefits of modeling to digital hardware and hardware design. Sound reasoning about accurate mathematical models of flight control systems can be an important part of reducing risk of unsafe flight control.

Experience Using Formal Methods for Specifying a Multi-Agent System

NASA Technical Reports Server (NTRS)

Rouff, Christopher; Rash, James; Hinchey, Michael; Szczur, Martha R. (Technical Monitor)

2000-01-01

The process and results of using formal methods to specify the Lights Out Ground Operations System (LOGOS) is presented in this paper. LOGOS is a prototype multi-agent system developed to show the feasibility of providing autonomy to satellite ground operations functions at NASA Goddard Space Flight Center (GSFC). After the initial implementation of LOGOS the development team decided to use formal methods to check for race conditions, deadlocks and omissions. The specification exercise revealed several omissions as well as race conditions. After completing the specification, the team concluded that certain tools would have made the specification process easier. This paper gives a sample specification of two of the agents in the LOGOS system and examples of omissions and race conditions found. It concludes with describing an architecture of tools that would better support the future specification of agents and other concurrent systems.

Formal Methods for Autonomic and Swarm-based Systems

NASA Technical Reports Server (NTRS)

Rouff, Christopher; Vanderbilt, Amy; Hinchey, Mike; Truszkowski, Walt; Rash, James

2004-01-01

Swarms of intelligent rovers and spacecraft are being considered for a number of future NASA missions. These missions will provide MSA scientist and explorers greater flexibility and the chance to gather more science than traditional single spacecraft missions. These swarms of spacecraft are intended to operate for large periods of time without contact with the Earth. To do this, they must be highly autonomous, have autonomic properties and utilize sophisticated artificial intelligence. The Autonomous Nano Technology Swarm (ANTS) mission is an example of one of the swarm type of missions NASA is considering. This mission will explore the asteroid belt using an insect colony analogy cataloging the mass, density, morphology, and chemical composition of the asteroids, including any anomalous concentrations of specific minerals. Verifying such a system would be a huge task. This paper discusses ongoing work to develop a formal method for verifying swarm and autonomic systems.

Formal methods technology transfer: Some lessons learned

NASA Technical Reports Server (NTRS)

Hamilton, David

1992-01-01

IBM has a long history in the application of formal methods to software development and verification. There have been many successes in the development of methods, tools and training to support formal methods. And formal methods have been very successful on several projects. However, the use of formal methods has not been as widespread as hoped. This presentation summarizes several approaches that have been taken to encourage more widespread use of formal methods, and discusses the results so far. The basic problem is one of technology transfer, which is a very difficult problem. It is even more difficult for formal methods. General problems of technology transfer, especially the transfer of formal methods technology, are also discussed. Finally, some prospects for the future are mentioned.

Unmanned Aircraft Systems in the National Airspace System: A Formal Methods Perspective

NASA Technical Reports Server (NTRS)

Munoz, Cesar A.; Dutle, Aaron; Narkawicz, Anthony; Upchurch, Jason

2016-01-01

As the technological and operational capabilities of unmanned aircraft systems (UAS) have grown, so too have international efforts to integrate UAS into civil airspace. However, one of the major concerns that must be addressed in realizing this integration is that of safety. For example, UAS lack an on-board pilot to comply with the legal requirement that pilots see and avoid other aircraft. This requirement has motivated the development of a detect and avoid (DAA) capability for UAS that provides situational awareness and maneuver guidance to UAS operators to aid them in avoiding and remaining well clear of other aircraft in the airspace. The NASA Langley Research Center Formal Methods group has played a fundamental role in the development of this capability. This article gives a selected survey of the formal methods work conducted in support of the development of a DAA concept for UAS. This work includes specification of low-level and high-level functional requirements, formal verification of algorithms, and rigorous validation of software implementations.

Using Formal Methods to Assist in the Requirements Analysis of the Space Shuttle GPS Change Request

NASA Technical Reports Server (NTRS)

DiVito, Ben L.; Roberts, Larry W.

1996-01-01

We describe a recent NASA-sponsored pilot project intended to gauge the effectiveness of using formal methods in Space Shuttle software requirements analysis. Several Change Requests (CR's) were selected as promising targets to demonstrate the utility of formal methods in this application domain. A CR to add new navigation capabilities to the Shuttle, based on Global Positioning System (GPS) technology, is the focus of this report. Carried out in parallel with the Shuttle program's conventional requirements analysis process was a limited form of analysis based on formalized requirements. Portions of the GPS CR were modeled using the language of SRI's Prototype Verification System (PVS). During the formal methods-based analysis, numerous requirements issues were discovered and submitted as official issues through the normal requirements inspection process. Shuttle analysts felt that many of these issues were uncovered earlier than would have occurred with conventional methods. We present a summary of these encouraging results and conclusions we have drawn from the pilot project.

Formal Methods for Life-Critical Software

NASA Technical Reports Server (NTRS)

Butler, Ricky W.; Johnson, Sally C.

1993-01-01

The use of computer software in life-critical applications, such as for civil air transports, demands the use of rigorous formal mathematical verification procedures. This paper demonstrates how to apply formal methods to the development and verification of software by leading the reader step-by-step through requirements analysis, design, implementation, and verification of an electronic phone book application. The current maturity and limitations of formal methods tools and techniques are then discussed, and a number of examples of the successful use of formal methods by industry are cited.

Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems. Volume 2; A Practitioner's Companion

NASA Technical Reports Server (NTRS)

1995-01-01

This guidebook, the second of a two-volume series, is intended to facilitate the transfer of formal methods to the avionics and aerospace community. The 1st volume concentrates on administrative and planning issues [NASA-95a], and the second volume focuses on the technical issues involved in applying formal methods to avionics and aerospace software systems. Hereafter, the term "guidebook" refers exclusively to the second volume of the series. The title of this second volume, A Practitioner's Companion, conveys its intent. The guidebook is written primarily for the nonexpert and requires little or no prior experience with formal methods techniques and tools. However, it does attempt to distill some of the more subtle ingredients in the productive application of formal methods. To the extent that it succeeds, those conversant with formal methods will also nd the guidebook useful. The discussion is illustrated through the development of a realistic example, relevant fragments of which appear in each chapter. The guidebook focuses primarily on the use of formal methods for analysis of requirements and high-level design, the stages at which formal methods have been most productively applied. Although much of the discussion applies to low-level design and implementation, the guidebook does not discuss issues involved in the later life cycle application of formal methods.

Experiences applying Formal Approaches in the Development of Swarm-Based Space Exploration Systems

NASA Technical Reports Server (NTRS)

Rouff, Christopher A.; Hinchey, Michael G.; Truszkowski, Walter F.; Rash, James L.

2006-01-01

NASA is researching advanced technologies for future exploration missions using intelligent swarms of robotic vehicles. One of these missions is the Autonomous Nan0 Technology Swarm (ANTS) mission that will explore the asteroid belt using 1,000 cooperative autonomous spacecraft. The emergent properties of intelligent swarms make it a potentially powerful concept, but at the same time more difficult to design and ensure that the proper behaviors will emerge. NASA is investigating formal methods and techniques for verification of such missions. The advantage of using formal methods is the ability to mathematically verify the behavior of a swarm, emergent or otherwise. Using the ANTS mission as a case study, we have evaluated multiple formal methods to determine their effectiveness in modeling and ensuring desired swarm behavior. This paper discusses the results of this evaluation and proposes an integrated formal method for ensuring correct behavior of future NASA intelligent swarms.

Formalisms for user interface specification and design

NASA Technical Reports Server (NTRS)

Auernheimer, Brent J.

1989-01-01

The application of formal methods to the specification and design of human-computer interfaces is described. A broad outline of human-computer interface problems, a description of the field of cognitive engineering and two relevant research results, the appropriateness of formal specification techniques, and potential NASA application areas are described.

Formal Methods Case Studies for DO-333

NASA Technical Reports Server (NTRS)

Cofer, Darren; Miller, Steven P.

2014-01-01

RTCA DO-333, Formal Methods Supplement to DO-178C and DO-278A provides guidance for software developers wishing to use formal methods in the certification of airborne systems and air traffic management systems. The supplement identifies the modifications and additions to DO-178C and DO-278A objectives, activities, and software life cycle data that should be addressed when formal methods are used as part of the software development process. This report presents three case studies describing the use of different classes of formal methods to satisfy certification objectives for a common avionics example - a dual-channel Flight Guidance System. The three case studies illustrate the use of theorem proving, model checking, and abstract interpretation. The material presented is not intended to represent a complete certification effort. Rather, the purpose is to illustrate how formal methods can be used in a realistic avionics software development project, with a focus on the evidence produced that could be used to satisfy the verification objectives found in Section 6 of DO-178C.

Experiences Using Formal Methods for Requirements Modeling

NASA Technical Reports Server (NTRS)

Easterbrook, Steve; Lutz, Robyn; Covington, Rick; Kelly, John; Ampo, Yoko; Hamilton, David

1996-01-01

This paper describes three cases studies in the lightweight application of formal methods to requirements modeling for spacecraft fault protection systems. The case studies differ from previously reported applications of formal methods in that formal methods were applied very early in the requirements engineering process, to validate the evolving requirements. The results were fed back into the projects, to improve the informal specifications. For each case study, we describe what methods were applied, how they were applied, how much effort was involved, and what the findings were. In all three cases, the formal modeling provided a cost effective enhancement of the existing verification and validation processes. We conclude that the benefits gained from early modeling of unstable requirements more than outweigh the effort needed to maintain multiple representations.

Guidance for Using Formal Methods in a Certification Context

NASA Technical Reports Server (NTRS)

Brown, Duncan; Delseny, Herve; Hayhurst, Kelly; Wiels, Virginie

2010-01-01

This paper discusses some of the challenges to using formal methods in a certification context and describes the effort by the Formal Methods Subgroup of RTCA SC-205/EUROCAE WG-71 to propose guidance to make the use of formal methods a recognized approach. This guidance, expected to take the form of a Formal Methods Technical Supplement to DO-178C/ED-12C, is described, including the activities that are needed when using formal methods, new or modified objectives with respect to the core DO-178C/ED-12C document, and evidence needed for meeting those objectives.

Ten Commandments of Formal Methods...Ten Years Later

NASA Technical Reports Server (NTRS)

Bowen, Jonathan P.; Hinchey, Michael G.

2006-01-01

More than a decade ago, in "Ten Commandments of Formal Methods," we offered practical guidelines for projects that sought to use formal methods. Over the years, the article, which was based on our knowledge of successful industrial projects, has been widely cited and has generated much positive feedback. However, despite this apparent enthusiasm, formal methods use has not greatly increased, and some of the same attitudes about the infeasibility of adopting them persist. Formal methodists believe that introducing greater rigor will improve the software development process and yield software with better structure, greater maintainability, and fewer errors.

Using NASA Data in the Classroom: Promoting STEM Learning in Formal Education using Real Space Science Data

NASA Astrophysics Data System (ADS)

Lawton, B.; Hemenway, M. K.; Mendez, B.; Odenwald, S.

2013-04-01

Among NASA's major education goals is the training of students in the Science, Technology, Engineering, and Math (STEM) disciplines. The use of real data, from some of the most sophisticated observatories in the world, provides formal educators the opportunity to teach their students real-world applications of the STEM subjects. Combining real space science data with lessons aimed at meeting state and national education standards provides a memorable educational experience that students can build upon throughout their academic careers. Many of our colleagues have adopted the use of real data in their education and public outreach (EPO) programs. There are challenges in creating resources using real data for classroom use that include, but are not limited to, accessibility to computers/Internet and proper instruction. Understanding and sharing these difficulties and best practices with the larger EPO community is critical to the development of future resources. In this session, we highlight three examples of how NASA data is being utilized in the classroom: the Galaxies and Cosmos Explorer Tool (GCET) that utilizes real Hubble Space Telescope data; the computer image-analysis resources utilized by the NASA WISE infrared mission; and the space science derived math applications from SpaceMath@NASA featuring the Chandra and Kepler space telescopes. Challenges and successes are highlighted for these projects. We also facilitate small-group discussions that focus on additional benefits and challenges of using real data in the formal education environment. The report-outs from those discussions are given here.

Moving formal methods into practice. Verifying the FTPP Scoreboard: Results, phase 1

NASA Technical Reports Server (NTRS)

Srivas, Mandayam; Bickford, Mark

1992-01-01

This report documents the Phase 1 results of an effort aimed at formally verifying a key hardware component, called Scoreboard, of a Fault-Tolerant Parallel Processor (FTPP) being built at Charles Stark Draper Laboratory (CSDL). The Scoreboard is part of the FTPP virtual bus that guarantees reliable communication between processors in the presence of Byzantine faults in the system. The Scoreboard implements a piece of control logic that approves and validates a message before it can be transmitted. The goal of Phase 1 was to lay the foundation of the Scoreboard verification. A formal specification of the functional requirements and a high-level hardware design for the Scoreboard were developed. The hardware design was based on a preliminary Scoreboard design developed at CSDL. A main correctness theorem, from which the functional requirements can be established as corollaries, was proved for the Scoreboard design. The goal of Phase 2 is to verify the final detailed design of Scoreboard. This task is being conducted as part of a NASA-sponsored effort to explore integration of formal methods in the development cycle of current fault-tolerant architectures being built in the aerospace industry.

Formal Methods Applications in Air Transportation

NASA Technical Reports Server (NTRS)

Farley, Todd

2009-01-01

The U.S. air transportation system is the most productive in the world, moving far more people and goods than any other. It is also the safest system in the world, thanks in part to its venerable air traffic control system. But as demand for air travel continues to grow, the air traffic control system s aging infrastructure and labor-intensive procedures are impinging on its ability to keep pace with demand. And that impinges on the growth of our economy. Air traffic control modernization has long held the promise of a more efficient air transportation system. Part of NASA s current mission is to develop advanced automation and operational concepts that will expand the capacity of our national airspace system while still maintaining its excellent record for safety. It is a challenging mission, as efforts to modernize have, for decades, been hamstrung by the inability to assure safety to the satisfaction of system operators, system regulators, and/or the traveling public. In this talk, we ll provide a brief history of air traffic control, focusing on the tension between efficiency and safety assurance, and the promise of formal methods going forward.

Experiences Using Lightweight Formal Methods for Requirements Modeling

NASA Technical Reports Server (NTRS)

Easterbrook, Steve; Lutz, Robyn; Covington, Rick; Kelly, John; Ampo, Yoko; Hamilton, David

1997-01-01

This paper describes three case studies in the lightweight application of formal methods to requirements modeling for spacecraft fault protection systems. The case studies differ from previously reported applications of formal methods in that formal methods were applied very early in the requirements engineering process, to validate the evolving requirements. The results were fed back into the projects, to improve the informal specifications. For each case study, we describe what methods were applied, how they were applied, how much effort was involved, and what the findings were. In all three cases, formal methods enhanced the existing verification and validation processes, by testing key properties of the evolving requirements, and helping to identify weaknesses. We conclude that the benefits gained from early modeling of unstable requirements more than outweigh the effort needed to maintain multiple representations.

Using formal specification in the Guidance and Control Software (GCS) experiment. Formal design and verification technology for life critical systems

NASA Technical Reports Server (NTRS)

Weber, Doug; Jamsek, Damir

1994-01-01

The goal of this task was to investigate how formal methods could be incorporated into a software engineering process for flight-control systems under DO-178B and to demonstrate that process by developing a formal specification for NASA's Guidance and Controls Software (GCS) Experiment. GCS is software to control the descent of a spacecraft onto a planet's surface. The GCS example is simplified from a real example spacecraft, but exhibits the characteristics of realistic spacecraft control software. The formal specification is written in Larch.

Why are Formal Methods Not Used More Widely?

NASA Technical Reports Server (NTRS)

Knight, John C.; DeJong, Colleen L.; Gibble, Matthew S.; Nakano, Luis G.

1997-01-01

Despite extensive development over many years and significant demonstrated benefits, formal methods remain poorly accepted by industrial practitioners. Many reasons have been suggested for this situation such as a claim that they extent the development cycle, that they require difficult mathematics, that inadequate tools exist, and that they are incompatible with other software packages. There is little empirical evidence that any of these reasons is valid. The research presented here addresses the question of why formal methods are not used more widely. The approach used was to develop a formal specification for a safety-critical application using several specification notations and assess the results in a comprehensive evaluation framework. The results of the experiment suggests that there remain many impediments to the routine use of formal methods.

Formal methods and digital systems validation for airborne systems

NASA Technical Reports Server (NTRS)

Rushby, John

1993-01-01

This report has been prepared to supplement a forthcoming chapter on formal methods in the FAA Digital Systems Validation Handbook. Its purpose is as follows: to outline the technical basis for formal methods in computer science; to explain the use of formal methods in the specification and verification of software and hardware requirements, designs, and implementations; to identify the benefits, weaknesses, and difficulties in applying these methods to digital systems used on board aircraft; and to suggest factors for consideration when formal methods are offered in support of certification. These latter factors assume the context for software development and assurance described in RTCA document DO-178B, 'Software Considerations in Airborne Systems and Equipment Certification,' Dec. 1992.

FORMED: Bringing Formal Methods to the Engineering Desktop

DTIC Science & Technology

2016-02-01

integrates formal verification into software design and development by precisely defining semantics for a restricted subset of the Unified Modeling...input-output contract satisfaction and absence of null pointer dereferences. 15. SUBJECT TERMS Formal Methods, Software Verification , Model-Based...Domain specific languages (DSLs) drive both implementation and formal verification

Weaving a Formal Methods Education with Problem-Based Learning

NASA Astrophysics Data System (ADS)

Gibson, J. Paul

The idea of weaving formal methods through computing (or software engineering) degrees is not a new one. However, there has been little success in developing and implementing such a curriculum. Formal methods continue to be taught as stand-alone modules and students, in general, fail to see how fundamental these methods are to the engineering of software. A major problem is one of motivation — how can the students be expected to enthusiastically embrace a challenging subject when the learning benefits, beyond passing an exam and achieving curriculum credits, are not clear? Problem-based learning has gradually moved from being an innovative pedagogique technique, commonly used to better-motivate students, to being widely adopted in the teaching of many different disciplines, including computer science and software engineering. Our experience shows that a good problem can be re-used throughout a student's academic life. In fact, the best computing problems can be used with children (young and old), undergraduates and postgraduates. In this paper we present a process for weaving formal methods through a University curriculum that is founded on the application of problem-based learning and a library of good software engineering problems, where students learn about formal methods without sitting a traditional formal methods module. The process of constructing good problems and integrating them into the curriculum is shown to be analagous to the process of engineering software. This approach is not intended to replace more traditional formal methods modules: it will better prepare students for such specialised modules and ensure that all students have an understanding and appreciation for formal methods even if they do not go on to specialise in them.

Software Formal Inspections Standard

NASA Technical Reports Server (NTRS)

1993-01-01

This Software Formal Inspections Standard (hereinafter referred to as Standard) is applicable to NASA software. This Standard defines the requirements that shall be fulfilled by the software formal inspections process whenever this process is specified for NASA software. The objective of this Standard is to define the requirements for a process that inspects software products to detect and eliminate defects as early as possible in the software life cycle. The process also provides for the collection and analysis of inspection data to improve the inspection process as well as the quality of the software.

Software Safety Progress in NASA

NASA Technical Reports Server (NTRS)

Radley, Charles F.

1995-01-01

NASA has developed guidelines for development and analysis of safety-critical software. These guidelines have been documented in a Guidebook for Safety Critical Software Development and Analysis. The guidelines represent a practical 'how to' approach, to assist software developers and safety analysts in cost effective methods for software safety. They provide guidance in the implementation of the recent NASA Software Safety Standard NSS-1740.13 which was released as 'Interim' version in June 1994, scheduled for formal adoption late 1995. This paper is a survey of the methods in general use, resulting in the NASA guidelines for safety critical software development and analysis.

NASA's Advanced Multimission Operations System: A Case Study in Formalizing Software Architecture Evolution

NASA Technical Reports Server (NTRS)

Barnes, Jeffrey M.

2011-01-01

All software systems of significant size and longevity eventually undergo changes to their basic architectural structure. Such changes may be prompted by evolving requirements, changing technology, or other reasons. Whatever the cause, software architecture evolution is commonplace in real world software projects. Recently, software architecture researchers have begun to study this phenomenon in depth. However, this work has suffered from problems of validation; research in this area has tended to make heavy use of toy examples and hypothetical scenarios and has not been well supported by real world examples. To help address this problem, I describe an ongoing effort at the Jet Propulsion Laboratory to re-architect the Advanced Multimission Operations System (AMMOS), which is used to operate NASA's deep-space and astrophysics missions. Based on examination of project documents and interviews with project personnel, I describe the goals and approach of this evolution effort and then present models that capture some of the key architectural changes. Finally, I demonstrate how approaches and formal methods from my previous research in architecture evolution may be applied to this evolution, while using languages and tools already in place at the Jet Propulsion Laboratory.

Formalizing structured file services for the data storage and retrieval subsystem of the data management system for Spacestation Freedom

NASA Technical Reports Server (NTRS)

Jamsek, Damir A.

1993-01-01

A brief example of the use of formal methods techniques in the specification of a software system is presented. The report is part of a larger effort targeted at defining a formal methods pilot project for NASA. One possible application domain that may be used to demonstrate the effective use of formal methods techniques within the NASA environment is presented. It is not intended to provide a tutorial on either formal methods techniques or the application being addressed. It should, however, provide an indication that the application being considered is suitable for a formal methods by showing how such a task may be started. The particular system being addressed is the Structured File Services (SFS), which is a part of the Data Storage and Retrieval Subsystem (DSAR), which in turn is part of the Data Management System (DMS) onboard Spacestation Freedom. This is a software system that is currently under development for NASA. An informal mathematical development is presented. Section 3 contains the same development using Penelope (23), an Ada specification and verification system. The complete text of the English version Software Requirements Specification (SRS) is reproduced in Appendix A.

(abstract) Formal Inspection Technology Transfer Program

NASA Technical Reports Server (NTRS)

Welz, Linda A.; Kelly, John C.

1993-01-01

A Formal Inspection Technology Transfer Program, based on the inspection process developed by Michael Fagan at IBM, has been developed at JPL. The goal of this program is to support organizations wishing to use Formal Inspections to improve the quality of software and system level engineering products. The Technology Transfer Program provides start-up materials and assistance to help organizations establish their own Formal Inspection program. The course materials and certified instructors associated with the Technology Transfer Program have proven to be effective in classes taught at other NASA centers as well as at JPL. Formal Inspections (NASA tailored Fagan Inspections) are a set of technical reviews whose objective is to increase quality and reduce the cost of software development by detecting and correcting errors early. A primary feature of inspections is the removal of engineering errors before they amplify into larger and more costly problems downstream in the development process. Note that the word 'inspection' is used differently in software than in a manufacturing context. A Formal Inspection is a front-end quality enhancement technique, rather than a task conducted just prior to product shipment for the purpose of sorting defective systems (manufacturing usage). Formal Inspections are supporting and in agreement with the 'total quality' approach being adopted by many NASA centers.

Formal methods for dependable real-time systems

NASA Technical Reports Server (NTRS)

Rushby, John

1993-01-01

The motivation for using formal methods to specify and reason about real time properties is outlined and approaches that were proposed and used are sketched. The formal verifications of clock synchronization algorithms are concluded as showing that mechanically supported reasoning about complex real time behavior is feasible. However, there was significant increase in the effectiveness of verification systems since those verifications were performed, at it is to be expected that verifications of comparable difficulty will become fairly routine. The current challenge lies in developing perspicuous and economical approaches to the formalization and specification of real time properties.

Mending the Gap, An Effort to Aid the Transfer of Formal Methods Technology

NASA Technical Reports Server (NTRS)

Hayhurst, Kelly

2009-01-01

Formal methods can be applied to many of the development and verification activities required for civil avionics software. RTCA/DO-178B, Software Considerations in Airborne Systems and Equipment Certification, gives a brief description of using formal methods as an alternate method of compliance with the objectives of that standard. Despite this, the avionics industry at large has been hesitant to adopt formal methods, with few developers have actually used formal methods for certification credit. Why is this so, given the volume of evidence of the benefits of formal methods? This presentation will explore some of the challenges to using formal methods in a certification context and describe the effort by the Formal Methods Subgroup of RTCA SC-205/EUROCAE WG-71 to develop guidance to make the use of formal methods a recognized approach.

Verification of NASA Emergent Systems

NASA Technical Reports Server (NTRS)

Rouff, Christopher; Vanderbilt, Amy K. C. S.; Truszkowski, Walt; Rash, James; Hinchey, Mike

2004-01-01

NASA is studying advanced technologies for a future robotic exploration mission to the asteroid belt. This mission, the prospective ANTS (Autonomous Nano Technology Swarm) mission, will comprise of 1,000 autonomous robotic agents designed to cooperate in asteroid exploration. The emergent properties of swarm type missions make them powerful, but at the same time are more difficult to design and assure that the proper behaviors will emerge. We are currently investigating formal methods and techniques for verification and validation of future swarm-based missions. The advantage of using formal methods is their ability to mathematically assure the behavior of a swarm, emergent or otherwise. The ANT mission is being used as an example and case study for swarm-based missions for which to experiment and test current formal methods with intelligent swam. Using the ANTS mission, we have evaluated multiple formal methods to determine their effectiveness in modeling and assuring swarm behavior.

Why Engineers Should Consider Formal Methods

NASA Technical Reports Server (NTRS)

Holloway, C. Michael

1997-01-01

This paper presents a logical analysis of a typical argument favoring the use of formal methods for software development, and suggests an alternative argument that is simpler and stronger than the typical one.

NASA publications manual 1974

NASA Technical Reports Server (NTRS)

1974-01-01

The various types of NASA publications are described, including formal series, contributions to external publications, informal papers, and supplementary report material. The physical appearance and reproduction procedures for the format of the NASA formal series are discussed, and samples are provided. Matters relating to organization, content, and general style are also considered.

NASA plan for international crustal dynamics studies

NASA Technical Reports Server (NTRS)

1979-01-01

The international activities being planned as part of the NASA geodynamics program are described. Methods of studying the Earth's crustal movements and deformation characteristics are discussed. The significance of the eventual formalations of earthquake predictions methods is also discussed.

Formal Methods Specification and Verification Guidebook for Software and Computer Systems. Volume 1; Planning and Technology Insertion

NASA Technical Reports Server (NTRS)

1995-01-01

The Formal Methods Specification and Verification Guidebook for Software and Computer Systems describes a set of techniques called Formal Methods (FM), and outlines their use in the specification and verification of computer systems and software. Development of increasingly complex systems has created a need for improved specification and verification techniques. NASA's Safety and Mission Quality Office has supported the investigation of techniques such as FM, which are now an accepted method for enhancing the quality of aerospace applications. The guidebook provides information for managers and practitioners who are interested in integrating FM into an existing systems development process. Information includes technical and administrative considerations that must be addressed when establishing the use of FM on a specific project. The guidebook is intended to aid decision makers in the successful application of FM to the development of high-quality systems at reasonable cost. This is the first volume of a planned two-volume set. The current volume focuses on administrative and planning considerations for the successful application of FM.

Recent trends related to the use of formal methods in software engineering

NASA Technical Reports Server (NTRS)

Prehn, Soren

1986-01-01

An account is given of some recent developments and trends related to the development and use of formal methods in software engineering. Ongoing activities in Europe are focussed on, since there seems to be a notable difference in attitude towards industrial usage of formal methods in Europe and in the U.S. A more detailed account is given of the currently most widespread formal method in Europe: the Vienna Development Method. Finally, the use of Ada is discussed in relation to the application of formal methods, and the potential for constructing Ada-specific tools based on that method is considered.

Evidence Arguments for Using Formal Methods in Software Certification

NASA Technical Reports Server (NTRS)

Denney, Ewen W.; Pai, Ganesh

2013-01-01

We describe a generic approach for automatically integrating the output generated from a formal method/tool into a software safety assurance case, as an evidence argument, by (a) encoding the underlying reasoning as a safety case pattern, and (b) instantiating it using the data produced from the method/tool. We believe this approach not only improves the trustworthiness of the evidence generated from a formal method/tool, by explicitly presenting the reasoning and mechanisms underlying its genesis, but also provides a way to gauge the suitability of the evidence in the context of the wider assurance case. We illustrate our work by application to a real example-an unmanned aircraft system- where we invoke a formal code analysis tool from its autopilot software safety case, automatically transform the verification output into an evidence argument, and then integrate it into the former.

Dominant partition method. [based on a wave function formalism

NASA Technical Reports Server (NTRS)

Dixon, R. M.; Redish, E. F.

1979-01-01

By use of the L'Huillier, Redish, and Tandy (LRT) wave function formalism, a partially connected method, the dominant partition method (DPM) is developed for obtaining few body reductions of the many body problem in the LRT and Bencze, Redish, and Sloan (BRS) formalisms. The DPM maps the many body problem to a fewer body one by using the criterion that the truncated formalism must be such that consistency with the full Schroedinger equation is preserved. The DPM is based on a class of new forms for the irreducible cluster potential, which is introduced in the LRT formalism. Connectivity is maintained with respect to all partitions containing a given partition, which is referred to as the dominant partition. Degrees of freedom corresponding to the breakup of one or more of the clusters of the dominant partition are treated in a disconnected manner. This approach for simplifying the complicated BRS equations is appropriate for physical problems where a few body reaction mechanism prevails.

Formal Requirements-Based Programming for Complex Systems

NASA Technical Reports Server (NTRS)

Rash, James L.; Hinchey, Michael G.; Rouff, Christopher A.; Gracanin, Denis

2005-01-01

Computer science as a field has not yet produced a general method to mechanically transform complex computer system requirements into a provably equivalent implementation. Such a method would be one major step towards dealing with complexity in computing, yet it remains the elusive holy grail of system development. Currently available tools and methods that start with a formal model of a system and mechanically produce a provably equivalent implementation are valuable but not sufficient. The gap that such tools and methods leave unfilled is that the formal models cannot be proven to be equivalent to the system requirements as originated by the customer For the classes of complex systems whose behavior can be described as a finite (but significant) set of scenarios, we offer a method for mechanically transforming requirements (expressed in restricted natural language, or appropriate graphical notations) into a provably equivalent formal model that can be used as the basis for code generation and other transformations. While other techniques are available, this method is unique in offering full mathematical tractability while using notations and techniques that are well known and well trusted. We illustrate the application of the method to an example procedure from the Hubble Robotic Servicing Mission currently under study and preliminary formulation at NASA Goddard Space Flight Center.

Applying formal methods and object-oriented analysis to existing flight software

NASA Technical Reports Server (NTRS)

Cheng, Betty H. C.; Auernheimer, Brent

1993-01-01

Correctness is paramount for safety-critical software control systems. Critical software failures in medical radiation treatment, communications, and defense are familiar to the public. The significant quantity of software malfunctions regularly reported to the software engineering community, the laws concerning liability, and a recent NRC Aeronautics and Space Engineering Board report additionally motivate the use of error-reducing and defect detection software development techniques. The benefits of formal methods in requirements driven software development ('forward engineering') is well documented. One advantage of rigorously engineering software is that formal notations are precise, verifiable, and facilitate automated processing. This paper describes the application of formal methods to reverse engineering, where formal specifications are developed for a portion of the shuttle on-orbit digital autopilot (DAP). Three objectives of the project were to: demonstrate the use of formal methods on a shuttle application, facilitate the incorporation and validation of new requirements for the system, and verify the safety-critical properties to be exhibited by the software.

Integrating Formal Methods and Testing 2002

NASA Technical Reports Server (NTRS)

Cukic, Bojan

2002-01-01

Traditionally, qualitative program verification methodologies and program testing are studied in separate research communities. None of them alone is powerful and practical enough to provide sufficient confidence in ultra-high reliability assessment when used exclusively. Significant advances can be made by accounting not only tho formal verification and program testing. but also the impact of many other standard V&V techniques, in a unified software reliability assessment framework. The first year of this research resulted in the statistical framework that, given the assumptions on the success of the qualitative V&V and QA procedures, significantly reduces the amount of testing needed to confidently assess reliability at so-called high and ultra-high levels (10-4 or higher). The coming years shall address the methodologies to realistically estimate the impacts of various V&V techniques to system reliability and include the impact of operational risk to reliability assessment. Combine formal correctness verification, process and product metrics, and other standard qualitative software assurance methods with statistical testing with the aim of gaining higher confidence in software reliability assessment for high-assurance applications. B) Quantify the impact of these methods on software reliability. C) Demonstrate that accounting for the effectiveness of these methods reduces the number of tests needed to attain certain confidence level. D) Quantify and justify the reliability estimate for systems developed using various methods.

Formal Methods of V&V of Partial Specifications: An Experience Report

NASA Technical Reports Server (NTRS)

Easterbrook, Steve; Callahan, John

1997-01-01

This paper describes our work exploring the suitability of formal specification methods for independent verification and validation (IV&V) of software specifications for large, safety critical systems. An IV&V contractor often has to perform rapid analysis on incomplete specifications, with no control over how those specifications are represented. Lightweight formal methods show significant promise in this context, as they offer a way of uncovering major errors, without the burden of full proofs of correctness. We describe an experiment in the application of the method SCR. to testing for consistency properties of a partial model of requirements for Fault Detection Isolation and Recovery on the space station. We conclude that the insights gained from formalizing a specification is valuable, and it is the process of formalization, rather than the end product that is important. It was only necessary to build enough of the formal model to test the properties in which we were interested. Maintenance of fidelity between multiple representations of the same requirements (as they evolve) is still a problem, and deserves further study.

On the Need for Practical Formal Methods

DTIC Science & Technology

1998-01-01

additional research and engineering that is needed to make the current set of formal methods more practical. To illustrate the ideas, I present several exam ...either a good violin or a highly talented violinist. Light-weight techniques o er software developers good violins . A user need not be a talented

Building a Formal Model of a Human-Interactive System: Insights into the Integration of Formal Methods and Human Factors Engineering

NASA Technical Reports Server (NTRS)

Bolton, Matthew L.; Bass, Ellen J.

2009-01-01

Both the human factors engineering (HFE) and formal methods communities are concerned with finding and eliminating problems with safety-critical systems. This work discusses a modeling effort that leveraged methods from both fields to use model checking with HFE practices to perform formal verification of a human-interactive system. Despite the use of a seemingly simple target system, a patient controlled analgesia pump, the initial model proved to be difficult for the model checker to verify in a reasonable amount of time. This resulted in a number of model revisions that affected the HFE architectural, representativeness, and understandability goals of the effort. If formal methods are to meet the needs of the HFE community, additional modeling tools and technological developments are necessary.

Formal Method of Description Supporting Portfolio Assessment

ERIC Educational Resources Information Center

Morimoto, Yasuhiko; Ueno, Maomi; Kikukawa, Isao; Yokoyama, Setsuo; Miyadera, Youzou

2006-01-01

Teachers need to assess learner portfolios in the field of education. However, they need support in the process of designing and practicing what kind of portfolios are to be assessed. To solve the problem, a formal method of describing the relations between the lesson forms and portfolios that need to be collected and the relations between…

Formal Methods for Verification and Validation of Partial Specifications: A Case Study

NASA Technical Reports Server (NTRS)

Easterbrook, Steve; Callahan, John

1997-01-01

This paper describes our work exploring the suitability of formal specification methods for independent verification and validation (IV&V) of software specifications for large, safety critical systems. An IV&V contractor often has to perform rapid analysis on incomplete specifications, with no control over how those specifications are represented. Lightweight formal methods show significant promise in this context, as they offer a way of uncovering major errors, without the burden of full proofs of correctness. We describe a case study of the use of partial formal models for V&V of the requirements for Fault Detection Isolation and Recovery on the space station. We conclude that the insights gained from formalizing a specification are valuable, and it is the process of formalization, rather than the end product that is important. It was only necessary to build enough of the formal model to test the properties in which we were interested. Maintenance of fidelity between multiple representations of the same requirements (as they evolve) is still a problem, and deserves further study.

Formal Methods for Automated Diagnosis of Autosub 6000

NASA Technical Reports Server (NTRS)

Ernits, Juhan; Dearden, Richard; Pebody, Miles

2009-01-01

This is a progress report on applying formal methods in the context of building an automated diagnosis and recovery system for Autosub 6000, an Autonomous Underwater Vehicle (AUV). The diagnosis task involves building abstract models of the control system of the AUV. The diagnosis engine is based on Livingstone 2, a model-based diagnoser originally built for aerospace applications. Large parts of the diagnosis model can be built without concrete knowledge about each mission, but actual mission scripts and configuration parameters that carry important information for diagnosis are changed for every mission. Thus we use formal methods for generating the mission control part of the diagnosis model automatically from the mission script and perform a number of invariant checks to validate the configuration. After the diagnosis model is augmented with the generated mission control component model, it needs to be validated using verification techniques.

Applications of Formal Methods to Specification and Safety of Avionics Software

NASA Technical Reports Server (NTRS)

Hoover, D. N.; Guaspari, David; Humenn, Polar

1996-01-01

This report treats several topics in applications of formal methods to avionics software development. Most of these topics concern decision tables, an orderly, easy-to-understand format for formally specifying complex choices among alternative courses of action. The topics relating to decision tables include: generalizations fo decision tables that are more concise and support the use of decision tables in a refinement-based formal software development process; a formalism for systems of decision tables with behaviors; an exposition of Parnas tables for users of decision tables; and test coverage criteria and decision tables. We outline features of a revised version of ORA's decision table tool, Tablewise, which will support many of the new ideas described in this report. We also survey formal safety analysis of specifications and software.

Applying Various Methods of Communicating Science for Community Decision-Making and Public Awareness: A NASA DEVELOP National Program Case Study

NASA Astrophysics Data System (ADS)

Miller, T. N.; Brumbaugh, E. J.; Barker, M.; Ly, V.; Schick, R.; Rogers, L.

2015-12-01

The NASA DEVELOP National Program conducts over eighty Earth science projects every year. Each project applies NASA Earth observations to impact decision-making related to a local or regional community concern. Small, interdisciplinary teams create a methodology to address the specific issue, and then pass on the results to partner organizations, as well as providing them with instruction to continue using remote sensing for future decisions. Many different methods are used by individual teams, and the program as a whole, to communicate results and research accomplishments to decision-makers, stakeholders, alumni, and the general public. These methods vary in scope from formal publications to more informal venues, such as social media. This presentation will highlight the communication techniques used by the DEVELOP program. Audiences, strategies, and outlets will be discussed, including a newsletter, microjournal, video contest, and several others.

Formal methods and their role in digital systems validation for airborne systems

NASA Technical Reports Server (NTRS)

Rushby, John

1995-01-01

This report is based on one prepared as a chapter for the FAA Digital Systems Validation Handbook (a guide to assist FAA certification specialists with advanced technology issues). Its purpose is to explain the use of formal methods in the specification and verification of software and hardware requirements, designs, and implementations; to identify the benefits, weaknesses, and difficulties in applying these methods to digital systems used in critical applications; and to suggest factors for consideration when formal methods are offered in support of certification. The presentation concentrates on the rationale for formal methods and on their contribution to assurance for critical applications within a context such as that provided by DO-178B (the guidelines for software used on board civil aircraft); it is intended as an introduction for those to whom these topics are new.

Properties of a Formal Method to Model Emergence in Swarm-Based Systems

NASA Technical Reports Server (NTRS)

Rouff, Christopher; Vanderbilt, Amy; Truszkowski, Walt; Rash, James; Hinchey, Mike

2004-01-01

Future space missions will require cooperation between multiple satellites and/or rovers. Developers are proposing intelligent autonomous swarms for these missions, but swarm-based systems are difficult or impossible to test with current techniques. This viewgraph presentation examines the use of formal methods in testing swarm-based systems. The potential usefulness of formal methods in modeling the ANTS asteroid encounter mission is also examined.

Formal Solutions for Polarized Radiative Transfer. II. High-order Methods

DOE Office of Scientific and Technical Information (OSTI.GOV)

Janett, Gioele; Steiner, Oskar; Belluzzi, Luca, E-mail: gioele.janett@irsol.ch

When integrating the radiative transfer equation for polarized light, the necessity of high-order numerical methods is well known. In fact, well-performing high-order formal solvers enable higher accuracy and the use of coarser spatial grids. Aiming to provide a clear comparison between formal solvers, this work presents different high-order numerical schemes and applies the systematic analysis proposed by Janett et al., emphasizing their advantages and drawbacks in terms of order of accuracy, stability, and computational cost.

NASA USAID Memorandum of Understanding

NASA Image and Video Library

2011-04-25

USAID Administrator Rajiv Shahspeaks prior to signing a five-year memorandum of understanding with NASA, Monday, April 25, 2011, at NASA Headquarters in Washington. The agreement formalizes ongoing agency collaborations that use Earth science data to address developmental challenges, and to assist in disaster mitigation and humanitarian responses. The agreement also encourages NASA and USAID to apply geospatial technologies to solve development challenges affecting the United States and developing countries. Photo Credit: (NASA/Paul E. Alers)

NASA USAID Memorandum of Understanding

NASA Image and Video Library

2011-04-25

USAID Administrator Rajiv Shah, left, and NASA Administrator Charles Bolden sign a five-year memorandum of understanding, Monday, April 25, 2011, at NASA Headquarters in Washington. The agreement formalizes ongoing agency collaborations that use Earth science data to address developmental challenges, and to assist in disaster mitigation and humanitarian responses. The agreement also encourages NASA and USAID to apply geospatial technologies to solve development challenges affecting the United States and developing countries. Photo Credit: (NASA/Paul E. Alers)

NASA USAID Memorandum of Understanding

NASA Image and Video Library

2011-04-25

USAID Administrator Rajiv Shah speaks prior to signing a five-year memorandum of understanding with NASA, Monday, April 25, 2011, at NASA Headquarters in Washington. The agreement formalizes ongoing agency collaborations that use Earth science data to address developmental challenges, and to assist in disaster mitigation and humanitarian responses. The agreement also encourages NASA and USAID to apply geospatial technologies to solve development challenges affecting the United States and developing countries. Photo Credit: (NASA/Paul E. Alers)

A High-Level Formalization of Floating-Point Number in PVS

NASA Technical Reports Server (NTRS)

Boldo, Sylvie; Munoz, Cesar

2006-01-01

We develop a formalization of floating-point numbers in PVS based on a well-known formalization in Coq. We first describe the definitions of all the needed notions, e.g., floating-point number, format, rounding modes, etc.; then, we present an application to polynomial evaluation for elementary function evaluation. The application already existed in Coq, but our formalization shows a clear improvement in the quality of the result due to the automation provided by PVS. We finally integrate our formalization into a PVS hardware-level formalization of the IEEE-854 standard previously developed at NASA.

Systems, methods and apparatus for implementation of formal specifications derived from informal requirements

NASA Technical Reports Server (NTRS)

Hinchey, Michael G. (Inventor); Rouff, Christopher A. (Inventor); Rash, James L. (Inventor); Erickson, John D. (Inventor); Gracinin, Denis (Inventor)

2010-01-01

Systems, methods and apparatus are provided through which in some embodiments an informal specification is translated without human intervention into a formal specification. In some embodiments the formal specification is a process-based specification. In some embodiments, the formal specification is translated into a high-level computer programming language which is further compiled into a set of executable computer instructions.

NASA systems engineering handbook

NASA Astrophysics Data System (ADS)

Shishko, Robert; Aster, Robert; Chamberlain, Robert G.; McDuffee, Patrick; Pieniazek, Les; Rowell, Tom; Bain, Beth; Cox, Renee I.; Mooz, Harold; Polaski, Lou

1995-06-01

This handbook brings the fundamental concepts and techniques of systems engineering to NASA personnel in a way that recognizes the nature of NASA systems and environment. It is intended to accompany formal NASA training courses on systems engineering and project management when appropriate, and is designed to be a top-level overview. The concepts were drawn from NASA field center handbooks, NMI's/NHB's, the work of the NASA-wide Systems Engineering Working Group and the Systems Engineering Process Improvement Task team, several non-NASA textbooks and guides, and material from independent systems engineering courses taught to NASA personnel. Five core chapters cover systems engineering fundamentals, the NASA Project Cycle, management issues in systems engineering, systems analysis and modeling, and specialty engineering integration. It is not intended as a directive.

NASA USAID Memorandum of Understanding

NASA Image and Video Library

2011-04-25

USAID Administrator Rajiv Shah, left, and NASA Administrator Charles Bolden shake hands after signing a five-year memorandum of understanding, Monday, April 25, 2011, at NASA Headquarters in Washington. The agreement formalizes ongoing agency collaborations that use Earth science data to address developmental challenges, and to assist in disaster mitigation and humanitarian responses. The agreement also encourages NASA and USAID to apply geospatial technologies to solve development challenges affecting the United States and developing countries. Photo Credit: (NASA/Paul E. Alers)

Ten Commandments Revisited: A Ten-Year Perspective on the Industrial Application of Formal Methods

NASA Technical Reports Server (NTRS)

Bowen, Jonathan P.; Hinchey, Michael G.

2005-01-01

Ten years ago, our 1995 paper Ten Commandments of Formal Methods suggested some guidelines to help ensure the success of a formal methods project. It proposed ten important requirements (or "commandments") for formal developers to consider and follow, based on our knowledge of several industrial application success stories, most of which have been reported in more detail in two books. The paper was surprisingly popular, is still widely referenced, and used as required reading in a number of formal methods courses. However, not all have agreed with some of our commandments, feeling that they may not be valid in the long-term. We re-examine the original commandments ten years on, and consider their validity in the light of a further decade of industrial best practice and experiences.

NASA Systems Engineering Handbook

NASA Technical Reports Server (NTRS)

Shishko, Robert; Aster, Robert; Chamberlain, Robert G.; Mcduffee, Patrick; Pieniazek, Les; Rowell, Tom; Bain, Beth; Cox, Renee I.; Mooz, Harold; Polaski, Lou

1995-01-01

This handbook brings the fundamental concepts and techniques of systems engineering to NASA personnel in a way that recognizes the nature of NASA systems and environment. It is intended to accompany formal NASA training courses on systems engineering and project management when appropriate, and is designed to be a top-level overview. The concepts were drawn from NASA field center handbooks, NMI's/NHB's, the work of the NASA-wide Systems Engineering Working Group and the Systems Engineering Process Improvement Task team, several non-NASA textbooks and guides, and material from independent systems engineering courses taught to NASA personnel. Five core chapters cover systems engineering fundamentals, the NASA Project Cycle, management issues in systems engineering, systems analysis and modeling, and specialty engineering integration. It is not intended as a directive. Superseded by: NASA/SP-2007-6105 Rev 1 (20080008301).

Survey of NASA V and V Processes/Methods

NASA Technical Reports Server (NTRS)

Pecheur, Charles; Nelson, Stacy

2002-01-01

The purpose of this report is to describe current NASA Verification and Validation (V&V) techniques and to explain how these techniques are applicable to 2nd Generation RLV Integrated Vehicle Health Management (IVHM) software. It also contains recommendations for special V&V requirements for IVHM. This report is divided into the following three sections: 1) Survey - Current NASA V&V Processes/Methods; 2) Applicability of NASA V&V to 2nd Generation RLV IVHM; and 3) Special 2nd Generation RLV IVHM V&V Requirements.

Formal methods in the design of Ada 1995

NASA Technical Reports Server (NTRS)

Guaspari, David

1995-01-01

Formal, mathematical methods are most useful when applied early in the design and implementation of a software system--that, at least, is the familiar refrain. I will report on a modest effort to apply formal methods at the earliest possible stage, namely, in the design of the Ada 95 programming language itself. This talk is an 'experience report' that provides brief case studies illustrating the kinds of problems we worked on, how we approached them, and the extent (if any) to which the results proved useful. It also derives some lessons and suggestions for those undertaking future projects of this kind. Ada 95 is the first revision of the standard for the Ada programming language. The revision began in 1988, when the Ada Joint Programming Office first asked the Ada Board to recommend a plan for revising the Ada standard. The first step in the revision was to solicit criticisms of Ada 83. A set of requirements for the new language standard, based on those criticisms, was published in 1990. A small design team, the Mapping Revision Team (MRT), became exclusively responsible for revising the language standard to satisfy those requirements. The MRT, from Intermetrics, is led by S. Tucker Taft. The work of the MRT was regularly subject to independent review and criticism by a committee of distinguished Reviewers and by several advisory teams--for example, the two User/Implementor teams, each consisting of an industrial user (attempting to make significant use of the new language on a realistic application) and a compiler vendor (undertaking, experimentally, to modify its current implementation in order to provide the necessary new features). One novel decision established the Language Precision Team (LPT), which investigated language proposals from a mathematical point of view. The LPT applied formal mathematical analysis to help improve the design of Ada 95 (e.g., by clarifying the language proposals) and to help promote its acceptance (e.g., by identifying a

NASA Publications Guide

NASA Technical Reports Server (NTRS)

1982-01-01

The publication programs and management policies of NASA are described and the details that authors and publication specialists need to know to carry out the agency's mission of disseminating the scientific and technical information derived from its activities are highlighted. Topics covered include the various kinds of NASA formal publications; selection of publication medium; printing and distribution; and requirements concerning style and format standards, copyright transfers, the cover, color, and foldouts. The sections of a report are delineated and editorial and page make-up responsibilities are also discussed.

Method of Fabricating NASA-Standard Macro-Fiber Composite Piezoelectric Actuators

NASA Technical Reports Server (NTRS)

High, James W.; Wilkie, W. Keats

2003-01-01

The NASA Macro-Fiber Composite actuator is a flexible piezoelectric composite device designed for controlling vibrations and shape deformations in high performance aerospace structures. A complete method for fabricating the standard NASA Macro-Fiber Composite actuator is presented in this document. When followed precisely, these procedures will yield devices with electromechanical properties identical to the standard actuator manufactured by NASA Langley Research Center.

Science@NASA: Direct to People Via the Internet

NASA Technical Reports Server (NTRS)

Koczor, R. J.; Phillips, T.; Whitaker, Ann F. (Technical Monitor)

2001-01-01

NASA's founding charter includes the requirement for reporting all scientific results to the public. This requirement is based on the principal that the exploration of space results in real benefits to humanity and that those benefits are to be shared as widely as practical. When NASA was founded, the traditional education and outreach methods were through the news media and the formal and informal (museums, planetariums exhibits, etc.) educational communities. With the nearly ubiquitous availability of the Internet, a third choice presents itself: communicating directly with individuals in their homes. This powerful approach offers benefits and pitfalls that must be addressed to be effective. This paper covers an integrated approach to providing high quality NASA research information to multiple audiences via a family of websites. The paper discuss the content generation, review, and production process and provide metrics on evaluating the results.

Formal Assurance Certifiable Tooling Formal Assurance Certifiable Tooling Strategy Final Report

NASA Technical Reports Server (NTRS)

Bush, Eric; Oglesby, David; Bhatt, Devesh; Murugesan, Anitha; Engstrom, Eric; Mueller, Joe; Pelican, Michael

2017-01-01

This is the Final Report of a research project to investigate issues and provide guidance for the qualification of formal methods tools under the DO-330 qualification process. It consisted of three major subtasks spread over two years: 1) an assessment of theoretical soundness issues that may affect qualification for three categories of formal methods tools, 2) a case study simulating the DO-330 qualification of two actual tool sets, and 3) an investigation of risk mitigation strategies that might be applied to chains of such formal methods tools in order to increase confidence in their certification of airborne software.

A New Look at NASA: Strategic Research In Information Technology

NASA Technical Reports Server (NTRS)

Alfano, David; Tu, Eugene (Technical Monitor)

2002-01-01

This viewgraph presentation provides information on research undertaken by NASA to facilitate the development of information technologies. Specific ideas covered here include: 1) Bio/nano technologies: biomolecular and nanoscale systems and tools for assembly and computing; 2) Evolvable hardware: autonomous self-improving, self-repairing hardware and software for survivable space systems in extreme environments; 3) High Confidence Software Technologies: formal methods, high-assurance software design, and program synthesis; 4) Intelligent Controls and Diagnostics: Next generation machine learning, adaptive control, and health management technologies; 5) Revolutionary computing: New computational models to increase capability and robustness to enable future NASA space missions.

Towards the formal specification of the requirements and design of a processor interface unit

NASA Technical Reports Server (NTRS)

Fura, David A.; Windley, Phillip J.; Cohen, Gerald C.

1993-01-01

Work to formally specify the requirements and design of a Processor Interface Unit (PIU), a single-chip subsystem providing memory interface, bus interface, and additional support services for a commercial microprocessor within a fault-tolerant computer system, is described. This system, the Fault-Tolerant Embedded Processor (FTEP), is targeted towards applications in avionics and space requiring extremely high levels of mission reliability, extended maintenance free operation, or both. The approaches that were developed for modeling the PIU requirements and for composition of the PIU subcomponents at high levels of abstraction are described. These approaches were used to specify and verify a nontrivial subset of the PIU behavior. The PIU specification in Higher Order Logic (HOL) is documented in a companion NASA contractor report entitled 'Towards the Formal Specification of the Requirements and Design of a Processor Interfacs Unit - HOL Listings.' The subsequent verification approach and HOL listings are documented in NASA contractor report entitled 'Towards the Formal Verification of the Requirements and Design of a Processor Interface Unit' and NASA contractor report entitled 'Towards the Formal Verification of the Requirements and Design of a Processor Interface Unit - HOL Listings.'

Formal Modeling and Analysis of a Preliminary Small Aircraft Transportation System (SATS)Concept

NASA Technical Reports Server (NTRS)

Carrreno, Victor A.; Gottliebsen, Hanne; Butler, Ricky; Kalvala, Sara

2004-01-01

New concepts for automating air traffic management functions at small non-towered airports raise serious safety issues associated with the software implementations and their underlying key algorithms. The criticality of such software systems necessitates that strong guarantees of the safety be developed for them. In this paper we present a formal method for modeling and verifying such systems using the PVS theorem proving system. The method is demonstrated on a preliminary concept of operation for the Small Aircraft Transportation System (SATS) project at NASA Langley.

Formal Verification for a Next-Generation Space Shuttle

NASA Technical Reports Server (NTRS)

Nelson, Stacy D.; Pecheur, Charles; Koga, Dennis (Technical Monitor)

2002-01-01

This paper discusses the verification and validation (V&2) of advanced software used for integrated vehicle health monitoring (IVHM), in the context of NASA's next-generation space shuttle. We survey the current VBCV practice and standards used in selected NASA projects, review applicable formal verification techniques, and discuss their integration info existing development practice and standards. We also describe two verification tools, JMPL2SMV and Livingstone PathFinder, that can be used to thoroughly verify diagnosis applications that use model-based reasoning, such as the Livingstone system.

Formal assessment instrument for ensuring the security of NASA's networks, systems and software

NASA Technical Reports Server (NTRS)

Gilliam, D. P.; Powell, J. D.; Sherif, J.

2002-01-01

To address the problem of security for NASA's networks, systems and software, NASA has funded the Jet Propulsion Lab in conjunction with UC Davis to begin work on developing a software security assessment instrument for use in the software development and maintenance life cycle.

NASA Safety Standard: Guidelines and Assessment Procedures for Limiting Orbital Debris

NASA Technical Reports Server (NTRS)

1995-01-01

Collision with orbital debris is a hazard of growing concern as historically accepted practices and procedures have allowed man-made objects to accumulate in orbit. To limit future debris generation, NASA Management Instruction (NMI) 1700.8, 'Policy to Limit Orbital Debris Generation,' was issued in April of 1993. The NMI requires each program to conduct a formal assessment of the potential to generate orbital debris. This document serves as a companion to NMI 1700.08 and provides each NASA program with specific guidelines and assessment methods to assure compliance with the NMI. Each main debris assessment issue (e.g., Post Mission Disposal) is developed in a separate chapter.

Stopping power of dense plasmas: The collisional method and limitations of the dielectric formalism.

PubMed

Clauser, C F; Arista, N R

2018-02-01

We present a study of the stopping power of plasmas using two main approaches: the collisional (scattering theory) and the dielectric formalisms. In the former case, we use a semiclassical method based on quantum scattering theory. In the latter case, we use the full description given by the extension of the Lindhard dielectric function for plasmas of all degeneracies. We compare these two theories and show that the dielectric formalism has limitations when it is used for slow heavy ions or atoms in dense plasmas. We present a study of these limitations and show the regimes where the dielectric formalism can be used, with appropriate corrections to include the usual quantum and classical limits. On the other hand, the semiclassical method shows the correct behavior for all plasma conditions and projectile velocity and charge. We consider different models for the ion charge distributions, including bare and dressed ions as well as neutral atoms.

Can Regulatory Bodies Expect Efficient Help from Formal Methods?

NASA Technical Reports Server (NTRS)

Lopez Ruiz, Eduardo R.; Lemoine, Michel

2010-01-01

In the context of EDEMOI - a French national project that proposed the use of semiformal and formal methods to infer the consistency and robustness of aeronautical regulations through the analysis of faithfully representative models- a methodology had been suggested (and applied) to different (safety and security-related) aeronautical regulations. This paper summarizes the preliminary results of this experience by stating which were the methodology s expected benefits, from a scientific point of view, and which are its useful benefits, from a regulatory body s point of view.

National Aeronautics and Space Administration (NASA) Education 1993-2009

ERIC Educational Resources Information Center

Ivie, Christine M.

2009-01-01

The National Aeronautics and Space Administration was established in 1958 and began operating a formal education program in 1993. The purpose of this study was to analyze the education program from 1993-2009 by examining strategic plan documents produced by the NASA education office and interviewing NASA education officials who served during that…

NASA propagation information center

NASA Technical Reports Server (NTRS)

Smith, Ernest K.; Flock, Warren L.

1990-01-01

The NASA Propagation Information Center became formally operational in July 1988. It is located in the Department of Electrical and Computer Engineering of the University of Colorado at Boulder. The center is several things: a communications medium for the propagation with the outside world, a mechanism for internal communication within the program, and an aid to management.

NASA Propagation Information Center

NASA Technical Reports Server (NTRS)

Smith, Ernest K.; Flock, Warren L.

1989-01-01

The NASA Propagation Information Center became formally operational in July 1988. It is located in the Department of Electrical and Computer Engineering of the University of Colorado at Boulder. The Center is several things: a communications medium for the propagation with the outside world, a mechanism for internal communication within the program, and an aid to management.

Technical publications of the NASA Wallops Flight Facility, 1980 through 1983

NASA Technical Reports Server (NTRS)

Foster, J. N.

1984-01-01

This bibliography lists the publications sponsored by the NASA Wallops Flight Center/NASA Goddard Space Flight Center, Wallops Flight Facility during the period 1980 through 1983. The compilation contains citations listed by type of publication; i.e., NASA formal report, NASA contractor report, journal article, or presentation; by contract/grant number; and by accession number. Oceanography, astrophysics, artificial satellites, fluid mechanics, and sea ice are among the topics covered.

The HACMS program: using formal methods to eliminate exploitable bugs

PubMed Central

Launchbury, John; Richards, Raymond

2017-01-01

For decades, formal methods have offered the promise of verified software that does not have exploitable bugs. Until recently, however, it has not been possible to verify software of sufficient complexity to be useful. Recently, that situation has changed. SeL4 is an open-source operating system microkernel efficient enough to be used in a wide range of practical applications. Its designers proved it to be fully functionally correct, ensuring the absence of buffer overflows, null pointer exceptions, use-after-free errors, etc., and guaranteeing integrity and confidentiality. The CompCert Verifying C Compiler maps source C programs to provably equivalent assembly language, ensuring the absence of exploitable bugs in the compiler. A number of factors have enabled this revolution, including faster processors, increased automation, more extensive infrastructure, specialized logics and the decision to co-develop code and correctness proofs rather than verify existing artefacts. In this paper, we explore the promise and limitations of current formal-methods techniques. We discuss these issues in the context of DARPA’s HACMS program, which had as its goal the creation of high-assurance software for vehicles, including quadcopters, helicopters and automobiles. This article is part of the themed issue ‘Verified trustworthy software systems’. PMID:28871050

The HACMS program: using formal methods to eliminate exploitable bugs.

PubMed

Fisher, Kathleen; Launchbury, John; Richards, Raymond

2017-10-13

For decades, formal methods have offered the promise of verified software that does not have exploitable bugs. Until recently, however, it has not been possible to verify software of sufficient complexity to be useful. Recently, that situation has changed. SeL4 is an open-source operating system microkernel efficient enough to be used in a wide range of practical applications. Its designers proved it to be fully functionally correct, ensuring the absence of buffer overflows, null pointer exceptions, use-after-free errors, etc., and guaranteeing integrity and confidentiality. The CompCert Verifying C Compiler maps source C programs to provably equivalent assembly language, ensuring the absence of exploitable bugs in the compiler. A number of factors have enabled this revolution, including faster processors, increased automation, more extensive infrastructure, specialized logics and the decision to co-develop code and correctness proofs rather than verify existing artefacts. In this paper, we explore the promise and limitations of current formal-methods techniques. We discuss these issues in the context of DARPA's HACMS program, which had as its goal the creation of high-assurance software for vehicles, including quadcopters, helicopters and automobiles.This article is part of the themed issue 'Verified trustworthy software systems'. © 2017 The Authors.

NASA metrology and calibration, 1993

NASA Technical Reports Server (NTRS)

1993-01-01

Th sixteenth annual workshop of NASA's Metrology and Calibration Working Group was held April 20-22, 1993. The goals of the Working Group are to provide Agencywide standardization of individual metrology programs, where appropriate; to promote cooperation and exchange of information within NASA, with other Government agencies, and with industry; to serve as the primary Agency interface with the National Institute of Standards and Technology; and to encourage formal quality control techniques such as Measurement Assurance Programs. These proceedings contain unedited reports and presentations from the workshop and are provided for information only.

Using formal methods for content validation of medical procedure documents.

PubMed

Cota, Érika; Ribeiro, Leila; Bezerra, Jonas Santos; Costa, Andrei; da Silva, Rosiana Estefane; Cota, Gláucia

2017-08-01

We propose the use of a formal approach to support content validation of a standard operating procedure (SOP) for a therapeutic intervention. Such an approach provides a useful tool to identify ambiguities, omissions and inconsistencies, and improves the applicability and efficacy of documents in the health settings. We apply and evaluate a methodology originally proposed for the verification of software specification documents to a specific SOP. The verification methodology uses the graph formalism to model the document. Semi-automatic analysis identifies possible problems in the model and in the original document. The verification is an iterative process that identifies possible faults in the original text that should be revised by its authors and/or specialists. The proposed method was able to identify 23 possible issues in the original document (ambiguities, omissions, redundant information, and inaccuracies, among others). The formal verification process aided the specialists to consider a wider range of usage scenarios and to identify which instructions form the kernel of the proposed SOP and which ones represent additional or required knowledge that are mandatory for the correct application of the medical document. By using the proposed verification process, a simpler and yet more complete SOP could be produced. As consequence, during the validation process the experts received a more mature document and could focus on the technical aspects of the procedure itself. Copyright © 2017 Elsevier B.V. All rights reserved.

The Development of NASA's Fault Management Handbook

NASA Technical Reports Server (NTRS)

Dennehy, Cornelius J.; Fesq, Lorraine M.; Barth, Timothy; Clark, Micah; Day, John; Fretz, Kristen; Friberg, Kenneth; Johnson, Stephen; Hattis, Philip; McComas, David;

Operations planning and analysis handbook for NASA/MSFC phase B development projects

NASA Technical Reports Server (NTRS)

Batson, Robert C.

1986-01-01

Current operations planning and analysis practices on NASA/MSFC Phase B projects were investigated with the objectives of (1) formalizing these practices into a handbook and (2) suggesting improvements. The study focused on how Science and Engineering (S&E) Operational Personnel support Program Development (PD) Task Teams. The intimate relationship between systems engineering and operations analysis was examined. Methods identified for use by operations analysts during Phase B include functional analysis, interface analysis methods to calculate/allocate such criteria as reliability, Maintainability, and operations and support cost.

Whatever Happened to Formal Methods for Security?

PubMed

Voas, J; Schaffer, K

2016-08-01

We asked 7 experts 7 questions to find out what has occurred recently in terms of applying formal methods (FM) to security-centric, cyber problems. We are continually reminded of the 1996 paper by Tony Hoare "How did Software Get So Reliable Without Proof?" [1] In that vein, how did we get so insecure with proof? Given daily press announcements concerning new malware, data breaches, and privacy loss, is FM still relevant or was it ever? Our experts answered with unique personal insights. We were curious as to whether this successful methodology in "safety-critical" has succeeded as well for today's "build it, hack it, patch it" mindset. Our experts were John McLean (Naval Research Labs), Paul Black (National Institute of Standards and Technology), Karl Levitt (University of California at Davis), Joseph Williams (CloudEconomist.Com), Connie Heitmeyer (Naval Research Labs), Eugene Spafford (Purdue University), and Joseph Kiniry (Galois, Inc.). The questions and responses follow.

Whatever Happened to Formal Methods for Security?

PubMed Central

Voas, J.; Schaffer, K.

2016-01-01

We asked 7 experts 7 questions to find out what has occurred recently in terms of applying formal methods (FM) to security-centric, cyber problems. We are continually reminded of the 1996 paper by Tony Hoare “How did Software Get So Reliable Without Proof?” [1] In that vein, how did we get so insecure with proof? Given daily press announcements concerning new malware, data breaches, and privacy loss, is FM still relevant or was it ever? Our experts answered with unique personal insights. We were curious as to whether this successful methodology in “safety-critical” has succeeded as well for today’s “build it, hack it, patch it” mindset. Our experts were John McLean (Naval Research Labs), Paul Black (National Institute of Standards and Technology), Karl Levitt (University of California at Davis), Joseph Williams (CloudEconomist.Com), Connie Heitmeyer (Naval Research Labs), Eugene Spafford (Purdue University), and Joseph Kiniry (Galois, Inc.). The questions and responses follow. PMID:27890940

NASA Principal Center for Review of Clean Air Act Regulations

NASA Technical Reports Server (NTRS)

Clark-Ingram, Marceia; Munafo, Paul M. (Technical Monitor)

2002-01-01

The Clean Air Act (CAA) regulations have greatly impacted materials and processes utilized in the manufacture of aerospace hardware. Code JE/ NASA's Environmental Management Division at NASA Headquarters recognized the need for a formal, Agency-wide review process of CAA regulations. Marshall Space Flight Center (MSFC) was selected as the 'Principal Center for Review of Clean Air Act Regulations'. This presentation describes the centralized support provided by MSFC for the management and leadership of NASA's CAA regulation review process.

Location priority for non-formal early childhood education school based on promethee method and map visualization

NASA Astrophysics Data System (ADS)

Ayu Nurul Handayani, Hemas; Waspada, Indra

2018-05-01

Non-formal Early Childhood Education (non-formal ECE) is an education that is held for children under 4 years old. The implementation in District of Banyumas, Non-formal ECE is monitored by The District Government of Banyumas and helped by Sanggar Kegiatan Belajar (SKB) Purwokerto as one of the organizer of Non-formal Education. The government itself has a program for distributing ECE to all villages in Indonesia. However, The location to construct the ECE school in several years ahead is not arranged yet. Therefore, for supporting that program, a decision support system is made to give some recommendation villages for constructing The ECE building. The data are projected based on Brown’s Double Exponential Smoothing Method and utilizing Preference Ranking Organization Method for Enrichment Evaluation (Promethee) to generate priority order. As the recommendations system, it generates map visualization which is colored according to the priority level of sub-district and village area. The system was tested with black box testing, Promethee testing, and usability testing. The results showed that the system functionality and Promethee algorithm were working properly, and the user was satisfied.

Two-Step Formal Advertisement: An Examination.

DTIC Science & Technology

1976-10-01

The purpose of this report is to examine the potential application of the Two-Step Formal Advertisement method of procurement. Emphasis is placed on...Step formal advertising is a method of procurement designed to take advantage of negotiation flexibility and at the same time obtain the benefits of...formal advertising . It is used where the specifications are not sufficiently definite or may be too restrictive to permit full and free competition

NASA Education: Yesterday's Dream...Today's Vision...Tomorrow's Hope

NASA Technical Reports Server (NTRS)

Winterton, Joyce L.

2010-01-01

For 50 years, NASA's journeys into air and space have developed humankind's understanding of the universe, advanced technology breakthroughs, enhanced air travel safety and security, and expanded the frontiers of scientific research. These accomplishments share a common genesis: education. Education is a fundamental element of NASA's activities, reflecting a balanced and diverse portfolio of: Elementary and Secondary Education, Higher Education, e-Education, Informal Education, and Minority University Research and Education Programs (MUREP). Previous experience has shown that implementing exciting and compelling NASA missions are critical to inspiring the next generation of explorers, innovators, and leaders. Through partnerships with the Agency's Mission Directorates, other federal agencies, private industries, scientific research, and education/academic organizations, NASA's unique mission and education initiatives (content, people, and facilities) are helping to spark student interest and to guide them toward careers in science, technology, engineering, and mathematics (STEM). NASA continues to inspire the next generation of explorers, innovators, and future leaders through its educational investments, which are designed to: (1) Strengthen NASA and the Nation's future workforce -- NASA will identify and develop the critical skills and capabilities needed to ensure achievement of exploration, science, and aeronautics. (2) Attract and retain students in STEM disciplines through a progression of educational opportunities for students, teachers, and faculty -- To compete effectively for the minds, imaginations, and career ambitions of America's young people, NASA will focus on engaging and retaining students in STEM education programs to encourage their pursuit of educational disciplines critical to NASA's future engineering, scientific, and technical missions. 3. Engage Americans in NASA's mission -- NASA will build strategic partnerships and links between formal

Geometry and Formal Linguistics.

ERIC Educational Resources Information Center

Huff, George A.

This paper presents a method of encoding geometric line-drawings in a way which allows sets of such drawings to be interpreted as formal languages. A characterization of certain geometric predicates in terms of their properties as languages is obtained, and techniques usually associated with generative grammars and formal automata are then applied…

Methods for converging correlation energies within the dielectric matrix formalism

NASA Astrophysics Data System (ADS)

Dixit, Anant; Claudot, Julien; Gould, Tim; Lebègue, Sébastien; Rocca, Dario

2018-03-01

Within the dielectric matrix formalism, the random-phase approximation (RPA) and analogous methods that include exchange effects are promising approaches to overcome some of the limitations of traditional density functional theory approximations. The RPA-type methods however have a significantly higher computational cost, and, similarly to correlated quantum-chemical methods, are characterized by a slow basis set convergence. In this work we analyzed two different schemes to converge the correlation energy, one based on a more traditional complete basis set extrapolation and one that converges energy differences by accounting for the size-consistency property. These two approaches have been systematically tested on the A24 test set, for six points on the potential-energy surface of the methane-formaldehyde complex, and for reaction energies involving the breaking and formation of covalent bonds. While both methods converge to similar results at similar rates, the computation of size-consistent energy differences has the advantage of not relying on the choice of a specific extrapolation model.

NASA Astronauts on Soyuz: Experience and Lessons for the Future

NASA Technical Reports Server (NTRS)

2010-01-01

The U. S., Russia, and, China have each addressed the question of human-rating spacecraft. NASA's operational experience with human-rating primarily resides with Mercury, Gemini, Apollo, Space Shuttle, and International Space Station. NASA s latest developmental experience includes Constellation, X38, X33, and the Orbital Space Plane. If domestic commercial crew vehicles are used to transport astronauts to and from space, Soyuz is another example of methods that could be used to human-rate a spacecraft and to work with commercial spacecraft providers. For Soyuz, NASA's normal assurance practices were adapted. Building on NASA's Soyuz experience, this report contends all past, present, and future vehicles rely on a range of methods and techniques for human-rating assurance, the components of which include: requirements, conceptual development, prototype evaluations, configuration management, formal development reviews (safety, design, operations), component/system ground-testing, integrated flight tests, independent assessments, and launch readiness reviews. When constraints (cost, schedule, international) limit the depth/breadth of one or more preferred assurance means, ways are found to bolster the remaining areas. This report provides information exemplifying the above safety assurance model for consideration with commercial or foreign-government-designed spacecraft. Topics addressed include: U.S./Soviet-Russian government/agency agreements and engineering/safety assessments performed with lessons learned in historic U.S./Russian joint space ventures

LARCMACS: A TEX macro set for typesetting NASA reports

NASA Technical Reports Server (NTRS)

Woessner, Linda H.; Mccaskill, Mary K.

1988-01-01

This LARCMACS user's manual describes the February 1988 version of LARCMACS, the TEX macro set used by the Technical Editing Branch (TEB) at NASA Langley Research Center. These macros were developed by the authors to facilitate the typesetting of NASA formal reports. They are also useful, however, for informal NASA reports and other technical documents such as meeting papers. LARCMACS are distributed by TEB for the convenience of the Langley TEX user community. LARCMACS contain macros for obtaining the standard double-column format for NASA reports, for typesetting tables in the ruled format traditional in NASA reports, and for typesetting difficult mathematical expressions. Each macro is described and numerous examples are included. Definitions of the LARCMACS macros are also included.

Deep first formal concept search.

PubMed

Zhang, Tao; Li, Hui; Hong, Wenxue; Yuan, Xiamei; Wei, Xinyu

2014-01-01

The calculation of formal concepts is a very important part in the theory of formal concept analysis (FCA); however, within the framework of FCA, computing all formal concepts is the main challenge because of its exponential complexity and difficulty in visualizing the calculating process. With the basic idea of Depth First Search, this paper presents a visualization algorithm by the attribute topology of formal context. Limited by the constraints and calculation rules, all concepts are achieved by the visualization global formal concepts searching, based on the topology degenerated with the fixed start and end points, without repetition and omission. This method makes the calculation of formal concepts precise and easy to operate and reflects the integrity of the algorithm, which enables it to be suitable for visualization analysis.

Applications of Genetic Methods to NASA Design and Operations Problems

NASA Technical Reports Server (NTRS)

Laird, Philip D.

1996-01-01

We review four recent NASA-funded applications in which evolutionary/genetic methods are important. In the process we survey: the kinds of problems being solved today with these methods; techniques and tools used; problems encountered; and areas where research is needed. The presentation slides are annotated briefly at the top of each page.

Mathematical, Logical, and Formal Methods in Information Retrieval: An Introduction to the Special Issue.

ERIC Educational Resources Information Center

Crestani, Fabio; Dominich, Sandor; Lalmas, Mounia; van Rijsbergen, Cornelis Joost

2003-01-01

Discusses the importance of research on the use of mathematical, logical, and formal methods in information retrieval to help enhance retrieval effectiveness and clarify underlying concepts of information retrieval. Highlights include logic; probability; spaces; and future research needs. (Author/LRW)

A Study of Technical Engineering Peer Reviews at NASA

NASA Technical Reports Server (NTRS)

Chao, Lawrence P.; Tumer, Irem Y.; Bell, David G.

2003-01-01

This report describes the state of practices of design reviews at NASA and research into what can be done to improve peer review practices. There are many types of reviews at NASA: required and not, formalized and informal, programmatic and technical. Standing project formal reviews such as the Preliminary Design Review and Critical Design Review are a required part of every project and mission development. However, the technical, engineering peer reviews that support teams' work on such projects are informal, some times ad hoc, and inconsistent across the organization. The goal of this work is to identify best practices and lessons learned from NASA's experience, supported by academic research and methodologies to ultimately improve the process. This research has determined that the organization, composition, scope, and approach of the reviews impact their success. Failure Modes and Effects Analysis (FMEA) can identify key areas of concern before or in the reviews. Product definition tools like the Project Priority Matrix, engineering-focused Customer Value Chain Analysis (CVCA), and project or system-based Quality Function Deployment (QFD) help prioritize resources in reviews. The use of information technology and structured design methodologies can strengthen the engineering peer review process to help NASA work towards error-proofing the design process.

Discrete mathematics, formal methods, the Z schema and the software life cycle

NASA Technical Reports Server (NTRS)

Bown, Rodney L.

1991-01-01

The proper role and scope for the use of discrete mathematics and formal methods in support of engineering the security and integrity of components within deployed computer systems are discussed. It is proposed that the Z schema can be used as the specification language to capture the precise definition of system and component interfaces. This can be accomplished with an object oriented development paradigm.

Formal hardware verification of digital circuits

NASA Technical Reports Server (NTRS)

Joyce, J.; Seger, C.-J.

1991-01-01

The use of formal methods to verify the correctness of digital circuits is less constrained by the growing complexity of digital circuits than conventional methods based on exhaustive simulation. This paper briefly outlines three main approaches to formal hardware verification: symbolic simulation, state machine analysis, and theorem-proving.

NASA's Astronomy Education Program: Reaching Diverse Audiences

NASA Astrophysics Data System (ADS)

Hasan, Hashima; Smith, Denise Anne; Hertz, Paul; Meinke, Bonnie

2015-08-01

An overview will be given of the rich programs developed by NASA to inject the science from it's Astrophysics missions into STEM activities targeted to diverse audiences. For example, Astro4Girls was started as a pilot program during IYA2009. This program partners NASA astrophysics education programs with public libraries to provide NASA-themed hands-on education activities for girls and their families, and has been executed across the country. School curricula and NASA websites have been translated in Spanish; Braille books have been developed for the visually impaired; programs have been developed for the hearing impaired. Special effort has been made to reach underrepresented minorities. Audiences include students, teachers, and the general public through formal and informal education settings, social media and other outlets. NASA Astrophysics education providers include teams embedded in its space flight missions; professionals selected though peer reviewed programs; as well as the Science Mission Directorate Astrophysics Education forum. Representative examples will be presented to demonstrate the reach of NASA education programs, as well as an evaluation of the effectiveness of these programs.

NASA Nationwide and the Year of the Solar System (Invited)

NASA Astrophysics Data System (ADS)

Ferrari, K.

2010-12-01

NASA depends on the efforts of several volunteer networks to help implement its formal and informal education goals, to disseminate its key messages related to space and Earth science missions and to support broad public initiatives such as the upcoming Year of the Solar System (YSS), sponsored by the Planetary Science Education and Public Outreach Forum (SEPOF). These highly leveraged networks include programs such as Solar System Ambassadors, Solar System Educators, Night Sky Network, and NASA Explorer Schools. Founded in June 2008, NASA Nationwide: A Consortium of Formal and Informal Education Networks is a program that brings together these volunteer networks by creating an online community and shared resources which broadens the member networks’ base of support and provides opportunities to coordinate, cooperate, and collaborate with each other. Since its inception, NASA Nationwide has grown to include twelve NASA-funded volunteer networks as members and collaborates with three other NASA networks as affiliates. NASA Nationwide’s support for the Year of the Solar System includes management of several recently completed Solar System Nights kits, which will be made available regionally to collaborative teams of volunteers and affiliates for use in connecting with students in underserved, underrepresented and rural populations. In the latter part of 2010, the program will be further enhanced by the debut of the public NASA Nationwide website to showcase the successful efforts of these volunteers, provide information about member organizations and advertise their upcoming events in support of the Year of the Solar System. Through its broad reach and the dedicated enthusiasm of its members, NASA Nationwide will be an essential factor utilized to help achieve Year of the Solar System goals and ensure the ultimate success of the initiative.

Sub-grid scale models for discontinuous Galerkin methods based on the Mori-Zwanzig formalism

NASA Astrophysics Data System (ADS)

Parish, Eric; Duraisamy, Karthk

2017-11-01

The optimal prediction framework of Chorin et al., which is a reformulation of the Mori-Zwanzig (M-Z) formalism of non-equilibrium statistical mechanics, provides a framework for the development of mathematically-derived closure models. The M-Z formalism provides a methodology to reformulate a high-dimensional Markovian dynamical system as a lower-dimensional, non-Markovian (non-local) system. In this lower-dimensional system, the effects of the unresolved scales on the resolved scales are non-local and appear as a convolution integral. The non-Markovian system is an exact statement of the original dynamics and is used as a starting point for model development. In this work, we investigate the development of M-Z-based closures model within the context of the Variational Multiscale Method (VMS). The method relies on a decomposition of the solution space into two orthogonal subspaces. The impact of the unresolved subspace on the resolved subspace is shown to be non-local in time and is modeled through the M-Z-formalism. The models are applied to hierarchical discontinuous Galerkin discretizations. Commonalities between the M-Z closures and conventional flux schemes are explored. This work was supported in part by AFOSR under the project ''LES Modeling of Non-local effects using Statistical Coarse-graining'' with Dr. Jean-Luc Cambier as the technical monitor.

Formalization of the Access Control on ARM-Android Platform with the B Method

NASA Astrophysics Data System (ADS)

Ren, Lu; Wang, Wei; Zhu, Xiaodong; Man, Yujia; Yin, Qing

2018-01-01

ARM-Android is a widespread mobile platform with multi-layer access control mechanisms, security-critical in the system. Many access control vulnerabilities still exist due to the course-grained policy and numerous engineering defects, which have been widely studied. However, few researches focus on the mechanism formalization, including the Android permission framework, kernel process management and hardware isolation. This paper first develops a comprehensive formal access control model on the ARM-Android platform using the B method, from the Android middleware to hardware layer. All the model specifications are type checked and proved to be well-defined, with 75%of proof obligations demonstrated automatically. The results show that the proposed B model is feasible to specify and verify access control schemes in the ARM-Android system, and capable of implementing a practical control module.

Comparative Study of Impedance Eduction Methods, Part 2: NASA Tests and Methodology

NASA Technical Reports Server (NTRS)

Jones, Michael G.; Watson, Willie R.; Howerton, Brian M.; Busse-Gerstengarbe, Stefan

2013-01-01

A number of methods have been developed at NASA Langley Research Center for eduction of the acoustic impedance of sound-absorbing liners mounted in the wall of a flow duct. This investigation uses methods based on the Pridmore-Brown and convected Helmholtz equations to study the acoustic behavior of a single-layer, conventional liner fabricated by the German Aerospace Center and tested in the NASA Langley Grazing Flow Impedance Tube. Two key assumptions are explored in this portion of the investigation. First, a comparison of results achieved with uniform-flow and shear-flow impedance eduction methods is considered. Also, an approach based on the Prony method is used to extend these methods from single-mode to multi-mode implementations. Finally, a detailed investigation into the effects of harmonic distortion on the educed impedance is performed, and the results are used to develop guidelines regarding acceptable levels of harmonic distortion

Issues in NASA Program and Project Management. Special Edition: A Collection of Papers on NASA Procedures and Guidance 7120.5A. Volume 14

NASA Technical Reports Server (NTRS)

Hoffman, Edward J. (Editor); Lawbaugh, William M. (Editor)

1998-01-01

A key aspect of NASA's new Strategic Management System is improving the way we plan, approve, execute and evaluate our programs and projects. To this end, NASA has developed the NASA Program and Project Management processes and Requirements-NASA Procedures and Guidelines (NPG) 7120.5A, which formally documents the "Provide Aerospace Products and Capabilities" crosscutting process, and defines the processes and requirements that are responsive to the Program/Project Management-NPD 7120.4A. The Program/Project Management-NPD 7120.4A, issued November 14, 1996, provides the policy for managing programs and projects in a new way that is aligned with the new NASA environment. An Agencywide team has spent thousands of hours developing the NASA Program and Project Management Processes and Requirements-NPG 7120.5A. We have created significant flexibility, authority and discretion for the program and project managers to exercise and carry out their duties, and have delegated the responsibility and the accountability for their programs and projects.

Assessment of NASA Dual Microstructure Heat Treatment Method Utilizing Ladis SuperCooler(trademark) Cooling Technology

NASA Technical Reports Server (NTRS)

Lemsky, Joe; Gayda, John (Technical Monitor)

2005-01-01

The intent of this investigation was to demonstrate the NASA DMHT method with a tailored Ladish SuperCool(Trademark) cooling method on a Rolls-Royce AE2100, stage 3 disk shape. One disk each of two alloys, LSHR and ME3, were successfully converted as shown by macrostructure. DMHT heating time selection and cooling rate was aided by finite element modeling analysis. Residual stresses were also predicted and reported. Detailed microstructural analysis was performed by NASA and included in this report. Mechanical property characterization, also planned by NASA, is incomplete at this time and not part of this report.

An International Survey of Industrial Applications of Formal Methods. Volume 2. Case Studies

DTIC Science & Technology

1993-09-30

impact of the product on IBM revenues. 4. Error rates were claimed to be below industrial average and errors were minimal to fix. Formal methods, as...critical applications. These include: 3 I I International Survey of Industrial Applications 41 i) "Software failures, particularly under first use, seem...project to add improved modelling capability. I U International Survey of Industrial Applications 93 I Design and Implementation These products are being

Improving software quality - The use of formal inspections at the Jet Propulsion Laboratory

NASA Technical Reports Server (NTRS)

Bush, Marilyn

1990-01-01

The introduction of software formal inspections (Fagan Inspections) at JPL for finding and fixing defects early in the software development life cycle are reviewed. It is estimated that, by the year 2000, some software efforts will rise to as much as 80 percent of the total. Software problems are especially important at NASA as critical flight software must be error-free. It is shown that formal inspections are particularly effective at finding and removing defects having to do with clarity, correctness, consistency, and completeness. A very significant discovery was that code audits were not as effective at finding defects as code inspections.

Monte-Carlo methods make Dempster-Shafer formalism feasible

NASA Technical Reports Server (NTRS)

Kreinovich, Vladik YA.; Bernat, Andrew; Borrett, Walter; Mariscal, Yvonne; Villa, Elsa

1991-01-01

One of the main obstacles to the applications of Dempster-Shafer formalism is its computational complexity. If we combine m different pieces of knowledge, then in general case we have to perform up to 2(sup m) computational steps, which for large m is infeasible. For several important cases algorithms with smaller running time were proposed. We prove, however, that if we want to compute the belief bel(Q) in any given query Q, then exponential time is inevitable. It is still inevitable, if we want to compute bel(Q) with given precision epsilon. This restriction corresponds to the natural idea that since initial masses are known only approximately, there is no sense in trying to compute bel(Q) precisely. A further idea is that there is always some doubt in the whole knowledge, so there is always a probability p(sub o) that the expert's knowledge is wrong. In view of that it is sufficient to have an algorithm that gives a correct answer a probability greater than 1-p(sub o). If we use the original Dempster's combination rule, this possibility diminishes the running time, but still leaves the problem infeasible in the general case. We show that for the alternative combination rules proposed by Smets and Yager feasible methods exist. We also show how these methods can be parallelized, and what parallelization model fits this problem best.

Model based verification of the Secure Socket Layer (SSL) Protocol for NASA systems

NASA Technical Reports Server (NTRS)

Powell, John D.; Gilliam, David

2004-01-01

The National Aeronautics and Space Administration (NASA) has tens of thousands of networked computer systems and applications. Software Security vulnerabilities present risks such as lost or corrupted data, information theft, and unavailability of critical systems. These risks represent potentially enormous costs to NASA. The NASA Code Q research initiative 'Reducing Software Security Risk (RSSR) Trough an Integrated Approach' offers formal verification of information technology (IT), through the creation of a Software Security Assessment Instrument (SSAI), to address software security risks.

Example of Occupational Surveillance in a Telemedicine Setting: Application of Epidemiologic Methods at NASA Johnson Space Center

NASA Technical Reports Server (NTRS)

Babiak-Vazquez, Adriana; Ruffaner, Lanie M.; Wear, Mary L.; Crucian, Brian; Sams, Clarence; Lee, Lesley R.; Van Baalen, Mary

2016-01-01

In 2010, NASA implemented Lifetime Surveillance of Astronaut Health, a formal occupational surveillance program for the U.S. astronaut corps. Because of the nature of the space environment, space medicine presents unique challenges and opportunities for epidemiologists. One such example is the use of telemedicine while crewmembers are in flight, where the primary source of information about crew health is verbal communication between physicians and their crewmembers. Due to restricted medical capabilities, the available health information is primarily crewmember report of signs and symptoms, rather than diagnoses. As epidemiologists at NASA, Johnson Space Center, we have shifted our paradigm from tracking diagnoses based on traditional terrestrial clinical practice to one in which we also incorporate reported symptomology as potential antecedents of disease. In this presentation we describe how characterization of reported signs and symptoms can be used to establish incidence rates for inflight immunologic events. We describe interdisciplinary data sources of information that are used in combination with medical information to analyze the data. We also delineate criteria for symptom classification inclusion. Finally, we present incidence tables and graphs to illustrate the final outcomes. Using signs and symptoms reported via telemedicine, the epidemiologists provide summary evidence regarding incidence of potential inflight medical conditions. These results inform our NASA physicians and scientists, and support evaluation of the occupational health risks associated with spaceflight.

A Formal Approach to Requirements-Based Programming

NASA Technical Reports Server (NTRS)

Hinchey, Michael G.; Rash, James L.; Rouff, Christopher A.

2005-01-01

No significant general-purpose method is currently available to mechanically transform system requirements into a provably equivalent model. The widespread use of such a method represents a necessary step toward high-dependability system engineering for numerous application domains. Current tools and methods that start with a formal model of a system and mechanically produce a provably equivalent implementation are valuable but not sufficient. The "gap" unfilled by such tools and methods is that the formal models cannot be proven to be equivalent to the requirements. We offer a method for mechanically transforming requirements into a provably equivalent formal model that can be used as the basis for code generation and other transformations. This method is unique in offering full mathematical tractability while using notations and techniques that are well known and well trusted. Finally, we describe further application areas we are investigating for use of the approach.

Surveillance in a Telemedicine Setting: Application of Epidemiologic Methods at NASA Johnson Space Center Adriana

NASA Technical Reports Server (NTRS)

Babiak-Vazquez, Adriana; Ruffaner, Lanie; Wear, Mary; Crucian Brian; Sams, Clarence; Lee, Lesley R.; Van Baalen, Mary

2016-01-01

Space medicine presents unique challenges and opportunities for epidemiologists, such as the use of telemedicine during spaceflight. Medical capabilities aboard the International Space Station (ISS) are limited due to severe restrictions on power, volume, and mass. Consequently, inflight health information is based heavily on crewmember (CM) self-report of signs and symptoms, rather than formal diagnoses. While CM's are in flight, the primary source of crew health information is verbal communication between physicians and crewmembers. In 2010 NASA implemented the Lifetime Surveillance of Astronaut Health, an occupational surveillance program for the U.S. Astronaut corps. This has shifted the epidemiological paradigm from tracking diagnoses based on traditional terrestrial clinical practice to one that incorporates symptomatology and may gain a more population-based understanding of early detection of disease process.

A STUDY OF FORMALLY ADVERTISED PROCUREMENT

DTIC Science & Technology

As a method of procuring goods and services, formally advertised procurement offers a number of advantages. These include the prevention of fraud and...two-thirds of all contracts are let in these cases. This is done by examining over 2,300 contracts let under formal advertising procedures. A measure of

IDEF3 Formalization Report

DTIC Science & Technology

1991-10-01

SUBJECT TERMS 15. NUMBER OF PAGES engineering management information systems method formalization 60 information engineering process modeling 16 PRICE...CODE information systems requirements definition methods knowlede acquisition methods systems engineering 17. SECURITY CLASSIFICATION ji. SECURITY... Management , Inc., Santa Monica, California. CORYNEN, G. C., 1975, A Mathematical Theory of Modeling and Simula- tion. Ph.D. Dissertation, Department

NASA evolution of exploration architectures

NASA Technical Reports Server (NTRS)

Roberts, Barney B.

1991-01-01

A series of charts and diagrams is used to provide a detailed overview of the evolution of NASA space exploration architectures. The pre-Apollo programs including the Werner von Braun feasibility study are discussed and the evolution of the Apollo program itself is treated in detail. The post-Apollo era is reviewed and attention is given to the resurgence of strategic planning exemplified by both ad hoc and formal efforts at planning. Results of NASA's study of the main elements of the Space Exploration Initiative which examined technical scenarios, science opportunities, required technologies, international considerations, institutional strengths and needs, and resource estimates are presented. The 90-day study concludes that, among other things, major investments in challenging technologies are required, the scientific opportunities provided by the program are considerable, current launch capabilities are inadequate, and Space Station Freedom is essential.

NASA Team Collaboration Pilot: Enabling NASA's Virtual Teams

NASA Technical Reports Server (NTRS)

Prahst, Steve

2003-01-01

Most NASA projects and work activities are accomplished by teams of people. These teams are often geographically distributed - across NASA centers and NASA external partners, both domestic and international. NASA "virtual" teams are stressed by the challenge of getting team work done - across geographic boundaries and time zones. To get distributed work done, teams rely on established methods - travel, telephones, Video Teleconferencing (NASA VITS), and email. Time is our most critical resource - and team members are hindered by the overhead of travel and the difficulties of coordinating work across their virtual teams. Modern, Internet based team collaboration tools offer the potential to dramatically improve the ability of virtual teams to get distributed work done.

Unpacking (In)formal Learning in an Academic Development Programme: A Mixed-Method Social Network Perspective

ERIC Educational Resources Information Center

Rienties, Bart; Hosein, Anesa

2015-01-01

How and with whom academics develop and maintain formal and informal networks for reflecting on their teaching practice has received limited attention even though academic development (AD) programmes have become an almost ubiquitous feature of higher education. The primary goal of this mixed-method study is to unpack how 114 academics in an AD…

Experiences with a Requirements-Based Programming Approach to the Development of a NASA Autonomous Ground Control System

NASA Technical Reports Server (NTRS)

Hinchey, Michael G.; Rash, James L.; Rouff, Christopher A.; Gracanin, Denis; Erickson, John

2005-01-01

Requirements-to-Design-to-Code (R2D2C) is an approach to the engineering of computer-based systems that embodies the idea of requirements-based programming in system development. It goes further; however, in that the approach offers not only an underlying formalism, but full formal development from requirements capture through to the automatic generation of provably-correct code. As such, the approach has direct application to the development of systems requiring autonomic properties. We describe a prototype tool to support the method, and illustrate its applicability to the development of LOGOS, a NASA autonomous ground control system, which exhibits autonomic behavior. Finally, we briefly discuss other areas where the approach and prototype tool are being considered for application.

NASA Standard for Models and Simulations: Credibility Assessment Scale

NASA Technical Reports Server (NTRS)

Babula, Maria; Bertch, William J.; Green, Lawrence L.; Hale, Joseph P.; Moser, Gary E.; Steele, Martin J.; Sylvester, Andre; Woods, Jody

2008-01-01

As one of its many responses to the 2003 Space Shuttle Columbia accident, NASA decided to develop a formal standard for models and simulations (M and S)ii. Work commenced in May 2005. An interim version was issued in late 2006. This interim version underwent considerable revision following an extensive Agency-wide review in 2007 along with some additional revisions as a result of the review by the NASA Engineering Management Board (EMB) in the first half of 2008. Issuance of the revised, permanent version,hereafter referred to as the M and S Standard or just the Standard, occurred in July 2008.

Literate Specification: Using Design Rationale To Support Formal Methods in the Development of Human-Machine Interfaces.

ERIC Educational Resources Information Center

Johnson, Christopher W.

1996-01-01

The development of safety-critical systems (aircraft cockpits and reactor control rooms) is qualitatively different from that of other interactive systems. These differences impose burdens on design teams that must ensure the development of human-machine interfaces. Analyzes strengths and weaknesses of formal methods for the design of user…

The Hierarchical Structure of Formal Operational Tasks.

ERIC Educational Resources Information Center

Bart, William M.; Mertens, Donna M.

1979-01-01

The hierarchical structure of the formal operational period of Piaget's theory of cognitive development was explored through the application of ordering theoretical methods to a set of data that systematically utilized the various formal operational schemes. Results suggested a common structure underlying task performance. (Author/BH)

Mapping of Primary Instructional Methods and Teaching Techniques for Regularly Scheduled, Formal Teaching Sessions in an Anesthesia Residency Program.

PubMed

Vested Madsen, Matias; Macario, Alex; Yamamoto, Satoshi; Tanaka, Pedro

2016-06-01

In this study, we examined the regularly scheduled, formal teaching sessions in a single anesthesiology residency program to (1) map the most common primary instructional methods, (2) map the use of 10 known teaching techniques, and (3) assess if residents scored sessions that incorporated active learning as higher quality than sessions with little or no verbal interaction between teacher and learner. A modified Delphi process was used to identify useful teaching techniques. A representative sample of each of the formal teaching session types was mapped, and residents anonymously completed a 5-question written survey rating the session. The most common primary instructional methods were computer slides-based classroom lectures (66%), workshops (15%), simulations (5%), and journal club (5%). The number of teaching techniques used per formal teaching session averaged 5.31 (SD, 1.92; median, 5; range, 0-9). Clinical applicability (85%) and attention grabbers (85%) were the 2 most common teaching techniques. Thirty-eight percent of the sessions defined learning objectives, and one-third of sessions engaged in active learning. The overall survey response rate equaled 42%, and passive sessions had a mean score of 8.44 (range, 5-10; median, 9; SD, 1.2) compared with a mean score of 8.63 (range, 5-10; median, 9; SD, 1.1) for active sessions (P = 0.63). Slides-based classroom lectures were the most common instructional method, and faculty used an average of 5 known teaching techniques per formal teaching session. The overall education scores of the sessions as rated by the residents were high.

Simplification of the time-dependent generalized self-interaction correction method using two sets of orbitals: Application of the optimized effective potential formalism

DOE Office of Scientific and Technical Information (OSTI.GOV)

Messud, J.; Dinh, P. M.; Suraud, Eric

2009-10-15

We propose a simplification of the time-dependent self-interaction correction (TD-SIC) method using two sets of orbitals, applying the optimized effective potential (OEP) method. The resulting scheme is called time-dependent 'generalized SIC-OEP'. A straightforward approximation, using the spatial localization of one set of orbitals, leads to the 'generalized SIC-Slater' formalism. We show that it represents a great improvement compared to the traditional SIC-Slater and Krieger-Li-Iafrate formalisms.

Proceedings 3rd NASA/IEEE Workshop on Formal Approaches to Agent-Based Systems (FAABS-III)

NASA Technical Reports Server (NTRS)

Hinchey, Michael (Editor); Rash, James (Editor); Truszkowski, Walt (Editor); Rouff, Christopher (Editor)

2004-01-01

These preceedings contain 18 papers and 4 poster presentation, covering topics such as: multi-agent systems, agent-based control, formalism, norms, as well as physical and biological models of agent-based systems. Some applications presented in the proceedings include systems analysis, software engineering, computer networks and robot control.

Developing Formal Correctness Properties from Natural Language Requirements

NASA Technical Reports Server (NTRS)

Nikora, Allen P.

2006-01-01

This viewgraph presentation reviews the rationale of the program to transform natural language specifications into formal notation.Specifically, automate generation of Linear Temporal Logic (LTL)correctness properties from natural language temporal specifications. There are several reasons for this approach (1) Model-based techniques becoming more widely accepted, (2) Analytical verification techniques (e.g., model checking, theorem proving) significantly more effective at detecting types of specification design errors (e.g., race conditions, deadlock) than manual inspection, (3) Many requirements still written in natural language, which results in a high learning curve for specification languages, associated tools and increased schedule and budget pressure on projects reduce training opportunities for engineers, and (4) Formulation of correctness properties for system models can be a difficult problem. This has relevance to NASA in that it would simplify development of formal correctness properties, lead to more widespread use of model-based specification, design techniques, assist in earlier identification of defects and reduce residual defect content for space mission software systems. The presentation also discusses: potential applications, accomplishments and/or technological transfer potential and the next steps.

Simplification of the time-dependent generalized self-interaction correction method using two sets of orbitals: Application of the optimized effective potential formalism

NASA Astrophysics Data System (ADS)

Messud, J.; Dinh, P. M.; Reinhard, P.-G.; Suraud, Eric

2009-10-01

We propose a simplification of the time-dependent self-interaction correction (TD-SIC) method using two sets of orbitals, applying the optimized effective potential (OEP) method. The resulting scheme is called time-dependent “generalized SIC-OEP.” A straightforward approximation, using the spatial localization of one set of orbitals, leads to the “generalized SIC-Slater” formalism. We show that it represents a great improvement compared to the traditional SIC-Slater and Krieger-Li-Iafrate formalisms.

a Norm Pairing in Formal Modules

NASA Astrophysics Data System (ADS)

Vostokov, S. V.

1980-02-01

A pairing of the multiplicative group of a local field (a finite extension of the field of p-adic numbers Qp) with the group of points of a Lubin-Tate formal group is defined explicitly. The values of the pairing are roots of an isogeny of the formal group. The main properties of this pairing are established: bilinearity, invariance under the choice of a local uniformizing element, and independence of the method of expanding elements into series with respect to this uniformizing element. These properties of the pairing are used to prove that it agrees with the generalized Hilbert norm residue symbol when the field over whose ring of integers the formal group is defined is totally ramified over Qp. This yields an explicit expression for the generalized Hilbert symbol on the group of points of the formal group. Bibliography: 12 titles.

Towards Formal Implementation of PUS Standard

NASA Astrophysics Data System (ADS)

Ilić, D.

2009-05-01

As an effort to promote the reuse of on-board and ground systems ESA developed a standard for packet telemetry and telecommand - PUS. It defines a set of standard service models with the corresponding structures of the associated telemetry and telecommand packets. Various missions then can choose to implement those standard PUS services that best conform to their specific requirements. In this paper we propose a formal development (based on the Event-B method) of reusable service patterns, which can be instantiated for concrete application. Our formal models allow us to formally express and verify specific service properties including various telecommand and telemetry packet structure validation.

NASA Hydrogen Research for Spaceport and Space Based Applications

NASA Technical Reports Server (NTRS)

Anderson, Tim

2005-01-01

Project management activities for this grant includes internal oversight, coordination and facilitation among research groups (internal to UF and external); system and/or trade studies to assist in evaluating and prioritizing new hydrogen production processes that may become available for potential research investigations; a technical and programmatic outreach activity; and formal reporting, including periodic technical reviews with the NASA team.

Capacity Building for the Access and Application of NASA Earth Science Data

NASA Astrophysics Data System (ADS)

Blevins, B.; Prados, A. I.; Hook, E.

2016-12-01

Since 2008, NASA's Applied Remote Sensing Training (ARSET) program has built capacity in applied remote sensing by building awareness, and enabling access and use of NASA Earth science data. To reach decision and policy makers from all sectors, ARSET hosts hands-on workshops and online webinars. With over 70 trainings, reaching more than 6,000 people from 130 countries and 1,600 organizations, ARSET has ample experience with assessing and meeting end-user needs. To meet the spectrum of needs and levels of attendee expertise, ARSET holds trainings for both the novice and experienced end-user. Trainings employ exercises, assignments, and live demonstrations of data access tools to reinforce remote sensing concepts and to facilitate data use and analysis techniques. This program is in a unique position to collect important feedback from thousands of participants each year through formal surveys and informal methods on NASA tools, portals, data formats, and the applications of Earth science data for end-user decision making activities. This information is shared with NASA data centers and program managers to help inform data portal development and to help prioritize the production of new satellite derived data products. This presentation will discuss the challenges that arise in capacity building trainings, the integration of community feedback into the training development cycle, and lessons learned throughout the process.

Formal functional test designs with a test representation language

NASA Technical Reports Server (NTRS)

Hops, J. M.

1993-01-01

The application of the category-partition method to the test design phase of hardware, software, or system test development is discussed. The method provides a formal framework for reducing the total number of possible test cases to a minimum logical subset for effective testing. An automatic tool and a formal language were developed to implement the method and produce the specification of test cases.

A modified F/A-18 in a distinctive red, white and blue paint scheme was showcased during formal roll

NASA Technical Reports Server (NTRS)

2002-01-01

A modified F/A-18 in a distinctive red, white and blue paint scheme was showcased during formal rollout ceremonies for the Active Aeroelastic Wing flight research program at NASA's Dryden Flight Research Center on March 27, 2002.

Indexing NASA programs for technology transfer methods development and feasibility

NASA Technical Reports Server (NTRS)

Clingman, W. H.

1972-01-01

This project was undertaken to evaluate the application of a previously developed indexing methodology to ongoing NASA programs. These programs are comprehended by the NASA Program Approval Documents (PADS). Each PAD contains a technical plan for the area it covers. It was proposed that these could be used to generate an index to the complete NASA program. To test this hypothesis two PADS were selected by the NASA Technology Utilization Office for trial indexing. Twenty-five individuals indexed the two PADS using NASA Thesaurus terms. The results demonstrated the feasibility of indexing ongoing NASA programs using PADS as the source of information. The same indexing methodology could be applied to other documents containing a brief description of the technical plan. Results of this project showed that over 85% of the concepts in the technology should be covered by the indexing. Also over 85% of the descriptors chosen would be accurate. This completeness and accuracy for the indexing is considered satisfactory for application in technology transfer.

Formal verification of mathematical software

NASA Technical Reports Server (NTRS)

Sutherland, D.

1984-01-01

Methods are investigated for formally specifying and verifying the correctness of mathematical software (software which uses floating point numbers and arithmetic). Previous work in the field was reviewed. A new model of floating point arithmetic called the asymptotic paradigm was developed and formalized. Two different conceptual approaches to program verification, the classical Verification Condition approach and the more recently developed Programming Logic approach, were adapted to use the asymptotic paradigm. These approaches were then used to verify several programs; the programs chosen were simplified versions of actual mathematical software.

Best Practices in NASA's Astrophysics Education and Public Outreach Projects

NASA Astrophysics Data System (ADS)

Hasan, H.; Smith, D.

2015-11-01

NASA's Astrophysics Education and Public Outreach (EPO) program has partnered scientists and educators since its inception almost twenty years ago, leading to authentic STEM experiences and products widely used by the education and outreach community. We present examples of best practices and representative projects. Keys to success include effective use of unique mission science/technology, attention to audience needs, coordination of effort, robust partnerships and publicly accessible repositories of EPO products. Projects are broadly targeted towards audiences in formal education, informal education, and community engagement. All NASA programs are evaluated for quality and impact. New technology is incorporated to engage young students being raised in the digital age. All projects focus on conveying the excitement of scientific discoveries from NASA's Astrophysics missions, advancing scientific literacy, and engaging students in science and technology careers.

Using formal methods to scope performance challenges for Smart Manufacturing Systems: focus on agility.

PubMed

Jung, Kiwook; Morris, K C; Lyons, Kevin W; Leong, Swee; Cho, Hyunbo

2015-12-01

Smart Manufacturing Systems (SMS) need to be agile to adapt to new situations by using detailed, precise, and appropriate data for intelligent decision-making. The intricacy of the relationship of strategic goals to operational performance across the many levels of a manufacturing system inhibits the realization of SMS. This paper proposes a method for identifying what aspects of a manufacturing system should be addressed to respond to changing strategic goals. The method uses standard modeling techniques in specifying a manufacturing system and the relationship between strategic goals and operational performance metrics. Two existing reference models related to manufacturing operations are represented formally and harmonized to support the proposed method. The method is illustrated for a single scenario using agility as a strategic goal. By replicating the proposed method for other strategic goals and with multiple scenarios, a comprehensive set of performance challenges can be identified.

Using formal methods to scope performance challenges for Smart Manufacturing Systems: focus on agility

PubMed Central

Jung, Kiwook; Morris, KC; Lyons, Kevin W.; Leong, Swee; Cho, Hyunbo

2016-01-01

Smart Manufacturing Systems (SMS) need to be agile to adapt to new situations by using detailed, precise, and appropriate data for intelligent decision-making. The intricacy of the relationship of strategic goals to operational performance across the many levels of a manufacturing system inhibits the realization of SMS. This paper proposes a method for identifying what aspects of a manufacturing system should be addressed to respond to changing strategic goals. The method uses standard modeling techniques in specifying a manufacturing system and the relationship between strategic goals and operational performance metrics. Two existing reference models related to manufacturing operations are represented formally and harmonized to support the proposed method. The method is illustrated for a single scenario using agility as a strategic goal. By replicating the proposed method for other strategic goals and with multiple scenarios, a comprehensive set of performance challenges can be identified. PMID:27141209

Changes in formal sex education: 1995-2002.

PubMed

Lindberg, Laura Duberstein; Santelli, John S; Singh, Susheela

2006-12-01

Although comprehensive sex education is broadly supported by health professionals, funding for abstinence-only education has increased. Using data from the 1995 National Survey of Adolescent Males, the 1995 National Survey of Family Growth (NSFG) and the 2002 NSFG, changes in male and female adolescents' reports of the sex education they have received from formal sources were examined. Life-table methods were used to measure the timing of instruction, and t tests were used for changes over time. From 1995 to 2002, reports of formal instruction about birth control methods declined among both genders (males, from 81% to 66%; females, from 87% to 70%). This, combined with increases in reports of abstinence education among males (from 74% to 83%), resulted in a lower proportion of teenagers' overall receiving formal instruction about both abstinence and birth control methods (males, 65% to 59%; females, 84% to 65%), and a higher proportion of teenagers' receiving instruction only about abstinence (males, 9% to 24%; females, 8% to 21%). Teenagers in 2002 had received abstinence education about two years earlier (median age, 11.4 for males, 11.8 for females) than they had received birth control instruction (median age, 13.5 for both males and females). Among sexually experienced adolescents, 62% of females and 54% of males had received instruction about birth control methods prior to first sex. A substantial retreat from formal instruction about birth control methods has left increasing proportions of adolescents receiving only abstinence education. Efforts are needed to expand teenagers' access to medically accurate and comprehensive reproductive health information.

De novo reconstruction of gene regulatory networks from time series data, an approach based on formal methods.

PubMed

Ceccarelli, Michele; Cerulo, Luigi; Santone, Antonella

2014-10-01

Reverse engineering of gene regulatory relationships from genomics data is a crucial task to dissect the complex underlying regulatory mechanism occurring in a cell. From a computational point of view the reconstruction of gene regulatory networks is an undetermined problem as the large number of possible solutions is typically high in contrast to the number of available independent data points. Many possible solutions can fit the available data, explaining the data equally well, but only one of them can be the biologically true solution. Several strategies have been proposed in literature to reduce the search space and/or extend the amount of independent information. In this paper we propose a novel algorithm based on formal methods, mathematically rigorous techniques widely adopted in engineering to specify and verify complex software and hardware systems. Starting with a formal specification of gene regulatory hypotheses we are able to mathematically prove whether a time course experiment belongs or not to the formal specification, determining in fact whether a gene regulation exists or not. The method is able to detect both direction and sign (inhibition/activation) of regulations whereas most of literature methods are limited to undirected and/or unsigned relationships. We empirically evaluated the approach on experimental and synthetic datasets in terms of precision and recall. In most cases we observed high levels of accuracy outperforming the current state of art, despite the computational cost increases exponentially with the size of the network. We made available the tool implementing the algorithm at the following url: http://www.bioinformatics.unisannio.it. Copyright © 2014 Elsevier Inc. All rights reserved.

An overview of the USL/DBMS NASA/PC R and D project working paper series

NASA Technical Reports Server (NTRS)

Dominick, Wayne D. (Editor)

1984-01-01

An introduction is given to the University of Southwestern Louisiana Data Base Management System (USL/DBMS) NASA/PC R and D Working Paper Series which has been established to provide a foundation for both a formal and informal information dissemination mechanism concerning PC-based research and development activities being performed pursuant to the NASA contract. This entry also serves as an index to the collection of Working Paper Series reports.

State Event Models for the Formal Analysis of Human-Machine Interactions

NASA Technical Reports Server (NTRS)

Combefis, Sebastien; Giannakopoulou, Dimitra; Pecheur, Charles

2014-01-01

The work described in this paper was motivated by our experience with applying a framework for formal analysis of human-machine interactions (HMI) to a realistic model of an autopilot. The framework is built around a formally defined conformance relation called "fullcontrol" between an actual system and the mental model according to which the system is operated. Systems are well-designed if they can be described by relatively simple, full-control, mental models for their human operators. For this reason, our framework supports automated generation of minimal full-control mental models for HMI systems, where both the system and the mental models are described as labelled transition systems (LTS). The autopilot that we analysed has been developed in the NASA Ames HMI prototyping tool ADEPT. In this paper, we describe how we extended the models that our HMI analysis framework handles to allow adequate representation of ADEPT models. We then provide a property-preserving reduction from these extended models to LTSs, to enable application of our LTS-based formal analysis algorithms. Finally, we briefly discuss the analyses we were able to perform on the autopilot model with our extended framework.

Matching biomedical ontologies based on formal concept analysis.

PubMed

Zhao, Mengyi; Zhang, Songmao; Li, Weizhuo; Chen, Guowei

2018-03-19

The goal of ontology matching is to identify correspondences between entities from different yet overlapping ontologies so as to facilitate semantic integration, reuse and interoperability. As a well developed mathematical model for analyzing individuals and structuring concepts, Formal Concept Analysis (FCA) has been applied to ontology matching (OM) tasks since the beginning of OM research, whereas ontological knowledge exploited in FCA-based methods is limited. This motivates the study in this paper, i.e., to empower FCA with as much as ontological knowledge as possible for identifying mappings across ontologies. We propose a method based on Formal Concept Analysis to identify and validate mappings across ontologies, including one-to-one mappings, complex mappings and correspondences between object properties. Our method, called FCA-Map, incrementally generates a total of five types of formal contexts and extracts mappings from the lattices derived. First, the token-based formal context describes how class names, labels and synonyms share lexical tokens, leading to lexical mappings (anchors) across ontologies. Second, the relation-based formal context describes how classes are in taxonomic, partonomic and disjoint relationships with the anchors, leading to positive and negative structural evidence for validating the lexical matching. Third, the positive relation-based context can be used to discover structural mappings. Afterwards, the property-based formal context describes how object properties are used in axioms to connect anchor classes across ontologies, leading to property mappings. Last, the restriction-based formal context describes co-occurrence of classes across ontologies in anonymous ancestors of anchors, from which extended structural mappings and complex mappings can be identified. Evaluation on the Anatomy, the Large Biomedical Ontologies, and the Disease and Phenotype track of the 2016 Ontology Alignment Evaluation Initiative campaign

Automatically Grading Customer Confidence in a Formal Specification.

ERIC Educational Resources Information Center

Shukur, Zarina; Burke, Edmund; Foxley, Eric

1999-01-01

Describes an automatic grading system for a formal methods computer science course that is able to evaluate a formal specification written in the Z language. Quality is measured by considering first, specification correctness (syntax, semantics, and satisfaction of customer requirements), and second, specification maintainability (comparison of…

Using SCR methods to analyze requirements documentation

NASA Technical Reports Server (NTRS)

Callahan, John; Morrison, Jeffery

1995-01-01

Software Cost Reduction (SCR) methods are being utilized to analyze and verify selected parts of NASA's EOS-DIS Core System (ECS) requirements documentation. SCR is being used as a spot-inspection tool. Through this formal and systematic approach of the SCR requirements methods, insights as to whether the requirements are internally inconsistent or incomplete as the scenarios of intended usage evolve in the OC (Operations Concept) documentation. Thus, by modelling the scenarios and requirements as mode charts using the SCR methods, we have been able to identify problems within and between the documents.

A comparison between state-specific and linear-response formalisms for the calculation of vertical electronic transition energy in solution with the CCSD-PCM method.

PubMed

Caricato, Marco

2013-07-28

The calculation of vertical electronic transition energies of molecular systems in solution with accurate quantum mechanical methods requires the use of approximate and yet reliable models to describe the effect of the solvent on the electronic structure of the solute. The polarizable continuum model (PCM) of solvation represents a computationally efficient way to describe this effect, especially when combined with coupled cluster (CC) methods. Two formalisms are available to compute transition energies within the PCM framework: State-Specific (SS) and Linear-Response (LR). The former provides a more complete account of the solute-solvent polarization in the excited states, while the latter is computationally very efficient (i.e., comparable to gas phase) and transition properties are well defined. In this work, I review the theory for the two formalisms within CC theory with a focus on their computational requirements, and present the first implementation of the LR-PCM formalism with the coupled cluster singles and doubles method (CCSD). Transition energies computed with LR- and SS-CCSD-PCM are presented, as well as a comparison between solvation models in the LR approach. The numerical results show that the two formalisms provide different absolute values of transition energy, but similar relative solvatochromic shifts (from nonpolar to polar solvents). The LR formalism may then be used to explore the solvent effect on multiple states and evaluate transition probabilities, while the SS formalism may be used to refine the description of specific states and for the exploration of excited state potential energy surfaces of solvated systems.

Education and outreach bring NASA heliophysics to the public

NASA Astrophysics Data System (ADS)

Barbier, Beth

2011-11-01

Educating and inspiring students, teachers, and the public by communicating advances in heliophysics science is the objective of the education and public outreach (E/PO) specialists at the Heliophysics Science Division (HSD) at NASA Goddard Space Flight Center (GSFC) in Greenbelt, Md. The specialists carry out NASA's E/PO goal to enhance the nation's formal education system and contribute to the broad public understanding of science, math, and technology. HSD E/PO projects exploit community best practices to meet or surpass NASA's requirements, which include attention to quality; leverage through internal and external partnerships; and a focus on customer needs, project sustainability, and audience diversity. One key to the group's success is the involvement of enthusiastic HSD research scientists who directly interface with E/PO specialists and various audiences, verify scientific content, and/or provide data access or other resources. Scientists also mentor interns from high school to graduate school through NASA and GSFC programs, and several have shared their science with the public via appearances on national media, including the National Geographic and History channels as well as local news.

Accessing NASA Technology with the World Wide Web

NASA Technical Reports Server (NTRS)

Nelson, Michael L.; Bianco, David J.

1995-01-01

NASA Langley Research Center (LaRC) began using the World Wide Web (WWW) in the summer of 1993, becoming the first NASA installation to provide a Center-wide home page. This coincided with a reorganization of LaRC to provide a more concentrated focus on technology transfer to both aerospace and non-aerospace industry. Use of WWW and NCSA Mosaic not only provides automated information dissemination, but also allows for the implementation, evolution and integration of many technology transfer and technology awareness applications. This paper describes several of these innovative applications, including the on-line presentation of the entire Technology OPportunities Showcase (TOPS), an industrial partnering showcase that exists on the Web long after the actual 3-day event ended. The NASA Technical Report Server (NTRS) provides uniform access to many logically similar, yet physically distributed NASA report servers. WWW is also the foundation of the Langley Software Server (LSS), an experimental software distribution system which will distribute LaRC-developed software. In addition to the more formal technology distribution projects, WWW has been successful in connecting people with technologies and people with other people.

The NASA 2017 Eclipse Education Program: Through the Eyes of NASA to the Hearts of a Nation

NASA Astrophysics Data System (ADS)

Young, C. Alex; Mayo, Louis; Ng, Carolyn; Cline, Troy D.; Lewis, Elaine; Stephenson, Bryan; Odenwald, Sten; Hill, Steele; Bleacher, Lora; Kirk, Michael S.; jones, andrea

2016-05-01

The August 21, 2017, eclipse across America will be seen by an estimated 500 million people from northern Canada to South America as well as parts of western Europe and Africa. Through This "Great American Eclipse" NASA in partnership with Google, the American Parks Network, American Astronomical Society, the Astronomical League, and numerous other science, education, outreach, and public communications groups and organizations will develop the approaches, resources, partnerships, and technology applications necessary to bring the excitement and the science of the August 21st, 2017 total solar eclipse across America to formal and informal audiences in the US and around the world. This effort will be supported by the highly visible and successful Sun Earth Days program and will be the main theme for Sun-Earth Days 2017.This presentation will discuss NASA's education and communication plans for the eclipse and will detail a number of specific programs and partnerships from across the country being leveraged to enhance our reach and impact. We also discuss the observations and science of current and future NASA missions such as SDO, Hinode and Solar Probe Plus along with their relationship to such a unique celestial event as a total solar eclipse.

Five Years of NASA Science and Engineering in the Classroom: The Integrated Product Team/NASA Space Missions Course

NASA Astrophysics Data System (ADS)

Hakkila, Jon; Runyon, Cassndra; Benfield, M. P. J.; Turner, Matthew W.; Farrington, Phillip A.

2015-08-01

We report on five years of an exciting and successful educational collaboration in which science undergraduates at the College of Charleston work with engineering seniors at the University of Alabama in Huntsville to design a planetary science mission in response to a mock announcement of opportunity. Alabama high schools are also heavily involved in the project, and other colleges and universities have also participated. During the two-semester course students learn about scientific goals, past missions, methods of observation, instrumentation, and component integration, proposal writing, and presentation. More importantly, students learn about real-world communication and teamwork, and go through a series of baseline reviews before presenting their results at a formal final review for a panel of NASA scientists and engineers. The project is competitive, with multiple mission designs competing with one another for the best review score. Past classes have involved missions to Venus, Europa, Titan, Mars, asteroids, comets, and even the Moon. Classroom successes and failures have both been on epic scales.

Formal Safety Certification of Aerospace Software

NASA Technical Reports Server (NTRS)

Denney, Ewen; Fischer, Bernd

2005-01-01

In principle, formal methods offer many advantages for aerospace software development: they can help to achieve ultra-high reliability, and they can be used to provide evidence of the reliability claims which can then be subjected to external scrutiny. However, despite years of research and many advances in the underlying formalisms of specification, semantics, and logic, formal methods are not much used in practice. In our opinion this is related to three major shortcomings. First, the application of formal methods is still expensive because they are labor- and knowledge-intensive. Second, they are difficult to scale up to complex systems because they are based on deep mathematical insights about the behavior of the systems (t.e., they rely on the "heroic proof"). Third, the proofs can be difficult to interpret, and typically stand in isolation from the original code. In this paper, we describe a tool for formally demonstrating safety-relevant aspects of aerospace software, which largely circumvents these problems. We focus on safely properties because it has been observed that safety violations such as out-of-bounds memory accesses or use of uninitialized variables constitute the majority of the errors found in the aerospace domain. In our approach, safety means that the program will not violate a set of rules that can range for the simple memory access rules to high-level flight rules. These different safety properties are formalized as different safety policies in Hoare logic, which are then used by a verification condition generator along with the code and logical annotations in order to derive formal safety conditions; these are then proven using an automated theorem prover. Our certification system is currently integrated into a model-based code generation toolset that generates the annotations together with the code. However, this automated formal certification technology is not exclusively constrained to our code generator and could, in principle, also be

A Method for Capturing and Reconciling Stakeholder Intentions Based on the Formal Concept Analysis

NASA Astrophysics Data System (ADS)

Aoyama, Mikio

Information systems are ubiquitous in our daily life. Thus, information systems need to work appropriately anywhere at any time for everybody. Conventional information systems engineering tends to engineer systems from the viewpoint of systems functionality. However, the diversity of the usage context requires fundamental change compared to our current thinking on information systems; from the functionality the systems provide to the goals the systems should achieve. The intentional approach embraces the goals and related aspects of the information systems. This chapter presents a method for capturing, structuring and reconciling diverse goals of multiple stakeholders. The heart of the method lies in the hierarchical structuring of goals by goal lattice based on the formal concept analysis, a semantic extension of the lattice theory. We illustrate the effectiveness of the presented method through application to the self-checkout systems for large-scale supermarkets.

Access to timely formal dementia care in Europe: protocol of the Actifcare (ACcess to Timely Formal Care) study.

PubMed

Kerpershoek, Liselot; de Vugt, Marjolein; Wolfs, Claire; Jelley, Hannah; Orrell, Martin; Woods, Bob; Stephan, Astrid; Bieber, Anja; Meyer, Gabriele; Engedal, Knut; Selbaek, Geir; Handels, Ron; Wimo, Anders; Hopper, Louise; Irving, Kate; Marques, Maria; Gonçalves-Pereira, Manuel; Portolani, Elisa; Zanetti, Orazio; Verhey, Frans

2016-08-23

Previous findings indicate that people with dementia and their informal carers experience difficulties accessing and using formal care services due to a mismatch between needs and service use. This mismatch causes overall dissatisfaction and is a waste of the scarce financial care resources. This article presents the background and methods of the Actifcare (ACcess to Timely Formal Care) project. This is a European study aiming at best-practice development in finding timely access to formal care for community-dwelling people with dementia and their informal carers. There are five main objectives: 1) Explore predisposing and enabling factors associated with the use of formal care, 2) Explore the association between the use of formal care, needs and quality of life and 3) Compare these across European countries, 4) Understand the costs and consequences of formal care services utilization in people with unmet needs, 5) Determine the major costs and quality of life drivers and their relationship with formal care services across European countries. In a longitudinal cohort study conducted in eight European countries approximately 450 people with dementia and informal carers will be assessed three times in 1 year (baseline, 6 and 12 months). In this year we will closely monitor the process of finding access to formal care. Data on service use, quality of life and needs will be collected. The results of Actifcare are expected to reveal best-practices in organizing formal care. Knowledge about enabling and predisposing factors regarding access to care services, as well as its costs and consequences, can advance the state of the art in health systems research into pathways to dementia care, in order to benefit people with dementia and their informal carers.

Engage All Americans with Eclipse 2017 Through the Eyes of NASA

NASA Astrophysics Data System (ADS)

Ng, C.; Young, C. A.; Mayo, L.; Cline, T. D.; Stephenson, B. E.; Debebe, A.; Lewis, E. M.; Odenwald, S. F.; Hill, S. W.

2016-12-01

Join NASA and millions in the U.S. and around the world in observing the August 21, 2017 solar eclipse. This presentation will discuss NASA's education and communication plans for the 2017 eclipse, highlighting some programs, resources, and citizen science activities that will engage and educate many across the country and beyond. NASA will offer unique observations of this celestial event from the ground to space. Additionally, there are do-it-yourself (DIY) science, lunar and math challenges, art contests, Makerspace ideas, and various activities for learners of all ages. Education resources and tool kits may be of particular interest to formal and informal educators. Find out what events are happening in your neighborhood, and plan your own eclipse parties with resources and activities. Last but not the least, experience the eclipse on August 21 and learn more through NASA broadcast programming that will include telescopic views from multiple locations, simple measurements, and live and taped interviews.

Non-Formal Alternatives to Schooling: A Glossary of Educational Methods.

ERIC Educational Resources Information Center

Massachusetts Univ., Amherst. Center for International Education.

This document describes activities in the field of nonformal education as an aid to educators as they develop programs to meet individual student needs. Advantages of nonformal education include that it is need-oriented, less expensive than formal systems, flexible, involves peer teaching, and does not encourage elitist feelings among students.…

Generalizability of the Ordering among Five Formal Reasoning Tasks by an Ordering-Theoretic Method.

ERIC Educational Resources Information Center

Bart, William M.; And Others

1979-01-01

Five Inhelder-Piaget formal operations tasks were analyzed to determine the extent that the formal operational skills they assess were ordered into a stable hierarchy generalizable across samples of subjects. Subjects were 34 collegiate gymnasts (19 males, 15 females), and 22 students (1 male, 21 females) from a university nursing program.…

Keldysh formalism for multiple parallel worlds

NASA Astrophysics Data System (ADS)

Ansari, M.; Nazarov, Y. V.

2016-03-01

We present a compact and self-contained review of the recently developed Keldysh formalism for multiple parallel worlds. The formalism has been applied to consistent quantum evaluation of the flows of informational quantities, in particular, to the evaluation of Renyi and Shannon entropy flows. We start with the formulation of the standard and extended Keldysh techniques in a single world in a form convenient for our presentation. We explain the use of Keldysh contours encompassing multiple parallel worlds. In the end, we briefly summarize the concrete results obtained with the method.

Keldysh formalism for multiple parallel worlds

DOE Office of Scientific and Technical Information (OSTI.GOV)

Ansari, M.; Nazarov, Y. V., E-mail: y.v.nazarov@tudelft.nl

We present a compact and self-contained review of the recently developed Keldysh formalism for multiple parallel worlds. The formalism has been applied to consistent quantum evaluation of the flows of informational quantities, in particular, to the evaluation of Renyi and Shannon entropy flows. We start with the formulation of the standard and extended Keldysh techniques in a single world in a form convenient for our presentation. We explain the use of Keldysh contours encompassing multiple parallel worlds. In the end, we briefly summarize the concrete results obtained with the method.

A Formal Semantics for the WS-BPEL Recovery Framework

NASA Astrophysics Data System (ADS)

Dragoni, Nicola; Mazzara, Manuel

While current studies on Web services composition are mostly focused - from the technical viewpoint - on standards and protocols, this work investigates the adoption of formal methods for dependable composition. The Web Services Business Process Execution Language (WS-BPEL) - an OASIS standard widely adopted both in academic and industrial environments - is considered as a touchstone for concrete composition languages and an analysis of its ambiguous Recovery Framework specification is offered. In order to show the use of formal methods, a precise and unambiguous description of its (simplified) mechanisms is provided by means of a conservative extension of the π-calculus. This has to be intended as a well known case study providing methodological arguments for the adoption of formal methods in software specification. The aspect of verification is not the main topic of the paper but some hints are given.

Development of computational methods for unsteady aerodynamics at the NASA Langley Research Center

NASA Technical Reports Server (NTRS)

Yates, E. Carson, Jr.; Whitlow, Woodrow, Jr.

1987-01-01

The current scope, recent progress, and plans for research and development of computational methods for unsteady aerodynamics at the NASA Langley Research Center are reviewed. Both integral equations and finite difference methods for inviscid and viscous flows are discussed. Although the great bulk of the effort has focused on finite difference solution of the transonic small perturbation equation, the integral equation program is given primary emphasis here because it is less well known.

Development of computational methods for unsteady aerodynamics at the NASA Langley Research Center

NASA Technical Reports Server (NTRS)

Yates, E. Carson, Jr.; Whitlow, Woodrow, Jr.

1987-01-01

The current scope, recent progress, and plans for research and development of computational methods for unsteady aerodynamics at the NASA Langley Research Center are reviewed. Both integral-equations and finite-difference method for inviscid and viscous flows are discussed. Although the great bulk of the effort has focused on finite-difference solution of the transonic small-perturbation equation, the integral-equation program is given primary emphasis here because it is less well known.

Linking Formal and Informal Science Education: A Successful Model using Libraries, Volunteers and NASA Resources

NASA Astrophysics Data System (ADS)

Race, M. S.; Lafayette Library; Learning Center Foundation (Lllcf)

2011-12-01

In these times of budget cuts, tight school schedules, and limited opportunities for student field trips and teacher professional development, it is especially difficult to expose elementary and middle school students to the latest STEM information-particularly in the space sciences. Using our library as a facilitator and catalyst, we built a volunteer-based, multi-faceted, curriculum-linked program for students and teachers in local middle schools (Grade 8) and showcased new astronomical and planetary science information using mainly NASA resources and volunteer effort. The project began with the idea of bringing free NASA photo exhibits (FETTU) to the Lafayette and Antioch Libraries for public display. Subsequently, the effort expanded by adding layers of activities that brought space and science information to teachers, students and the pubic at 5 libraries and schools in the 2 cities, one of which serves a diverse, underserved community. Overall, the effort (supported by a pilot grant from the Bechtel Foundation) included school and library based teacher workshops with resource materials; travelling space museum visits with hands-on activities (Chabot-to-Go); separate powerpoint presentations for students and adults at the library; and concurrent ancillary space-related themes for young children's programs at the library. This pilot project, based largely on the use of free government resources and online materials, demonstrated that volunteer-based, standards-linked STEM efforts can enhance curriculum at the middle school, with libraries serving a special role. Using this model, we subsequently also obtained a small NASA-Space Grant award to bring star parties and hand-on science activities to three libraries this Fall, linking with numerous Grade 5 teachers and students in two additional underserved areas of our county. It's not necessary to reinvent the wheel, you just collect the pieces and build on what you already have.

Engaging Scientists in Meaningful E/PO: How the NASA SMD E/PO Community Addresses Informal Educators' Preferences for PD and Materials

NASA Astrophysics Data System (ADS)

Bartolone, Lindsay; Nelson, Andi; Smith, Denise A.; NASA SMD Astrophysics E/PO Community

2015-01-01

The NASA Astrophysics Science Education and Public Outreach Forum (SEPOF) coordinates the work of NASA Science Mission Directorate (SMD) Astrophysics EPO projects. These teams work together to capitalize on the cutting-edge discoveries of NASA Astrophysics missions to support educators in Science, Technology, Engineering, and Math (STEM) and to enable youth to engage in doing STEM inside and outside of school. The Astrophysics Forum assists scientists and educators with becoming involved in SMD E/PO, which is uniquely poised to foster collaboration between scientists with content expertise and educators with pedagogy expertise, and makes SMD E/PO resources and expertise accessible to the science and education communities. Informal educators participated in a recent nationally-distributed survey from the NASA SMD SEPOF Informal Education Working Group. The results show the preferences of staff from museums, parks, public libraries, community/afterschool centers, and others with regard to professional development and material resources. The results of the survey will be presented during this session.In addition, we present opportunities for the astronomy community to participate in collaborations supporting the NASA SMD efforts in K-12 Formal Education, Informal Science Education, and Outreach. These efforts focus on enhancing instruction, as well as youth and public engagement, in STEM via use of research-based best practices, collaborations with libraries, partnerships with local and national organizations, and remote engagement of audiences. The Forums' efforts for the Formal, Informal Science Education and Outreach communities include a literature review, appraisal of informal educators' needs, coordination of audience-based NASA resources and opportunities, professional development, plus support with the Next Generation Science Standards. Learn how to join in our collaborative efforts to support the K-12 Formal Education community and to reach the informal

NASA Technical Standards Program and Implications for Lessons Learned and Technical Standard Integration

NASA Technical Reports Server (NTRS)

Gill, Paul S.; Garcia, Danny; Vaughan, William W.; Parker, Nelson C. (Technical Monitor)

2002-01-01

The National Aeronautics and Space Agency consists of fourteen Facilities throughout the United States. They are organized to support the Agency's principal Enterprises: (1) Space Science, (2) Earth Science, (3) Aerospace Technology, (4) Human Exploration and Development of Space, and (5) Biological and Physical Research. Technical Standards are important to the activities of each Enterprise and have been an integral part in the development and operation of NASA Programs and Projects since the Agency was established in 1959. However, for years each Center was responsible for its own standards development and selection of non-NASA technical standards that met the needs of Programs and Projects for which they were responsible. There were few Agencywide applicable Technical Standards, mainly those in area of safety. Department of Defense Standards and Specifications were the foundation and main source for Technical Standards used by the Agency. This process existed until about 1997 when NASA embarked on a Program to convert NASA's Center-developed Technical Standards into Agencywide endorsed NASA Preferred Technical Standards. In addition, action was taken regarding the formal adoption of non-NASA Technical Standards (DOD, SAE, ASTM, ASME, IEEE, etc.) as NASA Preferred Technical Standards.

Towards the formal verification of the requirements and design of a processor interface unit

NASA Technical Reports Server (NTRS)

Fura, David A.; Windley, Phillip J.; Cohen, Gerald C.

1993-01-01

The formal verification of the design and partial requirements for a Processor Interface Unit (PIU) using the Higher Order Logic (HOL) theorem-proving system is described. The processor interface unit is a single-chip subsystem within a fault-tolerant embedded system under development within the Boeing Defense and Space Group. It provides the opportunity to investigate the specification and verification of a real-world subsystem within a commercially-developed fault-tolerant computer. An overview of the PIU verification effort is given. The actual HOL listing from the verification effort are documented in a companion NASA contractor report entitled 'Towards the Formal Verification of the Requirements and Design of a Processor Interface Unit - HOL Listings' including the general-purpose HOL theories and definitions that support the PIU verification as well as tactics used in the proofs.

Acoustic prediction methods for the NASA generalized advanced propeller analysis system (GAPAS)

NASA Technical Reports Server (NTRS)

Padula, S. L.; Block, P. J. W.

1984-01-01

Classical methods of propeller performance analysis are coupled with state-of-the-art Aircraft Noise Prediction Program (ANOPP:) techniques to yield a versatile design tool, the NASA Generalized Advanced Propeller Analysis System (GAPAS) for the novel quiet and efficient propellers. ANOPP is a collection of modular specialized programs. GAPAS as a whole addresses blade geometry and aerodynamics, rotor performance and loading, and subsonic propeller noise.

Adolescent thinking ála Piaget: The formal stage.

PubMed

Dulit, E

1972-12-01

Two of the formal-stage experiments of Piaget and Inhelder, selected largely for their closeness to the concepts defining the stage, were replicated with groups of average and gifted adolescents. This report describes the relevant Piagetian concepts (formal stage, concrete stage) in context, gives the methods and findings of this study, and concludes with a section discussing implications and making some reformulations which generally support but significantly qualify some of the central themes of the Piaget-Inhelder work. Fully developed formal-stage thinking emerges as far from commonplace among normal or average adolescents (by marked contrast with the impression created by the Piaget-Inhelder text, which chooses to report no middle or older adolescents who function at less than fully formal levels). In this respect, the formal stage differs appreciably from the earlier Piagetian stages, and early adolescence emerges as the age for which a "single path" model of cognitive development becomes seriously inadequate and a more complex model becomes essential. Formal-stage thinking seems best conceptualized, like most other aspects of psychological maturity, as a potentiality only partially attained by most and fully attained only by some.

Formal, Non-Formal and Informal Learning in the Sciences

ERIC Educational Resources Information Center

Ainsworth, Heather L.; Eaton, Sarah Elaine

2010-01-01

This research report investigates the links between formal, non-formal and informal learning and the differences between them. In particular, the report aims to link these notions of learning to the field of sciences and engineering in Canada and the United States, including professional development of adults working in these fields. It offers…

NASA/FAA helicopter simulator workshop

NASA Technical Reports Server (NTRS)

Larsen, William E. (Editor); Randle, Robert J., Jr. (Editor); Bray, Richard S. (Editor); Zuk, John (Editor)

1992-01-01

A workshop was convened by the FAA and NASA for the purpose of providing a forum at which leading designers, manufacturers, and users of helicopter simulators could initiate and participate in a development process that would facilitate the formulation of qualification standards by the regulatory agency. Formal papers were presented, special topics were discussed in breakout sessions, and a draft FAA advisory circular defining specifications for helicopter simulators was presented and discussed. A working group of volunteers was formed to work with the National Simulator Program Office to develop a final version of the circular. The workshop attracted 90 individuals from a constituency of simulator manufacturers, training organizations, the military, civil regulators, research scientists, and five foreign countries.

Making NASA Earth Observing System Satellite Data Accessible to the K-12 and Citizen Scientist Communities

NASA Technical Reports Server (NTRS)

Moore, Susan W.; Phelps, Carrie S.; Chambers, Lin H.

2004-01-01

The Atmospheric Sciences Data Center (ASDC) at NASA s Langley Research Center houses over 700 data sets related to Earth s radiation budget, clouds, aerosols and tropospheric chemistry. These data sets are produced to increase academic understanding of the natural and anthropogenic perturbations that influence global climate change. The Mentoring and inquirY using NASA Data on Atmospheric and earth science for Teachers and Amateurs (MY NASA DATA) project has been established to systematically support educational activities at all levels of formal and informal education by reducing these large data holdings to microsets that will be easily explored and understood by the K-12 and the amateur scientist communities

48 CFR 1852.245-73 - Financial reporting of NASA property in the custody of contractors.

Code of Federal Regulations, 2013 CFR

2013-10-01

... due. However, contractors' procedures must document the process for developing these estimates based... shall have formal policies and procedures, which address the validation of NF 1018 data, including data... validation is to ensure that information reported is accurate and in compliance with the NASA FAR Supplement...

48 CFR 1852.245-73 - Financial reporting of NASA property in the custody of contractors.

Code of Federal Regulations, 2012 CFR

2012-10-01

... due. However, contractors' procedures must document the process for developing these estimates based... shall have formal policies and procedures, which address the validation of NF 1018 data, including data... validation is to ensure that information reported is accurate and in compliance with the NASA FAR Supplement...

Memory sparing, fast scattering formalism for rigorous diffraction modeling

NASA Astrophysics Data System (ADS)

Iff, W.; Kämpfe, T.; Jourlin, Y.; Tishchenko, A. V.

2017-07-01

The basics and algorithmic steps of a novel scattering formalism suited for memory sparing and fast electromagnetic calculations are presented. The formalism, called ‘S-vector algorithm’ (by analogy with the known scattering-matrix algorithm), allows the calculation of the collective scattering spectra of individual layered micro-structured scattering objects. A rigorous method of linear complexity is applied to model the scattering at individual layers; here the generalized source method (GSM) resorting to Fourier harmonics as basis functions is used as one possible method of linear complexity. The concatenation of the individual scattering events can be achieved sequentially or in parallel, both having pros and cons. The present development will largely concentrate on a consecutive approach based on the multiple reflection series. The latter will be reformulated into an implicit formalism which will be associated with an iterative solver, resulting in improved convergence. The examples will first refer to 1D grating diffraction for the sake of simplicity and intelligibility, with a final 2D application example.

Analytical solution of Schrödinger equation in minimal length formalism for trigonometric potential using hypergeometry method

NASA Astrophysics Data System (ADS)

Nurhidayati, I.; Suparmi, A.; Cari, C.

2018-03-01

The Schrödinger equation has been extended by applying the minimal length formalism for trigonometric potential. The wave function and energy spectra were used to describe the behavior of subatomic particle. The wave function and energy spectra were obtained by using hypergeometry method. The result showed that the energy increased by the increasing both of minimal length parameter and the potential parameter. The energy were calculated numerically using MatLab.

Formal Assurance for Cognitive Architecture Based Autonomous Agent

NASA Technical Reports Server (NTRS)

Bhattacharyya, Siddhartha; Eskridge, Thomas; Neogi, Natasha; Carvalho, Marco

2017-01-01

Autonomous systems are designed and deployed in different modeling paradigms. These environments focus on specific concepts in designing the system. We focus our effort in the use of cognitive architectures to design autonomous agents to collaborate with humans to accomplish tasks in a mission. Our research focuses on introducing formal assurance methods to verify the behavior of agents designed in Soar, by translating the agent to the formal verification environment Uppaal.

Formal reasoning about systems biology using theorem proving

PubMed Central

Hasan, Osman; Siddique, Umair; Tahar, Sofiène

2017-01-01

System biology provides the basis to understand the behavioral properties of complex biological organisms at different levels of abstraction. Traditionally, analysing systems biology based models of various diseases have been carried out by paper-and-pencil based proofs and simulations. However, these methods cannot provide an accurate analysis, which is a serious drawback for the safety-critical domain of human medicine. In order to overcome these limitations, we propose a framework to formally analyze biological networks and pathways. In particular, we formalize the notion of reaction kinetics in higher-order logic and formally verify some of the commonly used reaction based models of biological networks using the HOL Light theorem prover. Furthermore, we have ported our earlier formalization of Zsyntax, i.e., a deductive language for reasoning about biological networks and pathways, from HOL4 to the HOL Light theorem prover to make it compatible with the above-mentioned formalization of reaction kinetics. To illustrate the usefulness of the proposed framework, we present the formal analysis of three case studies, i.e., the pathway leading to TP53 Phosphorylation, the pathway leading to the death of cancer stem cells and the tumor growth based on cancer stem cells, which is used for the prognosis and future drug designs to treat cancer patients. PMID:28671950

A new method based on the Butler-Volmer formalism to evaluate voltammetric cation and anion sensors.

PubMed

Cano, Manuel; Rodríguez-Amaro, Rafael; Fernández Romero, Antonio J

2008-12-11

A new method based on the Butler-Volmer formalism is applied to assess the capability of two voltammetric ion sensors based on polypyrrole films: PPy/DBS and PPy/ClO4 modified electrodes were studied as voltammetric cation and anion sensors, respectively. The reversible potential versus electrolyte concentrations semilogarithm plots provided positive calibration slopes for PPy/DBS and negative ones for PPy/ClO4, as was expected from the proposed method and that based on the Nernst equation. The slope expressions deduced from Butler-Volmer include the electron-transfer coefficient, which allows slope values different from the ideal Nernstian value to be explained. Both polymeric films exhibited a degree of ion-selectivity when they were immersed in mixed-analyte solutions. Selectivity coefficients for the two proposed voltammetric cation and anion sensors were obtained by several experimental methods, including the separated solution method (SSM) and matched potential method (MPM). The K values acquired by the different methods were very close for both polymeric sensors.

Through the Eyes of NASA: NASA's 2017 Eclipse Education Progam

NASA Astrophysics Data System (ADS)

Mayo, L.

2017-12-01

Over the last three years, NASA has been developing plans to bring the August 21st total solar eclipse to the nation, "as only NASA can", leveraging its considerable space assets, technology, scientists, and its unmatched commitment to science education. The eclipse, long anticipated by many groups, represents the largest Big Event education program that NASA has ever undertaken. It is the latest in a long string of successful Big Event international celebrations going back two decades including both transits of Venus, three solar eclipses, solar maximum, and mission events such as the MSL/Curiosity landing on Mars, and the launch of the Lunar Reconnaissance Orbiter (LRO) to name a few. This talk will detail NASA's program development methods, strategic partnerships, and strategies for using this celestial event to engage the nation and improve overall science literacy.

National Aeronautics and Space Administration (NASA) education 1993--2009

NASA Astrophysics Data System (ADS)

Ivie, Christine M.

The National Aeronautics and Space Administration was established in 1958 and began operating a formal education program in 1993. The purpose of this study was to analyze the education program from 1993 -- 2009 by examining strategic plan documents produced by the NASA education office and interviewing NASA education officials who served during that time period. Constant changes in education leadership at NASA resulted in changes in direction in the education program and the documents produced by each administration reflected both small and some significant changes in program direction. The result of the analysis of documents and interview data was the identification of several trends in the NASA education program. This study identified three significant trends in NASA education. First, the approach that NASA took in both its EPO efforts and in the efforts directed by the Office of Education is disjointed and seems to reflect individual preferences in education approaches designed to reach populations that are of interest to the individuals in decision-making positions rather than reflect a systematic approach designed to meet identified goals and outcomes. Second, this disjointed and person-driven approach led to a lack of consistent evaluation data available for review and planning purposes. Third, there was an ongoing assumption made by the education community that NASA education efforts were tied to larger education reports, concerns, needs, initiatives and evidence collected and presented in Science Technology Engineering and Math (STEM) education-related studies over the past twenty years. In fact, there is no evidence that the programs and projects initiated were a response to these identified needs or initiatives. That does not mean that NASA's efforts did not contribute to STEM education initiatives in the United States. This study, however, indicates that contributions to those initiatives occurred as a byproduct of the effort and not because of specific

ThermoBuild: Online Method Made Available for Accessing NASA Glenn Thermodynamic Data

NASA Technical Reports Server (NTRS)

McBride, Bonnie; Zehe, Michael J.

2004-01-01

The new Web site program "ThermoBuild" allows users to easily access and use the NASA Glenn Thermodynamic Database of over 2000 solid, liquid, and gaseous species. A convenient periodic table allows users to "build" the molecules of interest and designate the temperature range over which thermodynamic functions are to be displayed. ThermoBuild also allows users to build custom databases for use with NASA's Chemical Equilibrium with Applications (CEA) program or other programs that require the NASA format for thermodynamic properties. The NASA Glenn Research Center has long been a leader in the compilation and dissemination of up-to-date thermodynamic data, primarily for use with the NASA CEA program, but increasingly for use with other computer programs.

Evaluation of Alternative Altitude Scaling Methods for Thermal Ice Protection System in NASA Icing Research Tunnel

NASA Technical Reports Server (NTRS)

Lee, Sam; Addy, Harold E. Jr.; Broeren, Andy P.; Orchard, David M.

2017-01-01

A test was conducted at NASA Icing Research Tunnel to evaluate altitude scaling methods for thermal ice protection system. Two new scaling methods based on Weber number were compared against a method based on Reynolds number. The results generally agreed with the previous set of tests conducted in NRCC Altitude Icing Wind Tunnel where the three methods of scaling were also tested and compared along with reference (altitude) icing conditions. In those tests, the Weber number-based scaling methods yielded results much closer to those observed at the reference icing conditions than the Reynolds number-based icing conditions. The test in the NASA IRT used a much larger, asymmetric airfoil with an ice protection system that more closely resembled designs used in commercial aircraft. Following the trends observed during the AIWT tests, the Weber number based scaling methods resulted in smaller runback ice than the Reynolds number based scaling, and the ice formed farther upstream. The results show that the new Weber number based scaling methods, particularly the Weber number with water loading scaling, continue to show promise for ice protection system development and evaluation in atmospheric icing tunnels.

Implementation of the nudged elastic band method in a dislocation dynamics formalism: Application to dislocation nucleation

NASA Astrophysics Data System (ADS)

Geslin, Pierre-Antoine; Gatti, Riccardo; Devincre, Benoit; Rodney, David

2017-11-01

We propose a framework to study thermally-activated processes in dislocation glide. This approach is based on an implementation of the nudged elastic band method in a nodal mesoscale dislocation dynamics formalism. Special care is paid to develop a variational formulation to ensure convergence to well-defined minimum energy paths. We also propose a methodology to rigorously parametrize the model on atomistic data, including elastic, core and stacking fault contributions. To assess the validity of the model, we investigate the homogeneous nucleation of partial dislocation loops in aluminum, recovering the activation energies and loop shapes obtained with atomistic calculations and extending these calculations to lower applied stresses. The present method is also applied to heterogeneous nucleation on spherical inclusions.

NASA Advanced Supercomputing Facility Expansion

NASA Technical Reports Server (NTRS)

Thigpen, William W.

2017-01-01

The NASA Advanced Supercomputing (NAS) Division enables advances in high-end computing technologies and in modeling and simulation methods to tackle some of the toughest science and engineering challenges facing NASA today. The name "NAS" has long been associated with leadership and innovation throughout the high-end computing (HEC) community. We play a significant role in shaping HEC standards and paradigms, and provide leadership in the areas of large-scale InfiniBand fabrics, Lustre open-source filesystems, and hyperwall technologies. We provide an integrated high-end computing environment to accelerate NASA missions and make revolutionary advances in science. Pleiades, a petaflop-scale supercomputer, is used by scientists throughout the U.S. to support NASA missions, and is ranked among the most powerful systems in the world. One of our key focus areas is in modeling and simulation to support NASA's real-world engineering applications and make fundamental advances in modeling and simulation methods.

Higher order temporal finite element methods through mixed formalisms.

PubMed

Kim, Jinkyu

2014-01-01

The extended framework of Hamilton's principle and the mixed convolved action principle provide new rigorous weak variational formalism for a broad range of initial boundary value problems in mathematical physics and mechanics. In this paper, their potential when adopting temporally higher order approximations is investigated. The classical single-degree-of-freedom dynamical systems are primarily considered to validate and to investigate the performance of the numerical algorithms developed from both formulations. For the undamped system, all the algorithms are symplectic and unconditionally stable with respect to the time step. For the damped system, they are shown to be accurate with good convergence characteristics.

A Comparison of Participation Patterns in Selected Formal, Non-Formal, and Informal Online Learning Environments

ERIC Educational Resources Information Center

Schwier, Richard A.; Seaton, J. X.

2013-01-01

Does learner participation vary depending on the learning context? Are there characteristic features of participation evident in formal, non-formal, and informal online learning environments? Six online learning environments were chosen as epitomes of formal, non-formal, and informal learning contexts and compared. Transcripts of online…

Consumer experience of formal crisis-response services and preferred methods of crisis intervention.

PubMed

Boscarato, Kara; Lee, Stuart; Kroschel, Jon; Hollander, Yitzchak; Brennan, Alice; Warren, Narelle

2014-08-01

The manner in which people with mental illness are supported in a crisis is crucial to their recovery. The current study explored mental health consumers' experiences with formal crisis services (i.e. police and crisis assessment and treatment (CAT) teams), preferred crisis supports, and opinions of four collaborative interagency response models. Eleven consumers completed one-on-one, semistructured interviews. The results revealed that the perceived quality of previous formal crisis interventions varied greatly. Most participants preferred family members or friends to intervene. However, where a formal response was required, general practitioners and mental health case managers were preferred; no participant wanted a police response, and only one indicated a preference for CAT team assistance. Most participants welcomed collaborative crisis interventions. Of four collaborative interagency response models currently being trialled internationally, participants most strongly supported the Ride-Along Model, which enables a police officer and a mental health clinician to jointly respond to distressed consumers in the community. The findings highlight the potential for an interagency response model to deliver a crisis response aligned with consumers' preferences. © 2014 Australian College of Mental Health Nurses Inc.

Internal NASA Study: NASAs Protoflight Research Initiative

NASA Technical Reports Server (NTRS)

Coan, Mary R.; Hirshorn, Steven R.; Moreland, Robert

2015-01-01

The NASA Protoflight Research Initiative is an internal NASA study conducted within the Office of the Chief Engineer to better understand the use of Protoflight within NASA. Extensive literature reviews and interviews with key NASA members with experience in both robotic and human spaceflight missions has resulted in three main conclusions and two observations. The first conclusion is that NASA's Protoflight method is not considered to be "prescriptive." The current policies and guidance allows each Program/Project to tailor the Protoflight approach to better meet their needs, goals and objectives. Second, Risk Management plays a key role in implementation of the Protoflight approach. Any deviations from full qualification will be based on the level of acceptable risk with guidance found in NPR 8705.4. Finally, over the past decade (2004 - 2014) only 6% of NASA's Protoflight missions and 6% of NASA's Full qualification missions experienced a publicly disclosed mission failure. In other words, the data indicates that the Protoflight approach, in and of it itself, does not increase the mission risk of in-flight failure. The first observation is that it would be beneficial to document the decision making process on the implementation and use of Protoflight. The second observation is that If a Project/Program chooses to use the Protoflight approach with relevant heritage, it is extremely important that the Program/Project Manager ensures that the current project's requirements falls within the heritage design, component, instrument and/or subsystem's requirements for both the planned and operational use, and that the documentation of the relevant heritage is comprehensive, sufficient and the decision well documented. To further benefit/inform this study, a recommendation to perform a deep dive into 30 missions with accessible data on their testing/verification methodology and decision process to research the differences between Protoflight and Full Qualification

Improving Learner Outcomes in Lifelong Education: Formal Pedagogies in Non-Formal Learning Contexts?

ERIC Educational Resources Information Center

Zepke, Nick; Leach, Linda

2006-01-01

This article explores how far research findings about successful pedagogies in formal post-school education might be used in non-formal learning contexts--settings where learning may not lead to formal qualifications. It does this by examining a learner outcomes model adapted from a synthesis of research into retention. The article first…

A History of NASA Remote Sensing Contributions to Archaeology

NASA Technical Reports Server (NTRS)

Giardino, Marco J.

2010-01-01

During its long history of developing and deploying remote sensing instruments, NASA has provided a scientific data that have benefitted a variety of scientific applications among them archaeology. Multispectral and hyperspectral instrument mounted on orbiting and suborbital platforms have provided new and important information for the discovery, delineation and analysis of archaeological sites worldwide. Since the early 1970s, several of the ten NASA centers have collaborated with archaeologists to refine and validate the use of active and passive remote sensing for archeological use. The Stennis Space Center (SSC), located in Mississippi USA has been the NASA leader in archeological research. Together with colleagues from Goddard Space Flight Center (GSFC), Marshall Space Flight Center (MSFC), and the Jet Propulsion Laboratory (JPL), SSC scientists have provided the archaeological community with useful images and sophisticated processing that have pushed the technological frontiers of archaeological research and applications. Successful projects include identifying prehistoric roads in Chaco canyon, identifying sites from the Lewis and Clark Corps of Discovery exploration and assessing prehistoric settlement patterns in southeast Louisiana. The Scientific Data Purchase (SDP) stimulated commercial companies to collect archaeological data. At present, NASA formally solicits "space archaeology" proposals through its Earth Science Directorate and continues to assist archaeologists and cultural resource managers in doing their work more efficiently and effectively. This paper focuses on passive remote sensing and does not consider the significant contributions made by NASA active sensors. Hyperspectral data offers new opportunities for future archeological discoveries.

Formalization of an environmental model using formal concept analysis - FCA

NASA Astrophysics Data System (ADS)

Bourdon-García, Rubén D.; Burgos-Salcedo, Javier D.

2016-08-01

Nowadays, there is a huge necessity to generate novel strategies for social-ecological systems analyses for resolving global sustainability problems. This paper has as main purpose the application of the formal concept analysis to formalize the theory of Augusto Ángel Maya, who without a doubt, was one of the most important environmental philosophers in South America; Ángel Maya proposed and established that Ecosystem-Culture relations, instead Human-Nature ones, are determinants in our understanding and management of natural resources. Based on this, a concept lattice, formal concepts, subconcept-superconcept relations, partially ordered sets, supremum and infimum of the lattice and implications between attributes (Duquenne-Guigues base), were determined for the ecosystem-culture relations.

Disseminating NASA-based science through NASA's Universe of Learning: Girls STEAM Ahead

NASA Astrophysics Data System (ADS)

Marcucci, E.; Meinke, B. K.; Smith, D. A.; Ryer, H.; Slivinski, C.; Kenney, J.; Arcand, K.; Cominsky, L.

2017-12-01

The Girls STEAM Ahead with NASA (GSAWN) initiative partners the NASA's Universe of Learning (UoL) resources with public libraries to provide NASA-themed activities for girls and their families. The program expands upon the legacy program, NASA Science4Girls and Their Families, in celebration of National Women's History Month. Program resources include hands-on activities for engaging girls, such as coding experiences and use of remote telescopes, complementary exhibits, and professional development for library partner staff. The science-institute-embedded partners in NASA's UoL are uniquely poised to foster collaboration between scientists with content expertise and educators with pedagogy expertise. The thematic topics related to NASA Astrophysics enable audiences to experience the full range of NASA scientific and technical disciplines and the different career skills each requires. For example, an activity may focus on understanding exoplanets, methods of their detection, and characteristics that can be determined remotely. The events focus on engaging underserved and underrepresented audiences in Science, Technology, Engineering, and Mathematics (STEM) via use of research-based best practices, collaborations with libraries, partnerships with local and national organizations (e.g. National Girls Collaborative Project or NGCP), and remote engagement of audiences. NASA's UoL collaborated with another NASA STEM Activation partner, NASA@ My Library, to announce GSAWN to their extensive STAR_Net network of libraries. This partnership between NASA SMD-funded Science learning and literacy teams has included NASA@ My Library hosting a professional development webinar featuring a GSAWN activity, a newsletter and blog post about the program, and plans for future exhibit development. This presentation will provide an overview of the program's progress to engage girls and their families through the development and dissemination of NASA-based science programming.

An Educational Development Tool Based on Principles of Formal Ontology

ERIC Educational Resources Information Center

Guzzi, Rodolfo; Scarpanti, Stefano; Ballista, Giovanni; Di Nicolantonio, Walter

2005-01-01

Computer science provides with virtual laboratories, places where one can merge real experiments with the formalism of algorithms and mathematics and where, with the advent of multimedia, sounds and movies can also be added. In this paper we present a method, based on principles of formal ontology, allowing one to develop interactive educational…

Combining Formal, Non-Formal and Informal Learning for Workforce Skill Development

ERIC Educational Resources Information Center

Misko, Josie

2008-01-01

This literature review, undertaken for Australian Industry Group, shows how multiple variations and combinations of formal, informal and non-formal learning, accompanied by various government incentives and organisational initiatives (including job redesign, cross-skilling, multi-skilling, diversified career pathways, action learning projects,…

NASA's Aeroacoustic Tools and Methods for Analysis of Aircraft Noise

NASA Technical Reports Server (NTRS)

Rizzi, Stephen A.; Lopes, Leonard V.; Burley, Casey L.

2015-01-01

Aircraft community noise is a significant concern due to continued growth in air traffic, increasingly stringent environmental goals, and operational limitations imposed by airport authorities. The ability to quantify aircraft noise at the source and ultimately at observers is required to develop low noise aircraft designs and flight procedures. Predicting noise at the source, accounting for scattering and propagation through the atmosphere to the observer, and assessing the perception and impact on a community requires physics-based aeroacoustics tools. Along with the analyses for aero-performance, weights and fuel burn, these tools can provide the acoustic component for aircraft MDAO (Multidisciplinary Design Analysis and Optimization). Over the last decade significant progress has been made in advancing the aeroacoustic tools such that acoustic analyses can now be performed during the design process. One major and enabling advance has been the development of the system noise framework known as Aircraft NOise Prediction Program2 (ANOPP2). ANOPP2 is NASA's aeroacoustic toolset and is designed to facilitate the combination of acoustic approaches of varying fidelity for the analysis of noise from conventional and unconventional aircraft. The toolset includes a framework that integrates noise prediction and propagation methods into a unified system for use within general aircraft analysis software. This includes acoustic analyses, signal processing and interfaces that allow for the assessment of perception of noise on a community. ANOPP2's capability to incorporate medium fidelity shielding predictions and wind tunnel experiments into a design environment is presented. An assessment of noise from a conventional and Hybrid Wing Body (HWB) aircraft using medium fidelity scattering methods combined with noise measurements from a model-scale HWB recently placed in NASA's 14x22 wind tunnel are presented. The results are in the form of community noise metrics and

Bridging the gap between formal and experience-based knowledge for context-aware laparoscopy.

PubMed

Katić, Darko; Schuck, Jürgen; Wekerle, Anna-Laura; Kenngott, Hannes; Müller-Stich, Beat Peter; Dillmann, Rüdiger; Speidel, Stefanie

2016-06-01

Computer assistance is increasingly common in surgery. However, the amount of information is bound to overload processing abilities of surgeons. We propose methods to recognize the current phase of a surgery for context-aware information filtering. The purpose is to select the most suitable subset of information for surgical situations which require special assistance. We combine formal knowledge, represented by an ontology, and experience-based knowledge, represented by training samples, to recognize phases. For this purpose, we have developed two different methods. Firstly, we use formal knowledge about possible phase transitions to create a composition of random forests. Secondly, we propose a method based on cultural optimization to infer formal rules from experience to recognize phases. The proposed methods are compared with a purely formal knowledge-based approach using rules and a purely experience-based one using regular random forests. The comparative evaluation on laparoscopic pancreas resections and adrenalectomies employs a consistent set of quality criteria on clean and noisy input. The rule-based approaches proved best with noisefree data. The random forest-based ones were more robust in the presence of noise. Formal and experience-based knowledge can be successfully combined for robust phase recognition.

Using Life-Cycle Human Factors Engineering to Avoid $2.4 Million in Costs: Lessons Learned from NASA's Requirements Verification Process for Space Payloads

NASA Technical Reports Server (NTRS)

Carr, Daniel; Ellenberger, Rich

2008-01-01

The Human Factors Implementation Team (HFIT) process has been used to verify human factors requirements for NASA International Space Station (ISS) payloads since 2003, resulting in $2.4 million in avoided costs. This cost benefit has been realized by greatly reducing the need to process time-consuming formal waivers (exceptions) for individual requirements violations. The HFIT team, which includes astronauts and their technical staff, acts as the single source for human factors requirements integration of payloads. HFIT has the authority to provide inputs during early design phases, thus eliminating many potential requirements violations in a cost-effective manner. In those instances where it is not economically or technically feasible to meet the precise metric of a given requirement, HFIT can work with the payload engineers to develop common sense solutions and formally document that the resulting payload design does not materially affect the astronaut s ability to operate and interact with the payload. The HFIT process is fully ISO 9000 compliant and works concurrently with NASA s formal systems engineering work flow. Due to its success with payloads, the HFIT process is being adapted and extended to ISS systems hardware. Key aspects of this process are also being considered for NASA's Space Shuttle replacement, the Crew Exploration Vehicle.

General Formalism of Mass Scaling Approach for Replica-Exchange Molecular Dynamics and its Application

NASA Astrophysics Data System (ADS)

Nagai, Tetsuro

2017-01-01

Replica-exchange molecular dynamics (REMD) has demonstrated its efficiency by combining trajectories of a wide range of temperatures. As an extension of the method, the author formalizes the mass-manipulating replica-exchange molecular dynamics (MMREMD) method that allows for arbitrary mass scaling with respect to temperature and individual particles. The formalism enables the versatile application of mass-scaling approaches to the REMD method. The key change introduced in the novel formalism is the generalized rules for the velocity and momentum scaling after accepted replica-exchange attempts. As an application of this general formalism, the refinement of the viscosity-REMD (V-REMD) method [P. H. Nguyen, J. Chem. Phys. 132, 144109 (2010)] is presented. Numerical results are provided using a pilot system, demonstrating easier and more optimized applicability of the new version of V-REMD as well as the importance of adherence to the generalized velocity scaling rules. With the new formalism, more sound and efficient simulations will be performed.

Beyond formalism

NASA Technical Reports Server (NTRS)

Denning, Peter J.

1991-01-01

The ongoing debate over the role of formalism and formal specifications in software features many speakers with diverse positions. Yet, in the end, they share the conviction that the requirements of a software system can be unambiguously specified, that acceptable software is a product demonstrably meeting the specifications, and that the design process can be carried out with little interaction between designers and users once the specification has been agreed to. This conviction is part of a larger paradigm prevalent in American management thinking, which holds that organizations are systems that can be precisely specified and optimized. This paradigm, which traces historically to the works of Frederick Taylor in the early 1900s, is no longer sufficient for organizations and software systems today. In the domain of software, a new paradigm, called user-centered design, overcomes the limitations of pure formalism. Pioneered in Scandinavia, user-centered design is spreading through Europe and is beginning to make its way into the U.S.

Formalizing Resources for Planning

NASA Technical Reports Server (NTRS)

Bedrax-Weiss, Tania; McGann, Conor; Ramakrishnan, Sailesh

2003-01-01

In this paper we present a classification scheme which circumscribes a large class of resources found in the real world. Building on the work of others we also define key properties of resources that allow formal expression of the proposed classification. Furthermore, operations that change the state of a resource are formalized. Together, properties and operations go a long way in formalizing the representation and reasoning aspects of resources for planning.

Bridging the Gap between Earth Science and Students: An Integrated Approach using NASA Earth Science Climate Data

NASA Technical Reports Server (NTRS)

Alston, Erica J.; Chambers, Lin H.; Phelps, Carrie S.; Oots, Penny C.; Moore, Susan W.; Diones, Dennis D.

2007-01-01

Under the auspices of the Department of Education's No Child Left Behind (NCLB) Act, beginning in 2007 students will be tested in the science area. There are many techniques that educators can employ to teach students science. The use of authentic materials or in this case authentic data can be an engaging alternative to more traditional methods. An Earth science classroom is a great place for the integration of authentic data and science concepts. The National Aeronautics and Space Administration (NASA) has a wealth of high quality Earth science data available to the general public. For instance, the Atmospheric Science Data Center (ASDC) at NASA s Langley Research Center houses over 800 Earth science data sets related to Earth's radiation budget, clouds, aerosols and tropospheric chemistry. These data sets were produced to increase academic understanding of the natural and anthropogenic factors that influence global climate; however, a major hurdle in using authentic data is the size of the data and data documentation. To facilitate the use of these data sets for educational purposes, the Mentoring and inquirY using NASA Data on Atmospheric and Earth science for Teachers and Amateurs (MY NASA DATA) project has been established to systematically support educational activities at all levels of formal and informal education. The MY NASA DATA project accomplishes this by reducing these large data holdings to microsets that are easily accessible and explored by K-12 educators and students though the project's Web page. MY NASA DATA seeks to ease the difficulty in understanding the jargon-heavy language of Earth science. This manuscript will show how MY NASA DATA provides resources for NCLB implementation in the science area through an overview of the Web site, the different microsets available, the lesson plans and computer tools, and an overview of educational support mechanisms.

NASA World Wind, Open Source 4D Geospatial Visualization Platform: *.NET & Java*

NASA Astrophysics Data System (ADS)

Hogan, P.; Coughlan, J.

2006-12-01

NASA World Wind has only one goal, to provide the maximum opportunity for geospatial information to be experienced, be it education, science, research, business, or government. The benefits to understanding for information delivered in the context of its 4D virtual reality are extraordinary. The NASA World Wind visualization platform is open source and therefore lends itself well to being extended to service *any* requirements, be they proprietary and commercial or simply available. Data accessibility is highly optimized using standard formats including internationally certified open standards (W*S). Although proprietary applications can be built based on World Wind, and proprietary data delivered that leverage World Wind, there is nothing proprietary about the visualization platform itself or the multiple planetary data sets readily available, including global animations of live weather. NASA World Wind is being used by NASA research teams as well as being a formal part of high school and university curriculum. The National Guard uses World Wind for emergency response activities and State governments have incorporated high resolution imagery for GIS management as well as for their cross-agency emergency response activities. The U.S. federal government uses NASA World Wind for a myriad of GIS and security-related issues (NSA, NGA, DOE, FAA, etc.).

The NASA Heliophysics Active Final Archive at the Space Physics Data Facility

NASA Technical Reports Server (NTRS)

McGuire, Robert E.

2012-01-01

The 2009 NASA Heliophysics Science Data Management Policy re-defined and extended the responsibilities of the Space Physics Data Facility (SPDF) project. Building on SPDF's established capabilities, the new policy assigned the role of active "Final Archive" for non-solar NASA Heliophysics data to SPDF. The policy also recognized and formalized the responsibilities of SPDF as a source for critical infrastructure services such as VSPO to the overall Heliophysics Data Environment (HpDE) and as a Center of Excellence for existing SPDF science-enabling services and software including CDAWeb, SSCWeb/4D Orbit Viewer, OMNIweb and CDF. We will focus this talk to the principles, strategies and planned SPDF architecture to effectively and efficiently perform these roles, with special emphasis on how SPDF will ensure the long-term preservation and ongoing online community access to all the data entrusted to SPDF. We will layout our archival philosophy and what we are advocating in our work with NASA missions both current and future, with potential providers of NASA and NASA-relevant archival data, and to make the data and metadata held by SPDF accessible to other systems and services within the overall HpOE. We will also briefly review our current services, their metrics and our current plans and priorities for their evolution.

The NASA Technical Report Server

NASA Astrophysics Data System (ADS)

Nelson, M. L.; Gottlich, G. L.; Bianco, D. J.; Paulson, S. S.; Binkley, R. L.; Kellogg, Y. D.; Beaumont, C. J.; Schmunk, R. B.; Kurtz, M. J.; Accomazzi, A.; Syed, O.

The National Aeronautics and Space Act of 1958 established the National Aeronautics and Space Administration (NASA) and charged it to "provide for the widest practicable and appropriate dissemination of information concerning...its activities and the results thereof". The search for innovative methods to distribute NASA's information led a grass-roots team to create the NASA Technical Report Server (NTRS), which uses the World Wide Web and other popular Internet-based information systems .

The NASA Space Place: A Plethora of Games, Projects, and Fun Facts for Celebrating Astronomy

NASA Astrophysics Data System (ADS)

Leon, N. J.; Fisher, D. K.

2008-12-01

The Space Place is a unique NASA education and public outreach program. It includes a NASA website (spaceplace.nasa.gov) in English and Spanish that targets elementary age children with appealing, content- rich STEM material on space science, Earth science, and technology. The site features science and/or technology content related to, so far, over 40 NASA missions. This overall program, as well as special efforts planned for IYA2009, strongly support many of the objectives of IYA. Some of these are: 1. Stimulate interest in astronomy and science, especially among young people and in audiences not normally reached. 2. Increase scientific awareness. 3. Support and improve formal and informal science education. 4. Provide a contemporary image of science and scientists. 5. Facilitate new astronomy education networks and strengthen existing ones. 6. Improve the gender-balanced representation of scientists at all levels and promote greater involvement of underrepresented groups. The Space Place program has cultivated a large network of community partners (Obj. 5), including museums, libraries, and planetariums, as well as a large network of avocational astronomy societies. We send the community partners monthly mailings of the latest NASA materials for their "NASA Space Place" display boards (Obj. 1, 2, 3, 5). The astronomy societies receive original articles with the latest "insider" news on NASA missions for publication in their newsletters or on their websites (Obj. 2, 5). Through these leveraged partnerships, we reach a large audience of children; parents; formal and informal educators; rural, minority, and otherwise underserved audiences (Obj. 1, 6); and avocational astronomers, many of whom work with children and the general public in the classroom or at special events (Obj. 2, 3). Supporting Obj. 4, are the "Space Place Live" cartoon "talk show" episodes, spaceplace.nasa.gov/en/kids/live. For IYA 2009, we will specifically prepare our partners to plan and carry

Formal System Verification - Extension 2

DTIC Science & Technology

2012-08-08

vision of truly trustworthy systems has been to provide a formally verified microkernel basis. We have previously developed the seL4 microkernel...together with a formal proof (in the theorem prover Isabelle/HOL) of its functional correctness [6]. This means that all the behaviours of the seL4 C...source code are included in the high-level, formal specification of the kernel. This work enabled us to provide further formal guarantees about seL4 , in

A Linguistic Truth-Valued Temporal Reasoning Formalism and Its Implementation

NASA Astrophysics Data System (ADS)

Lu, Zhirui; Liu, Jun; Augusto, Juan C.; Wang, Hui

Temporality and uncertainty are important features of many real world systems. Solving problems in such systems requires the use of formal mechanism such as logic systems, statistical methods or other reasoning and decision-making methods. In this paper, we propose a linguistic truth-valued temporal reasoning formalism to enable the management of both features concurrently using a linguistic truth valued logic and a temporal logic. We also provide a backward reasoning algorithm which allows the answering of user queries. A simple but realistic scenario in a smart home application is used to illustrate our work.

NASA spinoffs to public service

NASA Technical Reports Server (NTRS)

Ault, L. A.; Cleland, J. G.

1989-01-01

The National Aeronautics and Space Administration (NASA) Technology Utilization (TU) Division of the Office of Commercial Programs has been quite successful in directing the transfer to technology into the public sector. NASA developments of particular interest have been those in the areas of aerodynamics and aviation transport, safety, sensors, electronics and computing, and satellites and remote sensing. NASA technology has helped law enforcement, firefighting, public transportation, education, search and rescue, and practically every other sector of activity serving the U.S. public. NASA works closely with public service agencies and associations, especially those serving local needs of citizens, to expedite technology transfer benefits. A number of examples exist to demonstrate the technology transfer method and opportunities of NASA spinoffs to public service.

Taxonomy of Teaching Methods and Teaching Forms for Youth in Non-Formal Education in the National Youth Council of Slovenia

ERIC Educational Resources Information Center

Miloševic Zupancic, Vesna

2018-01-01

Research from the field of non-formal education (NFE) in youth work emphasises the central role of experiential learning and learning in groups. The present paper aims to research teaching methods and teaching forms in NFE in youth work. The research sought to answer the following research questions: 'What teaching forms can be found in NFE for…

Symbols on Formal Groups

NASA Astrophysics Data System (ADS)

Vostokov, S. V.

1982-04-01

The theory of a continuous Steinberg symbol in a local field is generalized to formal commutative groups. For Lubin-Tate groups, a universal symbol is constructed in explicit form, and it is shown that the module of values of an arbitrary symbol imbeds into the group of points of the formal group. By means of this theory of symbols a new approach is given to obtaining an explicit form for the Hilbert norm residue symbol on Lubin-Tate formal groups. Bibliography: 10 titles.

48 CFR 1815.7001 - NASA Ombudsman Program.

Code of Federal Regulations, 2013 CFR

2013-10-01

... 48 Federal Acquisition Regulations System 6 2013-10-01 2013-10-01 false NASA Ombudsman Program... ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES CONTRACTING BY NEGOTIATION Ombudsman 1815.7001 NASA Ombudsman Program. NASA's implementation of an ombudsman program is in NPR 5101.33, Procurement Advocacy...

48 CFR 1815.7001 - NASA Ombudsman Program.

Code of Federal Regulations, 2014 CFR

2014-10-01

... 48 Federal Acquisition Regulations System 6 2014-10-01 2014-10-01 false NASA Ombudsman Program... ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES CONTRACTING BY NEGOTIATION Ombudsman 1815.7001 NASA Ombudsman Program. NASA's implementation of an ombudsman program is in NPR 5101.33, Procurement Advocacy...

48 CFR 1815.7001 - NASA Ombudsman Program.

Code of Federal Regulations, 2011 CFR

2011-10-01

... 48 Federal Acquisition Regulations System 6 2011-10-01 2011-10-01 false NASA Ombudsman Program... ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES CONTRACTING BY NEGOTIATION Ombudsman 1815.7001 NASA Ombudsman Program. NASA's implementation of an ombudsman program is in NPR 5101.33, Procurement Advocacy...

48 CFR 1815.7001 - NASA Ombudsman Program.

Code of Federal Regulations, 2012 CFR

2012-10-01

... 48 Federal Acquisition Regulations System 6 2012-10-01 2012-10-01 false NASA Ombudsman Program... ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES CONTRACTING BY NEGOTIATION Ombudsman 1815.7001 NASA Ombudsman Program. NASA's implementation of an ombudsman program is in NPR 5101.33, Procurement Advocacy...

48 CFR 1815.7001 - NASA Ombudsman Program.

Code of Federal Regulations, 2010 CFR

2010-10-01

... 48 Federal Acquisition Regulations System 6 2010-10-01 2010-10-01 true NASA Ombudsman Program... ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES CONTRACTING BY NEGOTIATION Ombudsman 1815.7001 NASA Ombudsman Program. NASA's implementation of an ombudsman program is in NPR 5101.33, Procurement Advocacy...

NASA's New Science Education and Public Outreach Forums: Bringing Communities and Resources Together to Increase Effectiveness and Sustainability

NASA Astrophysics Data System (ADS)

Smith, Denise A.; Mendez, B.; Shipp, S.; Schwerin, T.; Stockman, S.; Cooper, L. P.; Sharma, M.

2010-01-01

Scientists, engineers, educators, and public outreach professionals have a rich history of creatively using NASA's pioneering scientific discoveries and technology to engage and educate youth and adults nationwide in core science, technology, engineering, and mathematics topics. We introduce four new Science Education and Public Outreach Forums that will work in partnership with the community and NASA's Science Mission Directorate (SMD) to ensure that current and future SMD-funded education and public outreach (E/PO) activities form a seamless whole, with easy entry points for general public, students, K-12 formal and informal science educators, faculty, scientists, engineers, and E/PO professionals alike. The new Science Education and Public Outreach Forums support the astrophysics, heliophysics, planetary and Earth science divisions of NASA SMD in three core areas: 1) E/PO community engagement and development activities will provide clear paths of involvement for scientists and engineers interested - or potentially interested - in participating in SMD-funded E/PO activities. Collaborations with scientists and engineers are vital for infusing current, accurate SMD mission and research findings into educational products and activities. Forum activities will also yield readily accessible information on effective E/PO strategies, resources, and expertise; context for individual E/PO activities; and opportunities for collaboration. 2) A rigorous analysis of SMD-funded K-12 formal, informal, and higher education products and activities will help the community and SMD to understand how the existing collection supports education standards and audience needs, and to strategically identify areas of opportunity for new materials and activities. 3) Finally, a newly convened Coordinating Committee will work across the four SMD science divisions to address systemic issues and integrate related activities. By supporting the NASA E/PO community and facilitating coordination of E

The NASA SMD Science Education and Public Outreach Forums: Engaging Scientists in NASA Education and Public Outreach

NASA Astrophysics Data System (ADS)

Smith, Denise A.; Peticolas, L.; Schwerin, T.; Shipp, S.

2014-01-01

The NASA Science Mission Directorate (SMD) Education and Public Outreach (E/PO) program provides a direct return on the public’s investment in NASA’s science missions and research programs through a comprehensive suite of educational resources and opportunities for students, educators, and the public. Four Science Education and Public Outreach Forums work with SMD-funded missions, research programs, and grantees to organize individual E/PO activities into a coordinated, effective, and efficient nationwide effort, with easy entry points for scientists, educators, and the public. We outline the Forums’ role in 1) facilitating communication and collaboration among SMD E/PO programs, scientists, and educators; 2) supporting utilization of best practices and educational research; 3) creating clear paths of involvement for scientists interested in SMD E/PO; and, 4) enabling efficient and effective use of NASA content and education products. Our work includes a cross-Forum collaboration to inventory existing SMD education materials; identify and analyze gaps; and interconnect and organize materials in an accessible manner for multiple audiences. The result is NASAWavelength.org, a one-stop-shop for all NASA SMD education products, including tools to help users identify resources based upon their needs and national education standards. The Forums have also collaborated with the SMD E/PO community to provide a central point of access to metrics, evaluation findings, and impacts for SMD-funded E/PO programs (http://smdepo.org/page/5324). We also present opportunities for the astronomy community to participate in collaborations supporting NASA SMD efforts in the K - 12 Formal Education, Informal Education and Outreach, Higher Education and Research Scientist communities. See Bartolone et al., Lawton et al., Meinke et al., and Buxner et al. (this conference), respectively, to learn about Forum resources and opportunities specific to each of these communities.

NASA Handbook for Models and Simulations: An Implementation Guide for NASA-STD-7009

NASA Technical Reports Server (NTRS)

Steele, Martin J.

2013-01-01

The purpose of this Handbook is to provide technical information, clarification, examples, processes, and techniques to help institute good modeling and simulation practices in the National Aeronautics and Space Administration (NASA). As a companion guide to NASA-STD- 7009, Standard for Models and Simulations, this Handbook provides a broader scope of information than may be included in a Standard and promotes good practices in the production, use, and consumption of NASA modeling and simulation products. NASA-STD-7009 specifies what a modeling and simulation activity shall or should do (in the requirements) but does not prescribe how the requirements are to be met, which varies with the specific engineering discipline, or who is responsible for complying with the requirements, which depends on the size and type of project. A guidance document, which is not constrained by the requirements of a Standard, is better suited to address these additional aspects and provide necessary clarification. This Handbook stems from the Space Shuttle Columbia Accident Investigation (2003), which called for Agency-wide improvements in the "development, documentation, and operation of models and simulations"' that subsequently elicited additional guidance from the NASA Office of the Chief Engineer to include "a standard method to assess the credibility of the models and simulations."2 General methods applicable across the broad spectrum of model and simulation (M&S) disciplines were sought to help guide the modeling and simulation processes within NASA and to provide for consistent reporting ofM&S activities and analysis results. From this, the standardized process for the M&S activity was developed. The major contents of this Handbook are the implementation details of the general M&S requirements ofNASA-STD-7009, including explanations, examples, and suggestions for improving the credibility assessment of an M&S-based analysis.

Open Rotor Noise Prediction Methods at NASA Langley- A Technology Review

NASA Technical Reports Server (NTRS)

Farassat, F.; Dunn, Mark H.; Tinetti, Ana F.; Nark, Douglas M.

2009-01-01

Open rotors are once again under consideration for propulsion of the future airliners because of their high efficiency. The noise generated by these propulsion systems must meet the stringent noise standards of today to reduce community impact. In this paper we review the open rotor noise prediction methods available at NASA Langley. We discuss three codes called ASSPIN (Advanced Subsonic-Supersonic Propeller Induced Noise), FW - Hpds (Ffowcs Williams-Hawkings with penetrable data surface) and the FSC (Fast Scattering Code). The first two codes are in the time domain and the third code is a frequency domain code. The capabilities of these codes and the input data requirements as well as the output data are presented. Plans for further improvements of these codes are discussed. In particular, a method based on equivalent sources is outlined to get rid of spurious signals in the FW - Hpds code.

Guidelines for NASA Missions to Engage the User Community as a Part of the Mission Life Cycle

NASA Astrophysics Data System (ADS)

Escobar, V. M.; Friedl, L.; Bonniksen, C. K.

2017-12-01

NASA continues to improve the Earth Science Directorate in the areas of thematic integration, stakeholder feedback and Project Applications Program tailoring for missions to transfer knowledge between scientists and projects. The integration of application themes and the implementation of application science activities in flight projects have evolved to formally include user feedback and stakeholder integration. NASA's new Flight Applied Science Program Guidelines are designed to bridge NASA Earth Science Directorates in Flight, Applied Sciences and Research and Development by agreeing to integrate the user community into mission life cycles. Thus science development and science applications will guide all new instruments launched by NASAs ESD. The continued integration with the user community has enabled socio-economic considerations into NASA Earth Science projects to advance significantly. Making users a natural part of mission science leverages future socio-economic impact research and provides a platform for innovative and more actionable product to be used in decision support systems by society. This presentation will give an overview of the new NASA Guidelines and provide samples that demonstrate how the user community can be a part of NASA mission designs.

Application of Fast Multipole Methods to the NASA Fast Scattering Code

NASA Technical Reports Server (NTRS)

Dunn, Mark H.; Tinetti, Ana F.

2008-01-01

The NASA Fast Scattering Code (FSC) is a versatile noise prediction program designed to conduct aeroacoustic noise reduction studies. The equivalent source method is used to solve an exterior Helmholtz boundary value problem with an impedance type boundary condition. The solution process in FSC v2.0 requires direct manipulation of a large, dense system of linear equations, limiting the applicability of the code to small scales and/or moderate excitation frequencies. Recent advances in the use of Fast Multipole Methods (FMM) for solving scattering problems, coupled with sparse linear algebra techniques, suggest that a substantial reduction in computer resource utilization over conventional solution approaches can be obtained. Implementation of the single level FMM (SLFMM) and a variant of the Conjugate Gradient Method (CGM) into the FSC is discussed in this paper. The culmination of this effort, FSC v3.0, was used to generate solutions for three configurations of interest. Benchmarking against previously obtained simulations indicate that a twenty-fold reduction in computational memory and up to a four-fold reduction in computer time have been achieved on a single processor.

Connecting Formal and Informal Learning Experiences

ERIC Educational Resources Information Center

O'Mahony, Timothy Kieran

2010-01-01

The learning study reports on part of a larger project being lead by the author. In this dissertation I explore one goal of this project--to understand effects on student learning outcomes as a function of using different methods for connecting out-of-school experiential learning with formal school-based instruction. There is a long history of…

NASA Publications Guide for Authors

NASA Technical Reports Server (NTRS)

1999-01-01

Publication of scientific and technical information (STI) is one of the responsibilities of NASA as a Government Agency. The National Aeronautics and Space Act of 1958 established a requirement for NASA to provide "the widest practicable and appropriate dissemination of information concerning its activities and the results thereof." Persons engaged in NASA-funded or NASA-sponsored research and development and related efforts are therefore required to publish the results of their work in the NASA STI series or through other externally accessible channels. An Agency-wide committee of publications professionals prepared the standards and conventions presented in this guide for authors. Section 2 of this guide presents descriptions of each type of report in the NASA STI Report Series and briefly discusses the applicable production methods and appropriate dissemination of these reports. Section 3 discusses professional and ethical concerns. Section 4 provides recommended standards for document format, makeup, and organization. Section 5 presents miscellaneous preparation concerns.

Implementation of a method for calculating temperature-dependent resistivities in the KKR formalism

NASA Astrophysics Data System (ADS)

Mahr, Carsten E.; Czerner, Michael; Heiliger, Christian

2017-10-01

We present a method to calculate the electron-phonon induced resistivity of metals in scattering-time approximation based on the nonequilibrium Green's function formalism. The general theory as well as its implementation in a density-functional theory based Korringa-Kohn-Rostoker code are described and subsequently verified by studying copper as a test system. We model the thermal expansion by fitting a Debye-Grüneisen curve to experimental data. Both the electronic and vibrational structures are discussed for different temperatures, and employing a Wannier interpolation of these quantities we evaluate the scattering time by integrating the electron linewidth on a triangulation of the Fermi surface. Based thereupon, the temperature-dependent resistivity is calculated and found to be in good agreement with experiment. We show that the effect of thermal expansion has to be considered in the whole calculation regime. Further, for low temperatures, an accurate sampling of the Fermi surface becomes important.

Software Tools for Formal Specification and Verification of Distributed Real-Time Systems.

DTIC Science & Technology

1997-09-30

set of software tools for specification and verification of distributed real time systems using formal methods. The task of this SBIR Phase II effort...to be used by designers of real - time systems for early detection of errors. The mathematical complexity of formal specification and verification has

The AEC-NASA Nuclear Rocket Program

NASA Astrophysics Data System (ADS)

Finger, Harold B.

2002-01-01

The early days and years of the National Aeronautics and Space Administration (NASA), its assigned missions its organization and program development, provided major opportunities for still young technical people to participate in and contribute to making major technological advances and to broaden and grow their technical, management, and leadership capabilities for their and our country's and the world's benefit. Being one of those fortunate beneficiaries while I worked at NASA's predecessor, the National Advisory Committee for Aeronautics (NACA) Lewis Flight Propulsion Laboratory in Cleveland and then when I was transferred to the NASA Headquarters on October 1, 1958, the day NASA was formally activated, this paper will describe some of my experiences and their significant results, including the personal benefits I derived from that fabulous period of our major national accomplishments. Although I had a broad range of responsibility in NASA which changed and grew over time, I concentrate my discussion in this paper on those activities conducted by NASA and the Atomic Energy Committee (AEC) in the development of the technology of nuclear rocket propulsion to enable the performance of deep space missions. There are two very related but distinct elements of this memoir. One relates to NASA's and the U.S. missions in those very early years and some of the technical and administrative elements as well as the political influences and interagency activities, including primarily the AEC and NASA, as well as diverse industrial and governmental capabilities and activities required to permit the new NASA to accomplish its assigned mission responsibilities. The other concerns the more specific technical and management assignments used to achieve the program's major technological successes. I will discuss first, how and why I was assigned to manage those nuclear rocket propulsion program activities and, then, how we achieved our very significant and successful program

[How to write an article: formal aspects].

PubMed

Corral de la Calle, M A; Encinas de la Iglesia, J

2013-06-01

Scientific research and the publication of the results of the studies go hand in hand. Exquisite research methods can only be adequately reflected in formal publication with the optimum structure. To ensure the success of this process, it is necessary to follow orderly steps, including selecting the journal in which to publish and following the instructions to authors strictly as well as the guidelines elaborated by diverse societies of editors and other institutions. It is also necessary to structure the contents of the article in a logical and attractive way and to use an accurate, clear, and concise style of language. Although not all the authors are directly involved in the actual writing, elaborating a scientific article is a collective undertaking that does not finish until the article is published. This article provides practical advice about formal and not-so-formal details to take into account when writing a scientific article as well as references that will help readers find more information in greater detail. Copyright © 2012 SERAM. Published by Elsevier Espana. All rights reserved.

A Formal Valuation Framework for Emotions and Their Control.

PubMed

Huys, Quentin J M; Renz, Daniel

2017-09-15

Computational psychiatry aims to apply mathematical and computational techniques to help improve psychiatric care. To achieve this, the phenomena under scrutiny should be within the scope of formal methods. As emotions play an important role across many psychiatric disorders, such computational methods must encompass emotions. Here, we consider formal valuation accounts of emotions. We focus on the fact that the flexibility of emotional responses and the nature of appraisals suggest the need for a model-based valuation framework for emotions. However, resource limitations make plain model-based valuation impossible and require metareasoning strategies to apportion cognitive resources adaptively. We argue that emotions may implement such metareasoning approximations by restricting the range of behaviors and states considered. We consider the processes that guide the deployment of the approximations, discerning between innate, model-free, heuristic, and model-based controllers. A formal valuation and metareasoning framework may thus provide a principled approach to examining emotions. Copyright © 2017 Society of Biological Psychiatry. Published by Elsevier Inc. All rights reserved.

NASA Update

NASA Image and Video Library

2010-04-08

"NASA Update" program with NASA Administrator Charles Bolden, NASA Deputy Administrator Lori Garver and NASA Acting Asistant Administrator for Public Affairs Bob Jacobs as moderator, NASA Headquarters, Thursday, April 8, 2010 in Washington. Photo Credit: (NASA/Bill Ingalls)

OSI in the NASA science internet: An analysis

NASA Technical Reports Server (NTRS)

Nitzan, Rebecca

1990-01-01

The Open Systems Interconnection (OSI) protocol suite is a result of a world-wide effort to develop international standards for networking. OSI is formalized through the International Organization for Standardization (ISO) and the International Electrotechnical Commission (IEC). The goal of OSI is to provide interoperability between network products without relying on one particular vendor, and to do so on a multinational basis. The National Institute for Standards and Technology (NIST) has developed a Government OSI Profile (GOSIP) that specified a subset of the OSI protocols as a Federal Information Processing Standard (FIPS 146). GOSIP compatibility has been adopted as the direction for all U.S. government networks. OSI is extremely diverse, and therefore adherence to a profile will facilitate interoperability within OSI networks. All major computer vendors have indicated current or future support of GOSIP-compliant OSI protocols in their products. The NASA Science Internet (NSI) is an operational network, serving user requirements under NASA's Office of Space Science and Applications. NSI consists of the Space Physics Analysis Network (SPAN) that uses the DECnet protocols and the NASA Science Network (NSN) that uses TCP/IP protocols. The NSI Project Office is currently working on an OSI integration analysis and strategy. A long-term goal is to integrate SPAN and NSN into one unified network service, using a full OSI protocol suite, which will support the OSSA user community.

Combining Archetypes, Ontologies and Formalization Enables Automated Computation of Quality Indicators.

PubMed

Legaz-García, María Del Carmen; Dentler, Kathrin; Fernández-Breis, Jesualdo Tomás; Cornet, Ronald

2017-01-01

ArchMS is a framework that represents clinical information and knowledge using ontologies in OWL, which facilitates semantic interoperability and thereby the exploitation and secondary use of clinical data. However, it does not yet support the automated assessment of quality of care. CLIF is a stepwise method to formalize quality indicators. The method has been implemented in the CLIF tool which supports its users in generating computable queries based on a patient data model which can be based on archetypes. To enable the automated computation of quality indicators using ontologies and archetypes, we tested whether ArchMS and the CLIF tool can be integrated. We successfully automated the process of generating SPARQL queries from quality indicators that have been formalized with CLIF and integrated them into ArchMS. Hence, ontologies and archetypes can be combined for the execution of formalized quality indicators.

Formalized Epistemology, Logic, and Grammar

NASA Astrophysics Data System (ADS)

Bitbol, Michel

The task of a formal epistemology is defined. It appears that a formal epistemology must be a generalization of "logic" in the sense of Wittgenstein's Tractatus. The generalization is required because, whereas logic presupposes a strict relation between activity and language, this relation may be broken in some domains of experimental enquiry (e.g., in microscopic physics). However, a formal epistemology should also retain a major feature of Wittgenstein's "logic": It must not be a discourse about scientific knowledge, but rather a way of making manifest the structures usually implicit in knowledge-gaining activity. This strategy is applied to the formalism of quantum mechanics.

Physics in NASA Exploration

NASA Technical Reports Server (NTRS)

O'Callaghan, Fred

2004-01-01

The primary focus of the workshop was NASA's new concentration on sending crewed missions to the Moon by 2020, and then on to Mars and beyond. Several speakers, including JPL s Fred O Callaghan and NASA's Mark Lee, broached the problem that there is now a serious reduction of capability to perform experiments in the ISS, or to fly significant mass in microgravity by other means. By 2010, the shuttle fleet will be discontinued and Russian craft will provide the only access to the ISS. O Callaghan stated that the Fundamental Physics budget is being reduced by 70%. LTMPF and LCAP are slated for termination. However, ground-based experiments are continuing to be funded at present, and it will be possible to compete for $80-90 million in new money from the Human Research Initiative (HRI). The new program thrust is for exploration, not fundamental physics. Fundamental, we were told by Lee, does not ring well in Washington these days. Investigators were advised to consider how their work can benefit missions to the Moon and Mars. Work such as that regarding atomic clocks is looked upon with favor, for example, because it is considered important to navigation and planetary GPS. Mark Lee stressed that physicists must convey to NASA senior management that they are able and willing to contribute to the new exploration research programs. The new mentality must be we deliver products, not do research. This program needs to be able to say that it is doing at least 50% exploration-related research. JPL s Ulf Israelsson discussed the implications to OBPR, which will deliver methods and technology to assure human health and performance in extraterrestrial settings. The enterprise will provide advanced life-support systems and technology that are reliable, capable, simpler, less massive, smaller, and energy-efficient, and it may offer other necessary expertise in areas such as low-gravity behavior. Like Dr. Lee, he stated that the focus must be on products, not research. While there

Formal verification of AI software

NASA Technical Reports Server (NTRS)

Rushby, John; Whitehurst, R. Alan

1989-01-01

The application of formal verification techniques to Artificial Intelligence (AI) software, particularly expert systems, is investigated. Constraint satisfaction and model inversion are identified as two formal specification paradigms for different classes of expert systems. A formal definition of consistency is developed, and the notion of approximate semantics is introduced. Examples are given of how these ideas can be applied in both declarative and imperative forms.

Comparing NASA and ESA Cost Estimating Methods for Human Missions to Mars

NASA Technical Reports Server (NTRS)

Hunt, Charles D.; vanPelt, Michel O.

2004-01-01

To compare working methodologies between the cost engineering functions in NASA Marshall Space Flight Center (MSFC) and ESA European Space Research and Technology Centre (ESTEC), as well as to set-up cost engineering capabilities for future manned Mars projects and other studies which involve similar subsystem technologies in MSFC and ESTEC, a demonstration cost estimate exercise was organized. This exercise was a direct way of enhancing not only cooperation between agencies but also both agencies commitment to credible cost analyses. Cost engineers in MSFC and ESTEC independently prepared life-cycle cost estimates for a reference human Mars project and subsequently compared the results and estimate methods in detail. As a non-sensitive, public domain reference case for human Mars projects, the Mars Direct concept was chosen. In this paper the results of the exercise are shown; the differences and similarities in estimate methodologies, philosophies, and databases between MSFC and ESTEC, as well as the estimate results for the Mars Direct concept. The most significant differences are explained and possible estimate improvements identified. In addition, the Mars Direct plan and the extensive cost breakdown structure jointly set-up by MSFC and ESTEC for this concept are presented. It was found that NASA applied estimate models mainly based on historic Apollo and Space Shuttle cost data, taking into account the changes in technology since then. ESA used models mostly based on European satellite and launcher cost data, taking into account the higher equipment and testing standards for human space flight. Most of NASA's and ESA s estimates for the Mars Direct case are comparable, but there are some important, consistent differences in the estimates for: 1) Large Structures and Thermal Control subsystems; 2) System Level Management, Engineering, Product Assurance and Assembly, Integration and Test/Verification activities; 3) Mission Control; 4) Space Agency Program Level

Formal Solutions for Polarized Radiative Transfer. III. Stiffness and Instability

NASA Astrophysics Data System (ADS)

Janett, Gioele; Paganini, Alberto

2018-04-01

Efficient numerical approximation of the polarized radiative transfer equation is challenging because this system of ordinary differential equations exhibits stiff behavior, which potentially results in numerical instability. This negatively impacts the accuracy of formal solvers, and small step-sizes are often necessary to retrieve physical solutions. This work presents stability analyses of formal solvers for the radiative transfer equation of polarized light, identifies instability issues, and suggests practical remedies. In particular, the assumptions and the limitations of the stability analysis of Runge–Kutta methods play a crucial role. On this basis, a suitable and pragmatic formal solver is outlined and tested. An insightful comparison to the scalar radiative transfer equation is also presented.

Determination of Tolerance to Internal Shorts and Its Screening in Lithium-ion Cells NASA - JSC Method

NASA Technical Reports Server (NTRS)

Jeevarajan, Judith

2009-01-01

This slide presentation reviews the method developed by the NASA Johnson Space Center (JSC) to determine tolerances to internal shorts and screening for problems in commercial off the shelf (COTS) Lithium-ion batteries. The test apparatus is shown and several examples of the usage and results of the test are discussed.

NASA System Engineering Design Process

NASA Technical Reports Server (NTRS)

Roman, Jose

2011-01-01

This slide presentation reviews NASA's use of systems engineering for the complete life cycle of a project. Systems engineering is a methodical, disciplined approach for the design, realization, technical management, operations, and retirement of a system. Each phase of a NASA project is terminated with a Key decision point (KDP), which is supported by major reviews.

NASA #801 and NASA 7 on ramp

NASA Technical Reports Server (NTRS)

1997-01-01

NASA N801NA and NASA 7 together on the NASA Dryden ramp. The Beechcraft Beech 200 Super KingAir aircraft N7NA, known as NASA 7, has been a support aircraft for many years, flying 'shuttle' missions to Ames Research Center. It once flew from the Jet Propulsion Laboratory and back each day but now (2001) flies between the Dryden Flight Research Center and Ames. A second Beechcraft Beech 200 Super King Air, N701NA, redesignated N801NA, transferred to Dryden on 3 Oct. 1997 and is used for research missions but substitutes for NASA 7 on shuttle missions when NASA 7 is not available.

Spinor helicity methods in high-energy factorization: Efficient momentum-space calculations in the Color Glass Condensate formalism

NASA Astrophysics Data System (ADS)

Ayala, Alejandro; Hentschinski, Martin; Jalilian-Marian, Jamal; Tejeda-Yeomans, Maria Elena

2017-07-01

We use the spinor helicity formalism to calculate the cross section for production of three partons of a given polarization in Deep Inelastic Scattering (DIS) off proton and nucleus targets at small Bjorken x. The target proton or nucleus is treated as a classical color field (shock wave) from which the produced partons scatter multiple times. We reported our result for the final expression for the production cross section and studied the azimuthal angular correlations of the produced partons in [1]. Here we provide the full details of the calculation of the production cross section using the spinor helicity methods.

Indigenous Knowledge and Education from the Quechua Community to School: Beyond the Formal/Non-Formal Dichotomy

ERIC Educational Resources Information Center

Sumida Huaman, Elizabeth; Valdiviezo, Laura Alicia

2014-01-01

In this article, we propose to approach Indigenous education beyond the formal/non-formal dichotomy. We argue that there is a critical need to conscientiously include Indigenous knowledge in education processes from the school to the community; particularly, when formal systems exclude Indigenous cultures and languages. Based on ethnographic…

The Scientific and Engineering Student Internship (SESI) Program at NASA's GSFC

NASA Astrophysics Data System (ADS)

Bruhweiler, F.; Verner, E.; Rabin, D. M.

2011-12-01

Through our Scientific and Engineering Student Internship (SESI) program we have provided exceptional research opportunities for undergraduate and graduate students in one of the world's premier research centers dedicated to the Sun and its heliosphere, the Heliophysics Science Division at NASA/Goddard Space Flight Center. NASA/GSFC and the NSF/REU program have funded this activity jointly. These opportunities combine the advantages of the stimulating, multi-disciplinary, environment of a NASA laboratory with the guidance provided by researchers who are, in addition, committed to education and the encouragement of women, under-represented minorities, and students with disabilities. Opportunities also exist for non-U.S. citizens as well. Moreover, the surrounding Washington, DC area provides a variety of social and educational activities for our participating students. Our 19 years of experience has served as an effective catalyst, enabling us to establish a formal program for students interested in Solar and Space Physics at NASA and to develop more NASA-funded opportunities for students, in addition to those funded by NSF/REU awards. This has allowed us to present a combined NSF/REU and NASA-funded program for undergraduates at NASA/GSFC. This synergistic program exposes our student interns to a very wide range of projects and ideas, normally unavailable in other programs. We have had roughly 300 students (about 1/2 being supported by NSF) actively participate in over 200 different research opportunities. These research projects have spanned the spectrum, ranging from theoretical modeling associated with space weather, developing instrumentation for space missions, analysis of spacecraft data, including 'hands-on' experience with sounding rockets and working in the clean environs of GSFC's Detector Development Laboratory. Although SESI is largely a summer program, a number of students, often through other funding sources, continue their research projects during

Enhancing the Intercultural Effectiveness of Exchange Programmes: Formal and Non-Formal Educational Interventions

ERIC Educational Resources Information Center

Almeida, Joana; Fantini, Alvino E.; Simões, Ana Raquel; Costa, Nilza

2016-01-01

This paper examines how the addition of intercultural interventions carried out throughout European credit-bearing exchange programmes can enhance sojourners' development of intercultural competencies, and it explores how both formal and non-formal pedagogical interventions may be designed and implemented. Such interventions were conducted at a…

Formalizing Evaluation Procedures for Marketing Faculty Research Performance.

ERIC Educational Resources Information Center

McDermott, Dennis R.; And Others

1994-01-01

Results of a national survey of marketing department heads (n=142) indicate that few marketing departments have formalized the development and communication of research performance standards to faculty. Guidelines and methods to accomplish those procedures most efficiently were proposed. (Author/JOW)

Concepts of formal concept analysis

NASA Astrophysics Data System (ADS)

Žáček, Martin; Homola, Dan; Miarka, Rostislav

2017-07-01

The aim of this article is apply of Formal Concept Analysis on concept of world. Formal concept analysis (FCA) as a methodology of data analysis, information management and knowledge representation has potential to be applied to a verity of linguistic problems. FCA is mathematical theory for concepts and concept hierarchies that reflects an understanding of concept. Formal concept analysis explicitly formalizes extension and intension of a concept, their mutual relationships. A distinguishing feature of FCA is an inherent integration of three components of conceptual processing of data and knowledge, namely, the discovery and reasoning with concepts in data, discovery and reasoning with dependencies in data, and visualization of data, concepts, and dependencies with folding/unfolding capabilities.

NASA automatic subject analysis technique for extracting retrievable multi-terms (NASA TERM) system

NASA Technical Reports Server (NTRS)

Kirschbaum, J.; Williamson, R. E.

1978-01-01

Current methods for information processing and retrieval used at the NASA Scientific and Technical Information Facility are reviewed. A more cost effective computer aided indexing system is proposed which automatically generates print terms (phrases) from the natural text. Satisfactory print terms can be generated in a primarily automatic manner to produce a thesaurus (NASA TERMS) which extends all the mappings presently applied by indexers, specifies the worth of each posting term in the thesaurus, and indicates the areas of use of the thesaurus entry phrase. These print terms enable the computer to determine which of several terms in a hierarchy is desirable and to differentiate ambiguous terms. Steps in the NASA TERMS algorithm are discussed and the processing of surrogate entry phrases is demonstrated using four previously manually indexed STAR abstracts for comparison. The simulation shows phrase isolation, text phrase reduction, NASA terms selection, and RECON display.

NASA World Wind, Open Source 4D Geospatial Visualization Platform: *.NET & Java* for EDUCATION

NASA Astrophysics Data System (ADS)

Hogan, P.; Kuehnel, F.

2006-12-01

NASA World Wind has only one goal, to provide the maximum opportunity for geospatial information to be experienced, be it education, science, research, business, or government. The benefits to understanding for information delivered in the context of its 4D virtual reality are extraordinary. The NASA World Wind visualization platform is open source and therefore lends itself well to being extended to service *any* requirements, be they proprietary and commercial or simply available. Data accessibility is highly optimized using standard formats including internationally certified open standards (W*S). Although proprietary applications can be built based on World Wind, and proprietary data delivered that leverage World Wind, there is nothing proprietary about the visualization platform itself or the multiple planetary data sets readily available, including global animations of live weather. NASA World Wind is being used by NASA research teams as well as being a formal part of high school and university curriculum. The National Guard uses World Wind for emergency response activities and State governments have incorporated high resolution imagery for GIS management as well as for their cross-agency emergency response activities. The U.S. federal government uses NASA World Wind for a myriad of GIS and security-related issues (NSA, NGA, DOE, FAA, etc.).

NASA Update

NASA Image and Video Library

2011-02-15

NASA Administrator Charles F. Bolden Jr., answers questions during a NASA Update on, Tuesday, Feb. 15, 2011, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator and NASA Deputy Administrator Lori Garver took the time discuss the agency’s fiscal year 2012 budget request and to take questions from employees. Photo Credit: (NASA/Bill Ingalls)

Development of an Outreach Program for NASA: "NASA Ambassadors"

NASA Technical Reports Server (NTRS)

Lebo, George R.

1996-01-01

It is widely known that the average American citizen has either no idea or the wrong impression of what NASA is doing. The most common impression is that NASA's sole mission is to build and launch spacecraft and that the everyday experience of the common citizen would be impacted very little if NASA failed to exist altogether. Some feel that most of NASA's efforts are much too expensive and that the money would be better used on other efforts. Others feel that most of NASA's efforts either fail altogether or fail to meet their original objectives. Yet others feel that NASA is so mired in bureaucracy that it is no longer able to function. The goal of the NASA Ambassadors Program (NAP) is to educate the general populace as to what NASA's mission and goals actually are, to re-excite the "man on the street" with NASA's discoveries and technologies, and to convince him that NASA really does impact his everyday experience and that the economy of the U.S. is very dependent on NASA-type research. Each of the NASA centers currently run a speakers bureau through its Public Affairs Office (PAO). The speakers, NASA employees, are scheduled on an "as available" status and their travel is paid by NASA. However, there are only a limited number of them and their message may be regarded as being somewhat biased as they are paid by NASA. On the other hand, there are many members of NASA's summer programs which come from all areas of the country. Most of them not only believe that NASA's mission is important but are willing and able to articulate it to others. Furthermore, in the eyes of the public, they are probably more effective as ambassadors for NASA than are the NASA employees, as they do not derive their primary funding from it. Therefore it was decided to organize materials for them to use in presentations to general audiences in their home areas. Each person who accepted these materials was to be called a "NASA Ambassador".

Computer aided indexing at NASA

NASA Technical Reports Server (NTRS)

Buchan, Ronald L.

1987-01-01

The application of computer technology to the construction of the NASA Thesaurus and in NASA Lexical Dictionary development is discussed in a brief overview. Consideration is given to the printed and online versions of the Thesaurus, retrospective indexing, the NASA RECON frequency command, demand indexing, lists of terms by category, and the STAR and IAA annual subject indexes. The evolution of computer methods in the Lexical Dictionary program is traced, from DOD and DOE subject switching to LCSH machine-aided indexing and current techniques for handling natural language (e.g., the elimination of verbs to facilitate breakdown of sentences into words and phrases).

Viscous warm inflation: Hamilton-Jacobi formalism

NASA Astrophysics Data System (ADS)

Akhtari, L.; Mohammadi, A.; Sayar, K.; Saaidi, Kh.

2017-04-01

Using Hamilton-Jacobi formalism, the scenario of warm inflation with viscous pressure is considered. The formalism gives a way of computing the slow-rolling parameter without extra approximation, and it is well-known as a powerful method in cold inflation. The model is studied in detail for three different cases of the dissipation and bulk viscous pressure coefficients. In the first case where both coefficients are taken as constant, it is shown that the case could not portray warm inflationary scenario compatible with observational data even it is possible to restrict the model parameters. For other cases, the results shows that the model could properly predicts the perturbation parameters in which they stay in perfect agreement with Planck data. As a further argument, r -ns and αs -ns are drown that show the acquired result could stand in acceptable area expressing a compatibility with observational data.

47 CFR 8.12 - Formal complaints.

Code of Federal Regulations, 2014 CFR

2014-10-01

... 47 Telecommunication 1 2014-10-01 2014-10-01 false Formal complaints. 8.12 Section 8.12 Telecommunication FEDERAL COMMUNICATIONS COMMISSION GENERAL PRESERVING THE OPEN INTERNET § 8.12 Formal complaints. Any person may file a formal complaint alleging a violation of the rules in this part. ...

47 CFR 8.12 - Formal complaints.

Code of Federal Regulations, 2013 CFR

2013-10-01

... 47 Telecommunication 1 2013-10-01 2013-10-01 false Formal complaints. 8.12 Section 8.12 Telecommunication FEDERAL COMMUNICATIONS COMMISSION GENERAL PRESERVING THE OPEN INTERNET § 8.12 Formal complaints. Any person may file a formal complaint alleging a violation of the rules in this part. ...

47 CFR 8.12 - Formal complaints.

Code of Federal Regulations, 2012 CFR

2012-10-01

... 47 Telecommunication 1 2012-10-01 2012-10-01 false Formal complaints. 8.12 Section 8.12 Telecommunication FEDERAL COMMUNICATIONS COMMISSION GENERAL PRESERVING THE OPEN INTERNET § 8.12 Formal complaints. Any person may file a formal complaint alleging a violation of the rules in this part. ...

47 CFR 8.12 - Formal Complaints.

Code of Federal Regulations, 2011 CFR

2011-10-01

... 47 Telecommunication 1 2011-10-01 2011-10-01 false Formal Complaints. 8.12 Section 8.12 Telecommunication FEDERAL COMMUNICATIONS COMMISSION GENERAL PRESERVING THE OPEN INTERNET § 8.12 Formal Complaints. Any person may file a formal complaint alleging a violation of the rules in this part. ...

Radiative transfer calculated from a Markov chain formalism

NASA Technical Reports Server (NTRS)

Esposito, L. W.; House, L. L.

1978-01-01

The theory of Markov chains is used to formulate the radiative transport problem in a general way by modeling the successive interactions of a photon as a stochastic process. Under the minimal requirement that the stochastic process is a Markov chain, the determination of the diffuse reflection or transmission from a scattering atmosphere is equivalent to the solution of a system of linear equations. This treatment is mathematically equivalent to, and thus has many of the advantages of, Monte Carlo methods, but can be considerably more rapid than Monte Carlo algorithms for numerical calculations in particular applications. We have verified the speed and accuracy of this formalism for the standard problem of finding the intensity of scattered light from a homogeneous plane-parallel atmosphere with an arbitrary phase function for scattering. Accurate results over a wide range of parameters were obtained with computation times comparable to those of a standard 'doubling' routine. The generality of this formalism thus allows fast, direct solutions to problems that were previously soluble only by Monte Carlo methods. Some comparisons are made with respect to integral equation methods.

NASA Update

NASA Image and Video Library

2009-07-20

NASA Deputy Administrator Lori Garver, right, looks on as NASA Administrator Charles F. Bolden Jr. speaks during his first NASA Update,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator and Garver took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

NASA Update

NASA Image and Video Library

2009-07-20

NASA Deputy Administrator Lori Garver, second right on stage, speaks as NASA Administrator Charles F. Bolden Jr. looks on during a NASA Update,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator and Garver took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

NASA software specification and evaluation system design, part 1

NASA Technical Reports Server (NTRS)

1976-01-01

The research to develop methods for reducing the effort expended in software and verification is reported. The development of a formal software requirements methodology, a formal specifications language, a programming language, a language preprocessor, and code analysis tools are discussed.

Science Engagement Through Hands-On Activities that Promote Scientific Thinking and Generate Excitement and Awareness of NASA Assets, Missions, and Science

NASA Technical Reports Server (NTRS)

Graff, P. V.; Foxworth, S.; Miller, R.; Runco, S.; Luckey, M. K.; Maudlin, E.

2018-01-01

The public with hands-on activities that infuse content related to NASA assets, missions, and science and reflect authentic scientific practices promotes understanding and generates excitement about NASA science, research, and exploration. These types of activities expose our next generation of explorers to science they may be inspired to pursue as a future STEM career and expose people of all ages to unique, exciting, and authentic aspects of NASA exploration. The activities discussed here (Blue Marble Matches, Lunar Geologist Practice, Let's Discover New Frontiers, Target Asteroid, and Meteorite Bingo) have been developed by Astromaterials Research and Exploration Science (ARES) Science Engagement Specialists in conjunction with ARES Scientists at the NASA Johnson Space Center. Activities are designed to be usable across a variety of educational environments (formal and informal) and reflect authentic scientific content and practices.

Projected Regression Methods for Inverting Fredholm Integrals: Formalism and Application to Analytical Continuation

NASA Astrophysics Data System (ADS)

Arsenault, Louis-Francois; Neuberg, Richard; Hannah, Lauren A.; Millis, Andrew J.

We present a machine learning-based statistical regression approach to the inversion of Fredholm integrals of the first kind by studying an important example for the quantum materials community, the analytical continuation problem of quantum many-body physics. It involves reconstructing the frequency dependence of physical excitation spectra from data obtained at specific points in the complex frequency plane. The approach provides a natural regularization in cases where the inverse of the Fredholm kernel is ill-conditioned and yields robust error metrics. The stability of the forward problem permits the construction of a large database of input-output pairs. Machine learning methods applied to this database generate approximate solutions which are projected onto the subspace of functions satisfying relevant constraints. We show that for low input noise the method performs as well or better than Maximum Entropy (MaxEnt) under standard error metrics, and is substantially more robust to noise. We expect the methodology to be similarly effective for any problem involving a formally ill-conditioned inversion, provided that the forward problem can be efficiently solved. AJM was supported by the Office of Science of the U.S. Department of Energy under Subcontract No. 3F-3138 and LFA by the Columbia Univeristy IDS-ROADS project, UR009033-05 which also provided part support to RN and LH.

NASA SMD and DPS Resources for Higher Education Faculty

NASA Astrophysics Data System (ADS)

Buxner, Sanlyn; Grier, Jennifer; Meinke, Bonnie; Schneider, Nick; Low, Rusty; Schultz, Greg; Manning, James; Fraknoi, Andrew; Gross, Nicholas

2015-11-01

The NASA Education and Public Outreach Forums have developed and provided resources for higher education for the past six years through a cooperative agreement with NASA’s Science Mission Directorate. Collaborations with science organizations, including AAS’s Division of Planetary Sciences, have resulted in more tools, professional training opportunities, and dissemination of resources for teaching in the undergraduate classroom. Resources have been developed through needs assessments of the community and with input from scientists and undergraduate instructors. All resources are freely available.NASA Wavelength (nasawavelength.org) is a collection of digital peer reviewed Earth and space science resources for formal and informal educators of all levels. All resources were developed through funding of the NASA Science Mission Directorate and have undergone a peer-review process through which educators and scientists ensure the content is accurate and useful in an educational setting. Within NASA Wavelength are specific lists of activities and resources for higher education faculty. Additionally, several resources have been developed for introductory college classrooms. The DPS Discovery slide sets are 3-slide presentations that can be incorporated into college lectures to keep classes apprised of the fast moving field of planetary science (http://dps.aas.org/education/dpsdisc). The “Astro 101 slide sets”, developed by the Astro Forum, are presentations 5-7 slides in length on a new development or discovery from a NASA Astrophysics mission relevant to topics in introductory astronomy courses of discoveries not yet in textbooks. Additional resources guides are available for Astro 101 courses and include cosmology and exoplanets. (https://www.astrosociety.org/education/resources-for-the-higher-education-audience/).Professional development opportunities are available to faculty to increase content knowledge and pedagogical tools. These include workshops at

Public Outreach with NASA Lunar and Planetary Mapping and Modeling

NASA Technical Reports Server (NTRS)

Law, E.; Day, B

2017-01-01

NASA's Trek family of online portals is an exceptional collection of resources making it easy for students and the public to explore surfaces of planetary bodies using real data from real missions. Exotic landforms on other worlds and our plans to explore them provide inspiring context for science and technology lessons in classrooms, museums, and at home. These portals can be of great value to formal and informal educators, as well as to scientists working to share the excitement of the latest developments in planetary science, and can significantly enhance visibility and public engagement in missions of exploration.

NASA's Participation in Joint SatOPS Compatibility Efforts 2009-2010

NASA Technical Reports Server (NTRS)

Smith, Danford

2010-01-01

Many U.S. government organizations build or fly space systems: a) NASA, NOAA, Navy, Air Force, NRO, ORS. Others? b) Through the Joint SatOps Compatibility Committee (JSCC) we have increased the grass-roots interaction between many of these organizations. c) We all deal with many of the same challenges: More rapid deployments, lower budgets; Advancing technologies - frameworks, clouds, virtualization; Evolving concepts - automation, situational awareness, enterprise mngt. Standardization - formal or by common use. There is an inherently governmental role in creating the business case for contractors and commercial product vendors to move in directions beneficial to multiple government space organizations.

Public Outreach with NASA Lunar and Planetary Mapping and Modeling

NASA Astrophysics Data System (ADS)

Law, E.; Day, B.

2017-09-01

NASA's Trek family of online portals is an exceptional collection of resources making it easy for students and the public to explore surfaces of planetary bodies using real data from real missions. Exotic landforms on other worlds and our plans to explore them provide inspiring context for science and technology lessons in classrooms, museums, and at home. These portals can be of great value to formal and informal educators, as well as to scientists working to share the excitement of the latest developments in planetary science, and can significantly enhance visibility and public engagement in missions of exploration.

Geospatial Education: Working with the NASA Airborne Science Program

NASA Astrophysics Data System (ADS)

Lockwood, C. M.; Handley, L.; Handley, N.

2010-12-01

WETMAAP (Wetland Education Through Maps and Aerial Photography) , a program of CNL World, supports the NASA Strategic Goals and Objectives for Education by providing classroom teachers and formal and informal educators with professional development. WETMAAP promotes science by inquiry through the use of a building-block process, comparative analysis, and analytical observations. Through the WETMAAP workshops and website, educators receive the concepts necessary to provide students with a basic understanding of maps, aerial photography, and satellite and airborne imagery that focus on the study of wetlands and wetland change. The program targets educators, Grades 5 - 12, in earth science, environmental science, biology, geography, and mathematics, and emphasizes a comprehensive curriculum approach.

Analytical derivatives of the individual state energies in ensemble density functional theory method. I. General formalism

DOE PAGES

Filatov, Michael; Liu, Fang; Martínez, Todd J.

2017-07-21

The state-averaged (SA) spin restricted ensemble referenced Kohn-Sham (REKS) method and its state interaction (SI) extension, SI-SA-REKS, enable one to describe correctly the shape of the ground and excited potential energy surfaces of molecules undergoing bond breaking/bond formation reactions including features such as conical intersections crucial for theoretical modeling of non-adiabatic reactions. Until recently, application of the SA-REKS and SI-SA-REKS methods to modeling the dynamics of such reactions was obstructed due to the lack of the analytical energy derivatives. Here, the analytical derivatives of the individual SA-REKS and SI-SA-REKS energies are derived. The final analytic gradient expressions are formulated entirelymore » in terms of traces of matrix products and are presented in the form convenient for implementation in the traditional quantum chemical codes employing basis set expansions of the molecular orbitals. Finally, we will describe the implementation and benchmarking of the derived formalism in a subsequent article of this series.« less

Formalizing the concept of sound.

DOE Office of Scientific and Technical Information (OSTI.GOV)

Kaper, H. G.; Tipei, S.

1999-08-03

The notion of formalized music implies that a musical composition can be described in mathematical terms. In this article we explore some formal aspects of music and propose a framework for an abstract approach.

Sharing NASA Science with Decision Makers: A Perspective from NASA's Applied Remote Sensing Training (ARSET) Program

NASA Astrophysics Data System (ADS)

Prados, A. I.; Blevins, B.; Hook, E.

2015-12-01

NASA ARSET http://arset.gsfc.nasa.gov has been providing applied remote sensing training since 2008. The goals of the program are to develop the technical and analytical skills necessary to utilize NASA resources for decision-support. The program has reached over 3500 participants, with 1600 stakeholders from 100 countries in 2015 alone. The target audience for the program are professionals engaged in environmental management in the public and private sectors, such as air quality forecasters, public utilities, water managers and non-governmental organizations engaged in conservation. Many program participants have little or no expertise in NASA remote sensing, and it's frequently their very first exposure to NASA's vast resources. One the key challenges for the program has been the evolution and refinement of its approach to communicating NASA data access, research, and ultimately its value to stakeholders. We discuss ARSET's best practices for sharing NASA science, which include 1) training ARSET staff and other NASA scientists on methods for science communication, 2) communicating the proper amount of scientific information at a level that is commensurate with the technical skills of program participants, 3) communicating the benefit of NASA resources to stakeholders, and 4) getting to know the audience and tailoring the message so that science information is conveyed within the context of agencies' unique environmental challenges.

NASA Earth Observations (NEO): Data Imagery for Education and Visualization

NASA Astrophysics Data System (ADS)

Ward, K.

2008-12-01

NASA Earth Observations (NEO) has dramatically simplified public access to georeferenced imagery of NASA remote sensing data. NEO targets the non-traditional data users who are currently underserved by functionality and formats available from the existing data ordering systems. These users include formal and informal educators, museum and science center personnel, professional communicators, and citizen scientists. NEO currently serves imagery from 45 different datasets with daily, weekly, and/or monthly temporal resolutions, with more datasets currently under development. The imagery from these datasets is produced in coordination with several data partners who are affiliated either with the instrument science teams or with the respective data processing center. NEO is a system of three components -- website, WMS (Web Mapping Service), and ftp archive -- which together are able to meet the wide-ranging needs of our users. Some of these needs include the ability to: view and manipulate imagery using the NEO website -- e.g., applying color palettes, resizing, exporting to a variety of formats including PNG, JPEG, KMZ (Google Earth), GeoTIFF; access the NEO collection via a standards-based API (WMS); and create customized exports for select users (ftp archive) such as Science on a Sphere, NASA's Earth Observatory, and others.

Open systems & non-formal education

NASA Astrophysics Data System (ADS)

Wheeler, Gerald F.

1988-10-01

Professor Dib created an important structure that can be used to attach the many and various activities that fall in the category of this title. While I plan to use his structure, I will be emphasizing a different component of his spectrum and promoting a different need. Professor Dib suggested a critical need to move our teaching styles away from formal modes to non-formal modes of delivery. I suggest an equally critical need in the area of informal education. And, I will propose aways to move us toward the same goal, non-formal activities. I believe we need to find ways to use the many informal education activities that occur almost automatically in our societies to move our potential learners to richer non-formal endeavors. Both needs are real; both activities are valid.

NASA Update.

NASA Image and Video Library

2011-02-15

NASA Deputy Administrator Lori Garver answers questions during a NASA Update on, Tuesday, Feb. 15, 2011, at NASA Headquarters in Washington. Garver and NASA Administrator Charles Bolden took the time discuss the agency’s fiscal year 2012 budget request and to take questions from employees. Photo Credit: (NASA/Bill Ingalls)

NASA Update

NASA Image and Video Library

2009-07-20

Alan Ladwig, senior advisor to the NASA Administator, far left, makes a point as he introduces NASA Administrator Charles F. Bolden Jr. and Deputy Administrator Lori Garver at a NASA Update,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator and Garver took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

On the simulation of indistinguishable fermions in the many-body Wigner formalism

DOE Office of Scientific and Technical Information (OSTI.GOV)

Sellier, J.M., E-mail: jeanmichel.sellier@gmail.com; Dimov, I.

2015-01-01

The simulation of quantum systems consisting of interacting, indistinguishable fermions is an incredible mathematical problem which poses formidable numerical challenges. Many sophisticated methods addressing this problem are available which are based on the many-body Schrödinger formalism. Recently a Monte Carlo technique for the resolution of the many-body Wigner equation has been introduced and successfully applied to the simulation of distinguishable, spinless particles. This numerical approach presents several advantages over other methods. Indeed, it is based on an intuitive formalism in which quantum systems are described in terms of a quasi-distribution function, and highly scalable due to its Monte Carlo nature.more » In this work, we extend the many-body Wigner Monte Carlo method to the simulation of indistinguishable fermions. To this end, we first show how fermions are incorporated into the Wigner formalism. Then we demonstrate that the Pauli exclusion principle is intrinsic to the formalism. As a matter of fact, a numerical simulation of two strongly interacting fermions (electrons) is performed which clearly shows the appearance of a Fermi (or exchange–correlation) hole in the phase-space, a clear signature of the presence of the Pauli principle. To conclude, we simulate 4, 8 and 16 non-interacting fermions, isolated in a closed box, and show that, as the number of fermions increases, we gradually recover the Fermi–Dirac statistics, a clear proof of the reliability of our proposed method for the treatment of indistinguishable particles.« less

Requirements to Design to Code: Towards a Fully Formal Approach to Automatic Code Generation

NASA Technical Reports Server (NTRS)

Hinchey, Michael G.; Rash, James L.; Rouff, Christopher A.

2005-01-01

A general-purpose method to mechanically transform system requirements into a provably equivalent model has yet to appear. Such a method represents a necessary step toward high-dependability system engineering for numerous possible application domains, including distributed software systems, sensor networks, robot operation, complex scripts for spacecraft integration and testing, and autonomous systems. Currently available tools and methods that start with a formal model of a system and mechanically produce a provably equivalent implementation are valuable but not sufficient. The gap that current tools and methods leave unfilled is that their formal models cannot be proven to be equivalent to the system requirements as originated by the customer. For the classes of systems whose behavior can be described as a finite (but significant) set of scenarios, we offer a method for mechanically transforming requirements (expressed in restricted natural language, or in other appropriate graphical notations) into a provably equivalent formal model that can be used as the basis for code generation and other transformations.

Requirements to Design to Code: Towards a Fully Formal Approach to Automatic Code Generation

NASA Technical Reports Server (NTRS)

Hinchey, Michael G.; Rash, James L.; Rouff, Christopher A.

2005-01-01

A general-purpose method to mechanically transform system requirements into a provably equivalent model has yet to appear. Such a method represents a necessary step toward high-dependability system engineering for numerous possible application domains, including distributed software systems, sensor networks, robot operation, complex scripts for spacecraft integration and testing, and autonomous systems. Currently available tools and methods that start with a formal model of a: system and mechanically produce a provably equivalent implementation are valuable but not sufficient. The "gap" that current tools and methods leave unfilled is that their formal models cannot be proven to be equivalent to the system requirements as originated by the customer. For the ciasses of systems whose behavior can be described as a finite (but significant) set of scenarios, we offer a method for mechanically transforming requirements (expressed in restricted natural language, or in other appropriate graphical notations) into a provably equivalent formal model that can be used as the basis for code generation and other transformations.

Requirements to Design to Code: Towards a Fully Formal Approach to Automatic Code Generation

NASA Technical Reports Server (NTRS)

Hinchey, Michael G.; Rash, James L.; Rouff, Christopher A.

2004-01-01

A general-purpose method to mechanically transform system requirements into a provably equivalent model has yet to appear. Such a method represents a necessary step toward high-dependability system engineering for numerous possible application domains, including sensor networks and autonomous systems. Currently available tools and methods that start with a formal model of a system and mechanically produce a provably equivalent implementation are valuable but not sufficient. The gap that current tools and methods leave unfilled is that their formal models cannot be proven to be equivalent to the system requirements as originated by the customer. For the classes of systems whose behavior can be described as a finite (but significant) set of scenarios, we offer a method for mechanically transforming requirements (expressed in restricted natural language, or in other appropriate graphical notations) into a provably equivalent formal model that can be used as the basis for code generation and other transformations.

NASA Quest.

ERIC Educational Resources Information Center

Ashby, Susanne

2000-01-01

Introduces NASA Quest as part of NASA's Learning Technologies Project, which connects students to the people of NASA through the various pages at the website where students can glimpse the various types of work performed at different NASA facilities and talk to NASA workers about the type of work they do. (ASK)

The NASA Technical Report Server

NASA Technical Reports Server (NTRS)

Nelson, Michael L.; Gottlich, Gretchen L.; Bianco, David J.; Paulson, Sharon S.; Binkley, Robert L.; Kellogg, Yvonne D.; Beaumont, Chris J.; Schmunk, Robert B.; Kurtz, Michael J.; Accomazzi, Alberto

1995-01-01

The National Aeronautics and Space Act of 1958 established NASA and charged it to "provide for the widest practicable and appropriate dissemination of information concerning its activities and the results thereof." The search for innovative methods to distribute NASA's information lead a grass-roots team to create the NASA Technical Report Server (NTRS), which uses the World Wide Web and other popular Internet-based information systems as search engines. The NTRS is an inter-center effort which provides uniform access to various distributed publication servers residing on the Internet. Users have immediate desktop access to technical publications from NASA centers and institutes. The NTRS is comprised of several units, some constructed especially for inclusion in NTRS, and others that are existing NASA publication services that NTRS reuses. This paper presents the NTRS architecture, usage metrics, and the lessons learned while implementing and maintaining the service. The NTRS is largely constructed with freely available software running on existing hardware. NTRS builds upon existing hardware and software, and the resulting additional exposure for the body of literature contained ensures that NASA's institutional knowledge base will continue to receive the widest practicable and appropriate dissemination.

Formal verification of medical monitoring software using Z language: a representative sample.

PubMed

Babamir, Seyed Morteza; Borhani, Mehdi

2012-08-01

Medical monitoring systems are useful aids assisting physicians in keeping patients under constant surveillance; however, taking sound decision by the systems is a physician concern. As a result, verification of the systems behavior in monitoring patients is a matter of significant. The patient monitoring is undertaken by software in modern medical systems; so, software verification of modern medial systems have been noticed. Such verification can be achieved by the Formal Languages having mathematical foundations. Among others, the Z language is a suitable formal language has been used to formal verification of systems. This study aims to present a constructive method to verify a representative sample of a medical system by which the system is visually specified and formally verified against patient constraints stated in Z Language. Exploiting our past experience in formal modeling Continuous Infusion Insulin Pump (CIIP), we think of the CIIP system as a representative sample of medical systems in proposing our present study. The system is responsible for monitoring diabetic's blood sugar.

New method of contour image processing based on the formalism of spiral light beams

NASA Astrophysics Data System (ADS)

Volostnikov, Vladimir G.; Kishkin, S. A.; Kotova, S. P.

2013-07-01

The possibility of applying the mathematical formalism of spiral light beams to the problems of contour image recognition is theoretically studied. The advantages and disadvantages of the proposed approach are evaluated; the results of numerical modelling are presented.

NASA Update

NASA Image and Video Library

2011-02-15

NASA Administrator Charles F. Bolden Jr., and Deputy Administrator Lori Garver deliver a NASA Update on, Tuesday, Feb. 15, 2011, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator and Garver took the time discuss the agency’s fiscal year 2012 budget request and to take questions from employees. Photo Credit: (NASA/Bill Ingalls)

NASA Update

NASA Image and Video Library

2011-02-15

NASA Deputy Administrator Lori Garver listens as NASA Administrator Charles Bolden answers a question during a NASA Update on Tuesday, Feb. 15, 2011, at NASA Headquarters in Washington. Bolden and Garver took the time discuss the agency’s fiscal year 2012 budget request and to take questions from employees. Photo Credit: (NASA/Bill Ingalls)

The Formalism of Quantum Mechanics Specified by Covariance Properties

NASA Astrophysics Data System (ADS)

Nisticò, G.

2009-03-01

The known methods, due for instance to G.W. Mackey and T.F. Jordan, which exploit the transformation properties with respect to the Euclidean and Galileian group to determine the formalism of the Quantum Theory of a localizable particle, fail in the case that the considered transformations are not symmetries of the physical system. In the present work we show that the formalism of standard Quantum Mechanics for a particle without spin can be completely recovered by exploiting the covariance properties with respect to the group of Euclidean transformations, without requiring that these transformations are symmetries of the physical system.

Development of Implicit Methods in CFD NASA Ames Research Center 1970's - 1980's

NASA Technical Reports Server (NTRS)

Pulliam, Thomas H.

2010-01-01

The focus here is on the early development (mid 1970's-1980's) at NASA Ames Research Center of implicit methods in Computational Fluid Dynamics (CFD). A class of implicit finite difference schemes of the Beam and Warming approximate factorization type will be addressed. The emphasis will be on the Euler equations. A review of material pertinent to the solution of the Euler equations within the framework of implicit methods will be presented. The eigensystem of the equations will be used extensively in developing a framework for various methods applied to the Euler equations. The development and analysis of various aspects of this class of schemes will be given along with the motivations behind many of the choices. Various acceleration and efficiency modifications such as matrix reduction, diagonalization and flux split schemes will be presented.

State-vector formalism and the Legendre polynomial solution for modelling guided waves in anisotropic plates

NASA Astrophysics Data System (ADS)

Zheng, Mingfang; He, Cunfu; Lu, Yan; Wu, Bin

2018-01-01

We presented a numerical method to solve phase dispersion curve in general anisotropic plates. This approach involves an exact solution to the problem in the form of the Legendre polynomial of multiple integrals, which we substituted into the state-vector formalism. In order to improve the efficiency of the proposed method, we made a special effort to demonstrate the analytical methodology. Furthermore, we analyzed the algebraic symmetries of the matrices in the state-vector formalism for anisotropic plates. The basic feature of the proposed method was the expansion of field quantities by Legendre polynomials. The Legendre polynomial method avoid to solve the transcendental dispersion equation, which can only be solved numerically. This state-vector formalism combined with Legendre polynomial expansion distinguished the adjacent dispersion mode clearly, even when the modes were very close. We then illustrated the theoretical solutions of the dispersion curves by this method for isotropic and anisotropic plates. Finally, we compared the proposed method with the global matrix method (GMM), which shows excellent agreement.

NASA Wavelength: A Full Spectrum of NASA Resources for Earth and Space Science Education

NASA Astrophysics Data System (ADS)

Smith, D. A.; Schwerin, T. G.; Peticolas, L. M.; Porcello, D.; Kansa, E.; Shipp, S. S.; Bartolone, L.

2013-12-01

The NASA Science Education and Public Outreach Forums have developed a digital library--NASAWavelength.org--that enables easy discovery and retrieval of thousands of resources from the NASA Earth and space science education portfolio. The system has been developed based on best practices in the architecture and design of web-based information systems. The design style and philosophy emphasize simple, reusable data and services that facilitate the free flow of data across systems. The primary audiences for NASA Wavelength are STEM educators (K-12, higher education and informal education) as well as scientists, education and public outreach professionals who work with K-12, higher education, and informal education. A NASA Wavelength strandmap service features the 19 AAAS strandmaps that are most relevant to NASA science; the service also generates all of the 103 AAAS strandmaps with content from the Wavelength collection. These maps graphically and interactively provide connections between concepts as well as illustrate how concepts build upon one another across grade levels. New features have been developed for this site based on user feedback, including list-building so that users can create and share individual collections within Wavelength. We will also discuss potential methods for integrating the Next Generation Science Standards (NGSS) into the search and discovery tools on NASA Wavelength.

Teaching Astronomy in non-formal education: stars workshop

NASA Astrophysics Data System (ADS)

Hernán-Obispo, M.; Crespo-Chacón, I.; Gálvez, M. C.; López-Santiago, J.

One of the fields in which teaching Astronomy is more demanded is non-formal education. The Stars Workshop we present in this contribution consisted on an introduction to Astronomy and observation methods. The main objectives were: to know the main components of the Universe, their characteristics and the scales of size and time existing between them; to understand the movement of the different celestial objects; to know the different observational techniques; to value the different historical explanations about the Earth and the position of Humanity in the Universe. This Stars Workshop was a collaboration with the Escuela de Tiempo Libre Jumavi, which is a school dedicated to the training and non-formal education in the leisure field.

NASA Update

NASA Image and Video Library

2011-02-15

NASA Deputy Associate Administrator for the Office of Communications Bob Jacobs moderates the NASA Update program, Tuesday, Feb. 15, 2011 at NASA Headquarters in Washington. NASA's 12th Administrator Charles Bolden and Deputy Administrator Lori Garver took the time discuss the agency’s fiscal year 2012 budget request and to take questions from employees. Photo Credit: (NASA/Bill Ingalls)

Formal verification of an avionics microprocessor

NASA Technical Reports Server (NTRS)

Srivas, Mandayam, K.; Miller, Steven P.

1995-01-01

Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This report discusses a project undertaken to answer some of these questions, the formal verification of the AAMPS microprocessor. This project consisted of formally specifying in the PVS language a rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show that the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification.

Heuristics structure and pervade formal risk assessment.

PubMed

MacGillivray, Brian H

2014-04-01

Lay perceptions of risk appear rooted more in heuristics than in reason. A major concern of the risk regulation literature is that such "error-strewn" perceptions may be replicated in policy, as governments respond to the (mis)fears of the citizenry. This has led many to advocate a relatively technocratic approach to regulating risk, characterized by high reliance on formal risk and cost-benefit analysis. However, through two studies of chemicals regulation, we show that the formal assessment of risk is pervaded by its own set of heuristics. These include rules to categorize potential threats, define what constitutes valid data, guide causal inference, and to select and apply formal models. Some of these heuristics lay claim to theoretical or empirical justifications, others are more back-of-the-envelope calculations, while still more purport not to reflect some truth but simply to constrain discretion or perform a desk-clearing function. These heuristics can be understood as a way of authenticating or formalizing risk assessment as a scientific practice, representing a series of rules for bounding problems, collecting data, and interpreting evidence (a methodology). Heuristics are indispensable elements of induction. And so they are not problematic per se, but they can become so when treated as laws rather than as contingent and provisional rules. Pitfalls include the potential for systematic error, masking uncertainties, strategic manipulation, and entrenchment. Our central claim is that by studying the rules of risk assessment qua rules, we develop a novel representation of the methods, conventions, and biases of the prior art. © 2013 Society for Risk Analysis.

Strategies for recruiting additional African Americans into the NASA JSC summer faculty fellows program

NASA Technical Reports Server (NTRS)

Hyman, Ladelle M.

1993-01-01

African Americans have participated sporadically in the NASA JSC Summer Faculty Fellows Program--none in 1992 and four in 1993. There is a pool of African Americans who are both qualified to provide services and willing to participate in initiatives which support technologies required for future JSC programs. They can provide human support and handle mission operations, spacecraft systems, planet surface systems, and management tools. Most of these faculty teach at historically black colleges and universities (HBCU's). This research will document the current recruitment system, critique it, and develop a strategy which will facilitate the diversification of the NASA JSC Summer Faculty Fellows Program. While NASA currently mails notices to HBCU's, such notices have generated few applications from, and fewer selections of, targeted faculty. To increase the participation of African Americans in the NASA JSC Summer Faculty Fellows Program, this participant will prepare a strategy which includes a document which identifies HBCU-targeted faculty and enumerates more formally extensive and intensive communication procedures. A fifteen-minute panel discussion, which will include a video, will be delivered during the annual meeting of the American Society for Engineering Education (ASEE) to be held in Edmonton, Alberta, Canada, June 26-29, 1994. An announcement letter will be mailed to targeted faculty; follow-up telephone calls and personal visits will be made and a checklist flowchart will be completed by key NASA personnel or designee. Although initially limited to NASA JSC's recruitment of African Americans, this strategy may be broadened to include other NASA sites and other targeted minority groups.

NASA Update

NASA Image and Video Library

2009-07-20

NASA Administrator Charles F. Bolden Jr. left, speaks during his first NASA Update as Deputy Administrator Lori Garver looks on,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator and Garver took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

NASA Update

NASA Image and Video Library

2009-07-20

NASA Administrator Charles F. Bolden Jr. left, and Deputy Administrator Lori Garver are seen during their first NASA Update,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator and Garver took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

NASA Update

NASA Image and Video Library

2009-07-20

NASA Administrator Charles F. Bolden Jr. speaks during his first NASA Update,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator, was joined by Deputy Administrator Lori Garver where they took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

The influence of formal and informal policies and practices on health care innovation implementation: A mixed-methods analysis.

PubMed

DiMartino, Lisa D; Birken, Sarah A; Hanson, Laura C; Trogdon, Justin G; Clary, Alecia S; Weinberger, Morris; Reeder-Hayes, Katherine; Weiner, Bryan J

The implementation science literature has contributed important insights regarding the influence of formal policies and practices on health care innovation implementation, whereas informal implementation policies and practices have garnered little attention. The broader literature suggests that informal implementation policies and practices could also influence innovation use. We used the Organizational Theory of Innovation Implementation to further understand the role of formal and informal implementation policies and practices as determinants of implementation effectiveness. We examined their role within the context of initiatives to increase palliative care consultation in inpatient oncology. We used a case study design in two organizational settings within one academic medical center: medical and gynecologic oncology. We completed semistructured interviews with medical (n = 12) and gynecologic (n = 10) oncology clinicians using questions based on organizational theory. Quantitative data assessed implementation effectiveness, defined as aggregated palliative care consult rates within oncology services from 2010 to 2016. Four palliative care clinicians were interviewed to gain additional implementation context insights. Medical oncology employed multiple formal policies and practices including training and clinician prompting to support palliative care consultation and a top-down approach, yet most clinicians were unaware of the policies and practices, contributing to a weak implementation climate. In contrast, gynecologic oncology employed one formal policy (written guideline of criteria for initiating a consult) but also relied on informal policies and practices, such as spontaneous feedback and communication; they adopted a bottom-up approach, contributing to broader clinician awareness and strong implementation climate. Both services exhibited variable, increasing consult rates over time. Informal policies and practices may compensate or substitute for formal

Formalizing Probabilistic Safety Claims

NASA Technical Reports Server (NTRS)

Herencia-Zapana, Heber; Hagen, George E.; Narkawicz, Anthony J.

2011-01-01

A safety claim for a system is a statement that the system, which is subject to hazardous conditions, satisfies a given set of properties. Following work by John Rushby and Bev Littlewood, this paper presents a mathematical framework that can be used to state and formally prove probabilistic safety claims. It also enables hazardous conditions, their uncertainties, and their interactions to be integrated into the safety claim. This framework provides a formal description of the probabilistic composition of an arbitrary number of hazardous conditions and their effects on system behavior. An example is given of a probabilistic safety claim for a conflict detection algorithm for aircraft in a 2D airspace. The motivation for developing this mathematical framework is that it can be used in an automated theorem prover to formally verify safety claims.

Formal analysis of imprecise system requirements with Event-B.

PubMed

Le, Hong Anh; Nakajima, Shin; Truong, Ninh Thuan

2016-01-01

Formal analysis of functional properties of system requirements needs precise descriptions. However, the stakeholders sometimes describe the system with ambiguous, vague or fuzzy terms, hence formal frameworks for modeling and verifying such requirements are desirable. The Fuzzy If-Then rules have been used for imprecise requirements representation, but verifying their functional properties still needs new methods. In this paper, we propose a refinement-based modeling approach for specification and verification of such requirements. First, we introduce a representation of imprecise requirements in the set theory. Then we make use of Event-B refinement providing a set of translation rules from Fuzzy If-Then rules to Event-B notations. After that, we show how to verify both safety and eventuality properties with RODIN/Event-B. Finally, we illustrate the proposed method on the example of Crane Controller.

NASA EEE Parts and Advanced Interconnect Program (AIP)

NASA Technical Reports Server (NTRS)

Gindorf, T.; Garrison, A.

1996-01-01

none given From Program Objectives: I. Accelerate the readiness of new technologies through development of validation, assessment and test method/tools II. Provide NASA Projects infusion paths for emerging technologies III. Provide NASA Projects technology selection, application and validation guidelines for harware and processes IV. Disseminate quality assurance, reliability, validation, tools and availability information to the NASA community.

NASA Update

NASA Image and Video Library

2009-07-20

NASA Administrator Charles F. Bolden Jr. left on stage, speaks during his first NASA Update as Deputy Administrator Lori Garver looks on at right,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator and Garver took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

NASA Update

NASA Image and Video Library

2009-07-20

NASA Administrator Charles F. Bolden Jr., left on stage, speaks during his first NASA Update as Deputy Administrator Lori Garver looks on at right,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator and Garver took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

NASA Update

NASA Image and Video Library

2009-07-20

NASA Deputy Administrator Lori Garver makes a point as she speaks during a NASA Update with Administrator Charles F. Bolden Jr.,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator and Garver took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

Augmenting Reality and Formality of Informal and Non-Formal Settings to Enhance Blended Learning

ERIC Educational Resources Information Center

Pérez-Sanagustin, Mar; Hernández-Leo, Davinia; Santos, Patricia; Kloos, Carlos Delgado; Blat, Josep

2014-01-01

Visits to museums and city tours have been part of higher and secondary education curriculum activities for many years. However these activities are typically considered "less formal" when compared to those carried out in the classroom, mainly because they take place in informal or non-formal settings. Augmented Reality (AR) technologies…

The Development of Introductory Statistics Students' Informal Inferential Reasoning and Its Relationship to Formal Inferential Reasoning

ERIC Educational Resources Information Center

Jacob, Bridgette L.

2013-01-01

The difficulties introductory statistics students have with formal statistical inference are well known in the field of statistics education. "Informal" statistical inference has been studied as a means to introduce inferential reasoning well before and without the formalities of formal statistical inference. This mixed methods study…

Evaluation of Alternative Altitude Scaling Methods for Thermal Ice Protection System in NASA Icing Research Tunnel

NASA Technical Reports Server (NTRS)

Lee, Sam; Addy, Harold; Broeren, Andy P.; Orchard, David M.

2017-01-01

A test was conducted at NASA Icing Research Tunnel to evaluate altitude scaling methods for thermal ice protection system. Two scaling methods based on Weber number were compared against a method based on the Reynolds number. The results generally agreed with the previous set of tests conducted in NRCC Altitude Icing Wind Tunnel. The Weber number based scaling methods resulted in smaller runback ice mass than the Reynolds number based scaling method. The ice accretions from the Weber number based scaling method also formed farther upstream. However there were large differences in the accreted ice mass between the two Weber number based scaling methods. The difference became greater when the speed was increased. This indicated that there may be some Reynolds number effects that isnt fully accounted for and warrants further study.

NASA Update

NASA Image and Video Library

2009-07-20

NASA Administrator Charles F. Bolden Jr. is seen through a television camera monitor during his first NASA Update,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator, was joined by Deputy Administrator Lori Garver where they took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

NASA Update

NASA Image and Video Library

2009-07-20

NASA Administrator Charles F. Bolden Jr. is seen on a television camera monitor while speaking at his first NASA Update,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, NASA's 12th Administrator, was joined by Deputy Administrator Lori Garver where they took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

Formal and informal authority of hospital directors.

PubMed

Nirel, N; Schmid, H; Stern, Z

1994-01-01

Describes and contrasts the perceptions of formal and informal authority of hospital directors of two different kinds of organizations: hospitals that are part of public multi-hospital organizations (PMOs) and independent hospitals. Indicates that all the directors perceive their formal authority to be greater than their formal authority. However, there is a gap in the perception of formal and informal authority by directors of the two types of hospital. Directors of independent hospitals perceive themselves to have more formal and informal authority than do their colleagues at hospitals that are part of PMOs. Both structural and personal explanations for these findings are given. In addition, discusses the implications for policy making of the source of authority, informal, and formal authority in the transition to autonomous semi-independent hospitals in a changing environment.

MOOC & B-Learning: Students' Barriers and Satisfaction in Formal and Non-Formal Learning Environments

ERIC Educational Resources Information Center

Gutiérrez-Santiuste, Elba; Gámiz-Sánchez, Vanesa-M.; Gutiérrez-Pérez, Jose

2015-01-01

The study presents a comparative analysis of two virtual learning formats: one non-formal through a Massive Open Online Course (MOOC) and the other formal through b-learning. We compare the communication barriers and the satisfaction perceived by the students (N = 249) by developing a qualitative analysis using semi-structured questionnaires and…

Detecting Mode Confusion Through Formal Modeling and Analysis

NASA Technical Reports Server (NTRS)

Miller, Steven P.; Potts, James N.

1999-01-01

Aircraft safety has improved steadily over the last few decades. While much of this improvement can be attributed to the introduction of advanced automation in the cockpit, the growing complexity of these systems also increases the potential for the pilots to become confused about what the automation is doing. This phenomenon, often referred to as mode confusion, has been involved in several accidents involving modern aircraft. This report describes an effort by Rockwell Collins and NASA Langley to identify potential sources of mode confusion through two complementary strategies. The first is to create a clear, executable model of the automation, connect it to a simulation of the flight deck, and use this combination to review of the behavior of the automation and the man-machine interface with the designers, pilots, and experts in human factors. The second strategy is to conduct mathematical analyses of the model by translating it into a formal specification suitable for analysis with automated tools. The approach is illustrated by applying it to a hypothetical, but still realistic, example of the mode logic of a Flight Guidance System.

Formality of the Chinese collective leadership.

PubMed

Li, Haiying; Graesser, Arthur C

2016-09-01

We investigated the linguistic patterns in the discourse of four generations of the collective leadership of the Communist Party of China (CPC) from 1921 to 2012. The texts of Mao Zedong, Deng Xiaoping, Jiang Zemin, and Hu Jintao were analyzed using computational linguistic techniques (a Chinese formality score) to explore the persuasive linguistic features of the leaders in the contexts of power phase, the nation's education level, power duration, and age. The study was guided by the elaboration likelihood model of persuasion, which includes a central route (represented by formal discourse) versus a peripheral route (represented by informal discourse) to persuasion. The results revealed that these leaders adopted the formal, central route more when they were in power than before they came into power. The nation's education level was a significant factor in the leaders' adoption of the persuasion strategy. The leaders' formality also decreased with their increasing age and in-power times. However, the predictability of these factors for formality had subtle differences among the different types of leaders. These results enhance our understanding of the Chinese collective leadership and the role of formality in politically persuasive messages.

Formal Analysis of Extended Well-Clear Boundaries for Unmanned Aircraft

NASA Technical Reports Server (NTRS)

Munoz, Cesar; Narkawicz, Anthony

2016-01-01

This paper concerns the application of formal methods to the definition of a detect and avoid concept for unmanned aircraft systems (UAS). In particular, it illustrates how formal analysis was used to explain and correct unexpected behaviors of the logic that issues alerts when two aircraft are predicted not to be well clear from one another. As a result of this analysis, a recommendation was proposed to, and subsequently adopted by, the US standards organization that defines the minimum operational requirements for the UAS detect and avoid concept.

Extension of Liouville Formalism to Postinstability Dynamics

NASA Technical Reports Server (NTRS)

Zak, Michail

2003-01-01

A mathematical formalism has been developed for predicting the postinstability motions of a dynamic system governed by a system of nonlinear equations and subject to initial conditions. Previously, there was no general method for prediction and mathematical modeling of postinstability behaviors (e.g., chaos and turbulence) in such a system. The formalism of nonlinear dynamics does not afford means to discriminate between stable and unstable motions: an additional stability analysis is necessary for such discrimination. However, an additional stability analysis does not suggest any modifications of a mathematical model that would enable the model to describe postinstability motions efficiently. The most important type of instability that necessitates a postinstability description is associated with positive Lyapunov exponents. Such an instability leads to exponential growth of small errors in initial conditions or, equivalently, exponential divergence of neighboring trajectories. The development of the present formalism was undertaken in an effort to remove positive Lyapunov exponents. The means chosen to accomplish this is coupling of the governing dynamical equations with the corresponding Liouville equation that describes the evolution of the flow of error probability. The underlying idea is to suppress the divergences of different trajectories that correspond to different initial conditions, without affecting a target trajectory, which is one that starts with prescribed initial conditions.

Thermal Cyclotron Absorption Coefficients. II. Opacities in the Stokes Formalism

NASA Astrophysics Data System (ADS)

Vaeth, H. M.; Chanmugam, G.

1995-05-01

We extend the discussion of the calculation of the cyclotron opacities α± of the ordinary and extraordinary mode (Chanmugam et al.) to the opacities κ, q, υ in the Stokes formalism. We derive formulae with which a can be calculated from κ, q, υ. We are hence able to compare our calculations of the opacities, which are based on the single-particle method, with results obtained with the dielectric tensor method of Tam or. Excellent agreement is achieved. We present extensive tables of the opacities in the Stokes formalism for frequencies up to 25ωc, where ωc is the cyclotron frequency, and temperatures kT = 5, 10,20, 30,40, and 50 keV. Furthermore, we derive approximate formulae with which κ, q, υ can be calculated from α± and hence use the Robinson & Melrose analytic formulae for α± in order to calculate the opacities in the Stokes formalism. We compare these opacities to accurate numerical opacities and find that the analytic formulae can reproduce the qualitative behavior of the opacities in the regions where the harmonic structure is unimportant.

Formalization of the engineering science discipline - knowledge engineering

NASA Astrophysics Data System (ADS)

Peng, Xiao

Knowledge is the most precious ingredient facilitating aerospace engineering research and product development activities. Currently, the most common knowledge retention methods are paper-based documents, such as reports, books and journals. However, those media have innate weaknesses. For example, four generations of flying wing aircraft (Horten, Northrop XB-35/YB-49, Boeing BWB and many others) were mostly developed in isolation. The subsequent engineers were not aware of the previous developments, because these projects were documented such which prevented the next generation of engineers to benefit from the previous lessons learned. In this manner, inefficient knowledge retention methods have become a primary obstacle for knowledge transfer from the experienced to the next generation of engineers. In addition, the quality of knowledge itself is a vital criterion; thus, an accurate measure of the quality of 'knowledge' is required. Although qualitative knowledge evaluation criteria have been researched in other disciplines, such as the AAA criterion by Ernest Sosa stemming from the field of philosophy, a quantitative knowledge evaluation criterion needs to be developed which is capable to numerically determine the qualities of knowledge for aerospace engineering research and product development activities. To provide engineers with a high-quality knowledge management tool, the engineering science discipline Knowledge Engineering has been formalized to systematically address knowledge retention issues. This research undertaking formalizes Knowledge Engineering as follows: 1. Categorize knowledge according to its formats and representations for the first time, which serves as the foundation for the subsequent knowledge management function development. 2. Develop an efficiency evaluation criterion for knowledge management by analyzing the characteristics of both knowledge and the parties involved in the knowledge management processes. 3. Propose and develop an

NASA's Science Education and Public Outreach Forums: Bringing Communities and Resources Together to Increase Effectiveness and Sustainability of E/PO

NASA Astrophysics Data System (ADS)

Sharma, Mangala; Smith, D.; Mendez, B.; Shipp, S.; Schwerin, T.; Stockman, S.; Cooper, L.

2010-03-01

The AAS-HEAD community has a rich history of involvement in education and public outreach (E/PO). HEAD members have been using NASA science and educational resources to engage and educate youth and adults nationwide in science, technology, engineering, and mathematics topics. Four new Science Education and Public Outreach Forums ("Forums") funded by NASA Science Mission Directorate (SMD) are working in partnership with the research and education community to ensure that current and future SMD-funded E/PO activities form a seamless whole, with easy entry points for scientists, engineers, faculty, students, K-12 formal and informal science educators, general public, and E/PO professionals alike. These Forums support the astrophysics, heliophysics, planetary and Earth science divisions of NASA SMD in three core areas: 1) E/PO community engagement and development to facilitate clear paths of involvement for scientists, engineers and others interested - or potentially interested - in participating in SMD-funded E/PO activities. Collaborations with science professionals are vital for infusing current, accurate SMD mission and research findings into educational products and activities. Forum activities will yield readily accessible information on effective E/PO strategies, resources, and expertise; context for individual E/PO activities; and opportunities for collaboration. 2) A rigorous analysis of SMD-funded E/PO products and activities to help understand how the existing collection supports education standards and audience needs and to identify areas of opportunity for new materials and activities. K-12 formal, informal, and higher education products and activities are included in this analysis. 3) Finally, to address E/PO-related systemic issues and coordinate related activities across the four SMD science divisions. By supporting the NASA E/PO community and facilitating coordination of E/PO activities within and across disciplines, the SMD-Forum partnerships will

Advanced Durability and Damage Tolerance Design and Analysis Methods for Composite Structures: Lessons Learned from NASA Technology Development Programs

NASA Technical Reports Server (NTRS)

Harris, Charles E.; Starnes, James H., Jr.; Shuart, Mark J.

2003-01-01

Aerospace vehicles are designed to be durable and damage tolerant. Durability is largely an economic life-cycle design consideration whereas damage tolerance directly addresses the structural airworthiness (safety) of the vehicle. However, both durability and damage tolerance design methodologies must address the deleterious effects of changes in material properties and the initiation and growth of microstructural damage that may occur during the service lifetime of the vehicle. Durability and damage tolerance design and certification requirements are addressed for commercial transport aircraft and NASA manned spacecraft systems. The state-of-the-art in advanced design and analysis methods is illustrated by discussing the results of several recently completed NASA technology development programs. These programs include the NASA Advanced Subsonic Technology Program demonstrating technologies for large transport aircraft and the X-33 hypersonic test vehicle demonstrating technologies for a single-stage-to-orbit space launch vehicle.

Why formal learning theory matters for cognitive science.

PubMed

Fulop, Sean; Chater, Nick

2013-01-01

This article reviews a number of different areas in the foundations of formal learning theory. After outlining the general framework for formal models of learning, the Bayesian approach to learning is summarized. This leads to a discussion of Solomonoff's Universal Prior Distribution for Bayesian learning. Gold's model of identification in the limit is also outlined. We next discuss a number of aspects of learning theory raised in contributed papers, related to both computational and representational complexity. The article concludes with a description of how semi-supervised learning can be applied to the study of cognitive learning models. Throughout this overview, the specific points raised by our contributing authors are connected to the models and methods under review. Copyright © 2013 Cognitive Science Society, Inc.

Formal design specification of a Processor Interface Unit

NASA Technical Reports Server (NTRS)

Fura, David A.; Windley, Phillip J.; Cohen, Gerald C.

1992-01-01

This report describes work to formally specify the requirements and design of a processor interface unit (PIU), a single-chip subsystem providing memory-interface bus-interface, and additional support services for a commercial microprocessor within a fault-tolerant computer system. This system, the Fault-Tolerant Embedded Processor (FTEP), is targeted towards applications in avionics and space requiring extremely high levels of mission reliability, extended maintenance-free operation, or both. The need for high-quality design assurance in such applications is an undisputed fact, given the disastrous consequences that even a single design flaw can produce. Thus, the further development and application of formal methods to fault-tolerant systems is of critical importance as these systems see increasing use in modern society.

Generalized Bondi-Sachs equations for characteristic formalism of numerical relativity

NASA Astrophysics Data System (ADS)

Cao, Zhoujian; He, Xiaokai

2013-11-01

The Cauchy formalism of numerical relativity has been successfully applied to simulate various dynamical spacetimes without any symmetry assumption. But discovering how to set a mathematically consistent and physically realistic boundary condition is still an open problem for Cauchy formalism. In addition, the numerical truncation error and finite region ambiguity affect the accuracy of gravitational wave form calculation. As to the finite region ambiguity issue, the characteristic extraction method helps much. But it does not solve all of the above issues. Besides the above problems for Cauchy formalism, the computational efficiency is another problem. Although characteristic formalism of numerical relativity suffers the difficulty from caustics in the inner near zone, it has advantages in relation to all of the issues listed above. Cauchy-characteristic matching (CCM) is a possible way to take advantage of characteristic formalism regarding these issues and treat the inner caustics at the same time. CCM has difficulty treating the gauge difference between the Cauchy part and the characteristic part. We propose generalized Bondi-Sachs equations for characteristic formalism for the Cauchy-characteristic matching end. Our proposal gives out a possible same numerical evolution scheme for both the Cauchy part and the characteristic part. And our generalized Bondi-Sachs equations have one adjustable gauge freedom which can be used to relate the gauge used in the Cauchy part. Then these equations can make the Cauchy part and the characteristic part share a consistent gauge condition. So our proposal gives a possible new starting point for Cauchy-characteristic matching.

The Nuclear Energy Density Functional Formalism

NASA Astrophysics Data System (ADS)

Duguet, T.

The present document focuses on the theoretical foundations of the nuclear energy density functional (EDF) method. As such, it does not aim at reviewing the status of the field, at covering all possible ramifications of the approach or at presenting recent achievements and applications. The objective is to provide a modern account of the nuclear EDF formalism that is at variance with traditional presentations that rely, at one point or another, on a Hamiltonian-based picture. The latter is not general enough to encompass what the nuclear EDF method represents as of today. Specifically, the traditional Hamiltonian-based picture does not allow one to grasp the difficulties associated with the fact that currently available parametrizations of the energy kernel E[g',g] at play in the method do not derive from a genuine Hamilton operator, would the latter be effective. The method is formulated from the outset through the most general multi-reference, i.e. beyond mean-field, implementation such that the single-reference, i.e. "mean-field", derives as a particular case. As such, a key point of the presentation provided here is to demonstrate that the multi-reference EDF method can indeed be formulated in a mathematically meaningful fashion even if E[g',g] does not derive from a genuine Hamilton operator. In particular, the restoration of symmetries can be entirely formulated without making any reference to a projected state, i.e. within a genuine EDF framework. However, and as is illustrated in the present document, a mathematically meaningful formulation does not guarantee that the formalism is sound from a physical standpoint. The price at which the latter can be enforced as well in the future is eventually alluded to.

Formal and Non-Formal Digital Practices: Institutionalizing Transactional Learning Spaces in a Media Classroom

ERIC Educational Resources Information Center

de Lange, Thomas

2011-01-01

This article examines how a classroom procedure known as PGE (Plan/Go-through/Evaluate) group work aims at integrating formal and non-formal media experiences and practices into classroom-based media learning. The study displays, on the one hand, how PGE group work emerged and was institutionally embedded in a media course. On the other hand, the…

NASA Releases 'NASA App HD' for iPad

NASA Image and Video Library

2012-07-06

The NASA App HD invites you to discover a wealth of NASA information right on your iPad. The application collects, customizes and delivers an extensive selection of dynamically updated mission information, images, videos and Twitter feeds from various online NASA sources in a convenient mobile package. Come explore with NASA, now on your iPad. 2012 Updated Version - HD Resolution and new features. Original version published on Sept. 1, 2010.

The World Wide Web and Technology Transfer at NASA Langley Research Center

NASA Technical Reports Server (NTRS)

Nelson, Michael L.; Bianco, David J.

1994-01-01

NASA Langley Research Center (LaRC) began using the World Wide Web (WWW) in the summer of 1993, becoming the first NASA installation to provide a Center-wide home page. This coincided with a reorganization of LaRC to provide a more concentrated focus on technology transfer to both aerospace and non-aerospace industry. Use of the WWW and NCSA Mosaic not only provides automated information dissemination, but also allows for the implementation, evolution and integration of many technology transfer applications. This paper describes several of these innovative applications, including the on-line presentation of the entire Technology Opportunities Showcase (TOPS), an industrial partnering showcase that exists on the Web long after the actual 3-day event ended. During its first year on the Web, LaRC also developed several WWW-based information repositories. The Langley Technical Report Server (LTRS), a technical paper delivery system with integrated searching and retrieval, has proved to be quite popular. The NASA Technical Report Server (NTRS), an outgrowth of LTRS, provides uniform access to many logically similar, yet physically distributed NASA report servers. WWW is also the foundation of the Langley Software Server (LSS), an experimental software distribution system which will distribute LaRC-developed software with the possible phase-out of NASA's COSMIC program. In addition to the more formal technology distribution projects, WWW has been successful in connecting people with technologies and people with other people. With the completion of the LaRC reorganization, the Technology Applications Group, charged with interfacing with non-aerospace companies, opened for business with a popular home page.

14 CFR 1240.105 - Special procedures-NASA and NASA contractor employees.

Code of Federal Regulations, 2012 CFR

2012-01-01

... 14 Aeronautics and Space 5 2012-01-01 2012-01-01 false Special procedures-NASA and NASA contractor...—NASA and NASA contractor employees. (a) A NASA Headquarters office, a NASA field installation, or a NASA contractor may submit to the Board an application for an award identifying the originator(s) of...

14 CFR 1240.105 - Special procedures-NASA and NASA contractor employees.

Code of Federal Regulations, 2010 CFR

2010-01-01

... 14 Aeronautics and Space 5 2010-01-01 2010-01-01 false Special procedures-NASA and NASA contractor...—NASA and NASA contractor employees. (a) A NASA Headquarters office, a NASA field installation, or a NASA contractor may submit to the Board an application for an award identifying the originator(s) of...

14 CFR 1240.105 - Special procedures-NASA and NASA contractor employees.

Code of Federal Regulations, 2011 CFR

2011-01-01

... 14 Aeronautics and Space 5 2011-01-01 2010-01-01 true Special procedures-NASA and NASA contractor...—NASA and NASA contractor employees. (a) A NASA Headquarters office, a NASA field installation, or a NASA contractor may submit to the Board an application for an award identifying the originator(s) of...

NASA Earth Observations (NEO): Data Access for Informal Education and Outreach

NASA Technical Reports Server (NTRS)

Ward, Kevin; Herring, David

2005-01-01

The NEO (NASA Earth Observations) web space is currently under development with the goal of significantly increasing the demand for NASA remote sensing data while dramatically simplifying public access to georeferenced images. NEO will target the unsophisticated, nontraditional data users who are currently underserved by the existing data ordering systems. These users will include formal and informal educators, museum and science center personnel, professional communicators, and citizen scientists and amateur Earth observers. Users will be able to view and manipulate georeferenced browse imagery and, if they desire, download directly or order the source HDF data from the data provider (e.g., NASA DAAC or science team) via a single, integrated interface. NE0 will accomplish this goal by anticipating users expectations and knowledge level, thus providing an interface that presents material to users in a more simplified manner, without relying upon the jargon/technical terminology that make even the identification of the appropriate data set a significant hurdle. NEO will also act as a gateway that manages users expectations by providing specific details about images and data formats, developing tutorials regarding the manipulation of georeferenced imagery and raw data, links to software tools and ensuring that users are able to get the image they want in the format they want as easily as possible.

NASA Social

NASA Image and Video Library

2012-05-19

A NASA Social follower holds up a mobile device as NASA Administrator Charles Bolden, left, and Kennedy Space Center director Robert Cabana appear at the NASA Social event, Friday morning, May 19, 2012, at Kennedy Space Center in Cape Canaveral, Fla. About 50 NASA Social followers attended an event as part of activities surrounding the launch of Space Exploration Technologies, or SpaceX, demonstration mission of the company's Falcon 9 rocket to the International Space Station. Photo Credit: (NASA/Paul E. Alers)

Planning Non-Formal Education Curricula: The Case of Israel.

ERIC Educational Resources Information Center

Keller, Diana; Dror, Ilana

This paper compares the formal and non-formal education systems currently operating in Israel, describing the special features of curriculum planning in non-formal education. The central argument is that the non-formal education system fulfills functions that constitute a critique of the formal education system. The non-formal system offers the…

NASA Electronic Parts and Packaging Program

NASA Technical Reports Server (NTRS)

Kayali, Sammy

2000-01-01

NEPP program objectives are to: (1) Access the reliability of newly available electronic parts and packaging technologies for usage on NASA projects through validations, assessments, and characterizations, and the development of test methods/tools; (2)Expedite infusion paths for advanced (emerging) electronic parts and packaging technologies by evaluations of readiness for manufacturability and project usage consideration; (3) Provide NASA projects with technology selection, application, and validation guidelines for electronic parts and packaging hardware and processes; nd (4) Retain and disseminate electronic parts and packaging quality assurance, reliability validations, tools, and availability information to the NASA community.

Waste management in space: a NASA symposium. Special issue

NASA Technical Reports Server (NTRS)

Wydeven, T. (Principal Investigator)

1991-01-01

This special issue contains papers from the NASA Symposium on Waste Processing for Advanced Life Support, which was held at NASA Ames Research Center on September 11-13, 1990. Specialists in waste management from academia, government, and industry convened to exchange ideas and advise NASA in developing effective methods for waste management in a Controlled Ecological Life Support System (CELSS). Innovative and well-established methods were presented to assist in developing and managing wastes in closed systems for future long-duration space missions, especially missions to Mars.

The NASA/industry Design Analysis Methods for Vibrations (DAMVIBS) program: A government overview

NASA Technical Reports Server (NTRS)

Kvaternik, Raymond G.

1993-01-01

NASA-Langley, under the Design Analysis Methods for Vibrations (DAMVIBS) Program, set out in 1984 to establish the technology base needed by the rotorcraft industry for developing an advanced finite-element-based dynamics design analysis capability for vibrations. Considerable work has been done by the industry participants in the program since that time. Because the DAMVIBS Program is being phased out, a government/industry assessment of the program has been made to identify those accomplishments and contributions which may be ascribed to the program. The purpose of this paper is to provide an overview of the program and its accomplishments and contributions from the perspective of the government sponsoring organization.

Lights, Camera: Learning! Findings from studies of video in formal and informal science education

NASA Astrophysics Data System (ADS)

Borland, J.

2013-12-01

As part of the panel, media researcher, Jennifer Borland, will highlight findings from a variety of studies of videos across the spectrum of formal to informal learning, including schools, museums, and in viewers homes. In her presentation, Borland will assert that the viewing context matters a great deal, but there are some general take-aways that can be extrapolated to the use of educational video in a variety of settings. Borland has served as an evaluator on several video-related projects funded by NASA and the the National Science Foundation including: Data Visualization videos and Space Shows developed by the American Museum of Natural History, DragonflyTV, Earth the Operators Manual, The Music Instinct and Time Team America.

NASA Perspective on Requirements for Development of Advanced Methods Predicting Unsteady Aerodynamics and Aeroelasticity

NASA Technical Reports Server (NTRS)

Schuster, David M.

2008-01-01

Over the past three years, the National Aeronautics and Space Administration (NASA) has initiated design, development, and testing of a new human-rated space exploration system under the Constellation Program. Initial designs within the Constellation Program are scheduled to replace the present Space Shuttle, which is slated for retirement within the next three years. The development of vehicles for the Constellation system has encountered several unsteady aerodynamics challenges that have bearing on more traditional unsteady aerodynamic and aeroelastic analysis. This paper focuses on the synergy between the present NASA challenges and the ongoing challenges that have historically been the subject of research and method development. There are specific similarities in the flows required to be analyzed for the space exploration problems and those required for some of the more nonlinear unsteady aerodynamic and aeroelastic problems encountered on aircraft. The aggressive schedule, significant technical challenge, and high-priority status of the exploration system development is forcing engineers to implement existing tools and techniques in a design and application environment that is significantly stretching the capability of their methods. While these methods afford the users with the ability to rapidly turn around designs and analyses, their aggressive implementation comes at a price. The relative immaturity of the techniques for specific flow problems and the inexperience with their broad application to them, particularly on manned spacecraft flight system, has resulted in the implementation of an extensive wind tunnel and flight test program to reduce uncertainty and improve the experience base in the application of these methods. This provides a unique opportunity for unsteady aerodynamics and aeroelastic method developers to test and evaluate new analysis techniques on problems with high potential for acquisition of test and even flight data against which they

Measuring the economic returns from successful NASA life sciences technology transfers.

PubMed

Hertzfeld, Henry R

2002-12-01

ends, the formal relationship between the agency and the company also usually ends. However, the companies continue to use the prior connection to NASA for advertising and for developing new business partners. One recommendation of this study is for NASA to be more proactive with "alumni" companies and to help open additional financial and marketing doors for these companies.

Increasing patient safety and efficiency in transfusion therapy using formal process definitions.

PubMed

Henneman, Elizabeth A; Avrunin, George S; Clarke, Lori A; Osterweil, Leon J; Andrzejewski, Chester; Merrigan, Karen; Cobleigh, Rachel; Frederick, Kimberly; Katz-Bassett, Ethan; Henneman, Philip L

2007-01-01

The administration of blood products is a common, resource-intensive, and potentially problem-prone area that may place patients at elevated risk in the clinical setting. Much of the emphasis in transfusion safety has been targeted toward quality control measures in laboratory settings where blood products are prepared for administration as well as in automation of certain laboratory processes. In contrast, the process of transfusing blood in the clinical setting (ie, at the point of care) has essentially remained unchanged over the past several decades. Many of the currently available methods for improving the quality and safety of blood transfusions in the clinical setting rely on informal process descriptions, such as flow charts and medical algorithms, to describe medical processes. These informal descriptions, although useful in presenting an overview of standard processes, can be ambiguous or incomplete. For example, they often describe only the standard process and leave out how to handle possible failures or exceptions. One alternative to these informal descriptions is to use formal process definitions, which can serve as the basis for a variety of analyses because these formal definitions offer precision in the representation of all possible ways that a process can be carried out in both standard and exceptional situations. Formal process definitions have not previously been used to describe and improve medical processes. The use of such formal definitions to prospectively identify potential error and improve the transfusion process has not previously been reported. The purpose of this article is to introduce the concept of formally defining processes and to describe how formal definitions of blood transfusion processes can be used to detect and correct transfusion process errors in ways not currently possible using existing quality improvement methods.

20 CFR 702.336 - Formal hearings; new issues.

Code of Federal Regulations, 2010 CFR

2010-04-01

... 20 Employees' Benefits 3 2010-04-01 2010-04-01 false Formal hearings; new issues. 702.336 Section... Procedures Formal Hearings § 702.336 Formal hearings; new issues. (a) If, during the course of the formal hearing, the evidence presented warrants consideration of an issue or issues not previously considered...

Digital Resource Developments for Mathematics Education Involving Homework across Formal, Non-Formal and Informal Settings

ERIC Educational Resources Information Center

Radovic, Slaviša; Passey, Don

2016-01-01

The aim of this paper is to explore further an under-developed area--how drivers of curriculum, pedagogy and assessment conceptions and practices shape the creation and uses of technologically based resources to support mathematics learning across informal, non-formal and formal learning environments. The paper considers: the importance of…

The Interrelatedness of Formal, Non-Formal and Informal Learning: Evidence from Labour Market Program Participants

ERIC Educational Resources Information Center

Cameron, Roslyn; Harrison, Jennifer L.

2012-01-01

Definitions, differences and relationships between formal, non-formal and informal learning have long been contentious. There has been a significant change in language and reference from adult education to what amounts to forms of learning categorised by their modes of facilitation. Nonetheless, there is currently a renewed interest in the…

Technical Evaluation of the NASA Model for Cancer Risk to Astronauts Due to Space Radiation

NASA Technical Reports Server (NTRS)

2012-01-01

At the request of NASA, the National Research Council's (NRC's) Committee for Evaluation of Space Radiation Cancer Risk Model reviewed a number of changes that NASA proposes to make to its model for estimating the risk of radiation-induced cancer in astronauts. The NASA model in current use was last updated in 2005, and the proposed model would incorporate recent research directed at improving the quantification and understanding of the health risks posed by the space radiation environment. NASA's proposed model is defined by the 2011 NASA report Space Radiation Cancer Risk Projections and Uncertainties 2010 (Cucinotta et al., 2011). The committee's evaluation is based primarily on this source, which is referred to hereafter as the 2011 NASA report, with mention of specific sections or tables cited more formally as Cucinotta et al. (2011). The overall process for estimating cancer risks due to low linear energy transfer (LET) radiation exposure has been fully described in reports by a number of organizations. They include, more recently: (1) The "BEIR VII Phase 2" report from the NRC's Committee on Biological Effects of Ionizing Radiation (BEIR) (NRC, 2006); (2) Studies of Radiation and Cancer from the United Nations Scientific Committee on the Effects of Atomic Radiation (UNSCEAR, 2006), (3) The 2007 Recommendations of the International Commission on Radiological Protection (ICRP), ICRP Publication 103 (ICRP, 2007); and (4) The Environmental Protection Agency s (EPA s) report EPA Radiogenic Cancer Risk Models and Projections for the U.S. Population (EPA, 2011). The approaches described in the reports from all of these expert groups are quite similar. NASA's proposed space radiation cancer risk assessment model calculates, as its main output, age- and gender-specific risk of exposure-induced death (REID) for use in the estimation of mission and astronaut-specific cancer risk. The model also calculates the associated uncertainties in REID. The general approach for

Fairfield Plume Measurement and Analysis on the NASA-300M and NASA-300MS

NASA Technical Reports Server (NTRS)

Huang, Wensheng; Shastry, Rohit; Soulas, George C.; Kamhawi, Hani

2013-01-01

NASA is developing a 10- to 15-kW Hall thruster system to support future NASA missions. This activity is funded under the Space Technology Mission Directorate Solar Electric Propulsion Technology Demonstration Mission project. As a part of the development process, the NASA-300M, a 20-kW Hall thruster, was modified to incorporate the magnetic shielding concept and named the NASA-300MS. This activity was undertaken to assess the viability of using the magnetic shielding concept on a high-power Hall thruster to greatly reduce discharge channel erosion. This paper reports on the study to characterize the far-field plumes of the NASA-300M and NASA-300MS. Diagnostics deployed included a polarlyswept Faraday probe, a Wien filter (ExB probe), a retarding potential analyzer, and a Langmuir probe. During the study, a new, more accurate, integration method for analyzing Wien filter probe data was implemented and effect of secondary electron emission on the Faraday probe data was treated. Comparison of the diagnostic results from the two thrusters showed that the magnetically shielded version performed with 2 percent higher voltage utilization efficiency, 2 percent lower plume divergence efficiency, and 2 percent lower mass utilization efficiency compared to the baseline version. The net change in efficiency is within the aggregate measurement uncertainty so the overall performance is roughly equal for the two versions of the thruster. Anode efficiency calculated from thrust stand measurement corroborates this finding.

NASA Update

NASA Image and Video Library

2009-07-20

Alan Ladwig, Senior Advisor to the NASA Administrator, introduces Administrator Charles F. Bolden Jr. and Deputy Administrator Lori Garver at a NASA Update,Tuesday, July 21, 2009, at NASA Headquarters in Washington. Bolden, the agency's 12th Administrator and Garver took the time to introduce themselves and outline their vision for the agency going forward. No questions were taken during the session. Photo Credit: (NASA/Bill Ingalls)

NASA Social

NASA Image and Video Library

2011-05-18

Ed Mango, of the NASA Commercial Crew Office, speaks during a NASA Social, Friday, May 18, 2012, at Kennedy Space Center in Cape Canaveral, Fla. About 50 NASA Social followers attended an event as part of activities surrounding the launch of Space Exploration Technologies, or SpaceX, demonstration mission of the company's Falcon 9 rocket to the International Space Station. Photo Credit: (NASA/Paul E. Alers)

40 CFR 35.938-4 - Formal advertising.

Code of Federal Regulations, 2010 CFR

2010-07-01

... 40 Protection of Environment 1 2010-07-01 2010-07-01 false Formal advertising. 35.938-4 Section 35... advertising. Each contract shall be awarded after formal advertising, unless negotiation is permitted in accordance with § 35.936-18. Formal advertising shall be in accordance with the following: (a) Adequate...

40 CFR 35.938-4 - Formal advertising.

Code of Federal Regulations, 2011 CFR

2011-07-01

... 40 Protection of Environment 1 2011-07-01 2011-07-01 false Formal advertising. 35.938-4 Section 35... advertising. Each contract shall be awarded after formal advertising, unless negotiation is permitted in accordance with § 35.936-18. Formal advertising shall be in accordance with the following: (a) Adequate...

40 CFR 35.938-4 - Formal advertising.

Code of Federal Regulations, 2014 CFR

2014-07-01

... 40 Protection of Environment 1 2014-07-01 2014-07-01 false Formal advertising. 35.938-4 Section 35... advertising. Each contract shall be awarded after formal advertising, unless negotiation is permitted in accordance with § 35.936-18. Formal advertising shall be in accordance with the following: (a) Adequate...

40 CFR 35.938-4 - Formal advertising.

Code of Federal Regulations, 2012 CFR

2012-07-01

... 40 Protection of Environment 1 2012-07-01 2012-07-01 false Formal advertising. 35.938-4 Section 35... advertising. Each contract shall be awarded after formal advertising, unless negotiation is permitted in accordance with § 35.936-18. Formal advertising shall be in accordance with the following: (a) Adequate...

40 CFR 35.938-4 - Formal advertising.

Code of Federal Regulations, 2013 CFR

2013-07-01

... 40 Protection of Environment 1 2013-07-01 2013-07-01 false Formal advertising. 35.938-4 Section 35... advertising. Each contract shall be awarded after formal advertising, unless negotiation is permitted in accordance with § 35.936-18. Formal advertising shall be in accordance with the following: (a) Adequate...

NASA Utilization of the International Space Station and the Vision for Space Exploration

NASA Technical Reports Server (NTRS)

Robinson, Julie A.; Thumm, Tracy L.; Thomas, Donald A.

2006-01-01

In response to the U.S. President s Vision for Space Exploration (January 14, 2004), NASA has revised its utilization plans for ISS to focus on (1) research on astronaut health and the development of countermeasures that will protect our crews from the space environment during long duration voyages, (2) ISS as a test bed for research and technology developments that will insure vehicle systems and operational practices are ready for future exploration missions, (3) developing and validating operational practices and procedures for long-duration space missions. In addition, NASA will continue a small amount of fundamental research in life and microgravity sciences. There have been significant research accomplishments that are important for achieving the Exploration Vision. Some of these have been formal research payloads, while others have come from research based on the operation of International Space Station (ISS). We will review a selection of these experiments and results, as well as outline some of ongoing and upcoming research. The ISS represents the only microgravity opportunity to perform on-orbit long-duration studies of human health and performance and technologies relevant for future long-duration missions planned during the next 25 years. Even as NASA focuses on developing the Orion spacecraft and return to the moon (2015-2020), research on and operation of the ISS is fundamental to the success of NASA s Exploration Vision.

NASA Utilization of the International Space Station and the Vision for Space Exploration

NASA Technical Reports Server (NTRS)

Robinson, Julie A.; Thumm, Tracy L.; Thomas, Donald A.

2007-01-01

In response to the U.S. President s Vision for Space Exploration (January 14, 2004), NASA has revised its utilization plans for ISS to focus on (1) research on astronaut health and the development of countermeasures that will protect our crews from the space environment during long duration voyages, (2) ISS as a test bed for research and technology developments that will insure vehicle systems and operational practices are ready for future exploration missions, (3) developing and validating operational practices and procedures for long-duration space missions. In addition, NASA will continue a small amount of fundamental research in life and microgravity sciences. There have been significant research accomplishments that are important for achieving the Exploration Vision. Some of these have been formal research payloads, while others have come from research based on the operation of International Space Station (ISS). We will review a selection of these experiments and results, as well as outline some of ongoing and upcoming research. The ISS represents the only microgravity opportunity to perform on-orbit long-duration studies of human health and performance and technologies relevant for future long-duration missions planned during the next 25 years. Even as NASA focuses on developing the Orion spacecraft and return to the moon (2015-2020), research on and operation of the ISS is fundamental to the success of NASA s Exploration Vision.

NASA Utilization of the International Space Station and the Vision for Space Exploration

NASA Technical Reports Server (NTRS)

Robinson, Julie A.; Thomas, Donald A.; Thumm, Tracy L.

2006-01-01

In response to the U.S. President's Vision for Space Exploration (January 14, 2004), NASA has revised its utilization plans for ISS to focus on (1) research on astronaut health and the development of countermeasures that will protect our crews from the space environment during long duration voyages, (2) ISS as a test bed for research and technology developments that will insure vehicle systems and operational practices are ready for future exploration missions, (3) developing and validating operational practices and procedures for long-duration space missions. In addition, NASA will continue a small amount of fundamental research in life and microgravity sciences. There have been significant research accomplishments that are important for achieving the Exploration Vision. Some of these have been formal research payloads, while others have come from research based on the operation of International Space Station (ISS). We will review a selection of these experiments and results, as well as outline some of ongoing and upcoming research. The ISS represents the only microgravity opportunity to perform on-orbit long-duration studies of human health and performance and technologies relevant for future long-duration missions planned during the next 25 years. Even as NASA focuses on developing the Orion spacecraft and return to the moon (2015-2020), research on and operation of the ISS is fundamental to the success of NASA s Exploration Vision.

NASA's Lunar Robotic Architecture Study

NASA Astrophysics Data System (ADS)

Mulville, Daniel R.

2006-07-01

This report documents the findings and analysis of a 60-day agency-wide Lunar Robotic Architecture Study (LRAS) conducted by the National Aeronautics and Space Administration (NASA). Work on this study began in January 2006. Its purpose was to: Define a lunar robotics architecture by addressing the following issues: 1) Do we need robotic missions at all? If so, why and under what conditions? 2) How would they be accomplished and at what cost? Are they within budget? 3) What are the minimum requirements? What is the minimum mission set? 4) Integrate these elements together to show a viable robotic architecture. 5) Establish a strategic framework for a lunar robotics program. The LRAS Final Report presents analysis and recommendations concerning potential approaches related to NASA s implementation of the President's Vision for Space Exploration. Project and contract requirements will likely be derived in part from the LRAS analysis and recommendations contained herein, but these do not represent a set of project or contract requirements and are not binding on the U.S. Government unless and until they are formally and expressly adopted as such. Details of any recommendations offered by the LRAS Final Report will be translated into implementation requirements. Moreover, the report represents the assessments and projects of the report s authors at the time it was prepared; it is anticipated that the concepts in this report will be analyzed further and refined. By the time some of the activities addressed in this report are implemented, certain assumptions on which the report s conclusions are based will likely evolve as a result of this analysis. Accordingly, NASA, and any entity under contract with NASA, should not use the information in this report for final project direction. Since the conclusion of this study, there have been various changes to the Agency's current portfolio of lunar robotic precursor activities. First, the Robotic Lunar Exploration Program (RLEP

Application of Pressure-Based Wall Correction Methods to Two NASA Langley Wind Tunnels

NASA Technical Reports Server (NTRS)

Iyer, V.; Everhart, J. L.

2001-01-01

This paper is a description and status report on the implementation and application of the WICS wall interference method to the National Transonic Facility (NTF) and the 14 x 22-ft subsonic wind tunnel at the NASA Langley Research Center. The method calculates free-air corrections to the measured parameters and aerodynamic coefficients for full span and semispan models when the tunnels are in the solid-wall configuration. From a data quality point of view, these corrections remove predictable bias errors in the measurement due to the presence of the tunnel walls. At the NTF, the method is operational in the off-line and on-line modes, with three tests already computed for wall corrections. At the 14 x 22-ft tunnel, initial implementation has been done based on a test on a full span wing. This facility is currently scheduled for an upgrade to its wall pressure measurement system. With the addition of new wall orifices and other instrumentation upgrades, a significant improvement in the wall correction accuracy is expected.

Selling to NASA

NASA Technical Reports Server (NTRS)

1990-01-01

This handbook is designed to promote a better understanding of NASA's interests and the process of doing business with NASA. The document is divided into the following sections: (1) this is NASA; (2) the procurement process; (3) marketing your capabilities; (4) special assistance programs; (5) NASA field installations; (6) sources of additional help; (7) listing of NASA small/minority business personnel; and (8) NASA organization chart.

Understanding Informality and Formality in Learning.

ERIC Educational Resources Information Center

Colley, Helen; Hodkinson, Phil; Malcolm, Janice

2003-01-01

Reviews definitions of and debates over distinctions among formal, informal, and nonformal learning. Outlines questions about four aspects of formality/informality with which to analyze learning situations: process, location/setting, purposes, and content. (SK)

Formal Analysis of the Remote Agent Before and After Flight

NASA Technical Reports Server (NTRS)

Havelund, Klaus; Lowry, Mike; Park, SeungJoon; Pecheur, Charles; Penix, John; Visser, Willem; White, Jon L.

2000-01-01

This paper describes two separate efforts that used the SPIN model checker to verify deep space autonomy flight software. The first effort occurred at the beginning of a spiral development process and found five concurrency errors early in the design cycle that the developers acknowledge would not have been found through testing. This effort required a substantial manual modeling effort involving both abstraction and translation from the prototype LISP code to the PROMELA language used by SPIN. This experience and others led to research to address the gap between formal method tools and the development cycle used by software developers. The Java PathFinder tool which directly translates from Java to PROMELA was developed as part of this research, as well as automatic abstraction tools. In 1999 the flight software flew on a space mission, and a deadlock occurred in a sibling subsystem to the one which was the focus of the first verification effort. A second quick-response "cleanroom" verification effort found the concurrency error in a short amount of time. The error was isomorphic to one of the concurrency errors found during the first verification effort. The paper demonstrates that formal methods tools can find concurrency errors that indeed lead to loss of spacecraft functions, even for the complex software required for autonomy. Second, it describes progress in automatic translation and abstraction that eventually will enable formal methods tools to be inserted directly into the aerospace software development cycle.

Lifelong Learning to Empowerment: Beyond Formal Education

ERIC Educational Resources Information Center

Carr, Alexis; Balasubramanian, K.; Atieno, Rosemary; Onyango, James

2018-01-01

This paper discusses the relevance of lifelong learning vis-à-vis the Sustainable Development Goals (SDGs) and stresses the need for an approach blending formal education, non-formal and informal learning. The role of Open and Distance Learning (ODL) in moving beyond formal education and the importance of integrating pedagogy, andragogy and…

NASA Social

NASA Image and Video Library

2012-12-04

NASA astronaut Joe Acaba answers questions at a NASA Social at NASA Headquarters on Tuesday, Dec. 4, 2012 in Washington. Acaba launched to the International Space Station on a Russian Soyuz spacecraft May 15, 2012, spending 123 days aboard as a flight engineer of the Expedition 31 and 32 crews. He recently returned to Earth on Sept. 17 after four months in low earth orbit. Photo Credit: (NASA/Carla Cioffi)

Formal Symplectic Groupoid of a Deformation Quantization

NASA Astrophysics Data System (ADS)

Karabegov, Alexander V.

2005-08-01

We give a self-contained algebraic description of a formal symplectic groupoid over a Poisson manifold M. To each natural star product on M we then associate a canonical formal symplectic groupoid over M. Finally, we construct a unique formal symplectic groupoid ‘with separation of variables’ over an arbitrary Kähler-Poisson manifold.

Studies with the USF/NASA toxicity screening test method - Exercise wheels and oxygen replenishment

NASA Technical Reports Server (NTRS)

Hilado, C. J.; Cumming, H. J.

1977-01-01

Continuing efforts to improve the University of San Francisco/NASA toxicity screening test method have included the addition of exercise wheels to provide a different measure of incapacitation, and oxygen replenishment to offset any effect of oxygen depletion by the test animals. The addition of exercise wheels limited the number of animals in each test and doubled the required number of tests without any significant improvement in reproducibility. Oxygen replenishment appears to have an effect on survival in the last 5 minutes of the 30-minute test, but the effect is expected to be similar for most materials.

An Overview of NASA Biotechnology

NASA Technical Reports Server (NTRS)

Pusey, Marc L.

1997-01-01

Biotechnology research at NASA has comprised three separate areas; cell science and tissue culture, separations methods, and macromolecular crystal growth. This presentation will primarily focus on the macromolecular crystal growth.

NASA Future Forum

NASA Image and Video Library

2011-08-11

Dr. Laurie Leshin, NASA Deputy Associate Administrator Exploration Systems Mission Directortorate, second from right, speaks as Dr. Waleed Abdalati, NASA Chief Scientist, right, Dr. Robert Braun, NASA Chief Technologist, and Leland Melvin, Assoicate Administrator for NASA Education, far left, at the NASA Future Forum held at the Riggs Alumni Center on the campus of the University of Maryland, Thursday, Aug. 11, 2011 in College Park, Md. Photo Credit: (NASA/Paul E. Alers)

Graph-state formalism for mutually unbiased bases

NASA Astrophysics Data System (ADS)

Spengler, Christoph; Kraus, Barbara

2013-11-01

A pair of orthonormal bases is called mutually unbiased if all mutual overlaps between any element of one basis and an arbitrary element of the other basis coincide. In case the dimension, d, of the considered Hilbert space is a power of a prime number, complete sets of d+1 mutually unbiased bases (MUBs) exist. Here we present a method based on the graph-state formalism to construct such sets of MUBs. We show that for n p-level systems, with p being prime, one particular graph suffices to easily construct a set of pn+1 MUBs. In fact, we show that a single n-dimensional vector, which is associated with this graph, can be used to generate a complete set of MUBs and demonstrate that this vector can be easily determined. Finally, we discuss some advantages of our formalism regarding the analysis of entanglement structures in MUBs, as well as experimental realizations.

NASA Social

NASA Image and Video Library

2012-05-19

NASA Administrator Charles Bolden, left, and Kennedy Space Center director Robert Cabana appear at the NASA Social event, Friday morning, May 19, 2012, at Kennedy Space Center in Cape Canaveral, Fla. About 50 NASA Social followers attended an event as part of activities surrounding the launch of Space Exploration Technologies, or SpaceX, demonstration mission of the company's Falcon 9 rocket to the International Space Station. Photo Credit: (NASA/Paul E. Alers)

NASA Social

NASA Image and Video Library

2012-12-04

NASA astronaut Joe Acaba speaks at a behind-the-scenes NASA Social at NASA Headquarters on Tuesday, Dec. 4, 2012 in Washington. Acaba launched to the International Space Station on a Russian Soyuz spacecraft May 15, 2012, spending 123 days aboard as a flight engineer of the Expedition 31 and 32 crews. He recently returned to Earth on Sept. 17 after four months in low earth orbit. Photo Credit: (NASA/Carla Cioffi)

NASA Social

NASA Image and Video Library

2012-12-04

A NASA Social participant tweets during as astronaut Joe Acaba answers questions from the audience at NASA Headquaters, Tuesday, Dec. 4, 2012 in Washington. NASA astronaut Acaba launched to the ISS on a Russian Soyuz spacecraft May 15, 2012, spending 123 days aboard as a flight engineer of the Expedition 31 and 32 crews. He recently returned to Earth on Sept. 17 after four months in low earth orbit. Photo Credit: (NASA/Carla Cioffi)

NASA Social

NASA Image and Video Library

2012-12-04

NASA astronaut Joe Acaba answers questions at a behind-the-scenes NASA Social at NASA Headquarters on Tuesday, Dec. 4, 2012 in Washington. Acaba launched to the International Space Station on a Russian Soyuz spacecraft May 15, 2012, spending 123 days aboard as a flight engineer of the Expedition 31 and 32 crews. He recently returned to Earth on Sept. 17 after four months in low earth orbit. Photo Credit: (NASA/Carla Cioffi)

NASA Social

NASA Image and Video Library

2012-12-04

NASA astronaut Joe Acaba, center, greets participants at a behind-the-scenes NASA Social in Washington, Tuesday, Dec. 4, 2012 at NASA Headquarters. Acaba launched to the International Space Station on a Russian Soyuz spacecraft May 15, 2012, spending 123 days aboard as a flight engineer of the Expedition 31 and 32 crews. He recently returned to Earth on Sept. 17 after four months in low earth orbit. Photo Credit: (NASA/Carla Cioffi)

From Informal Safety-Critical Requirements to Property-Driven Formal Validation

NASA Technical Reports Server (NTRS)

Cimatti, Alessandro; Roveri, Marco; Susi, Angelo; Tonetta, Stefano

2008-01-01

Most of the efforts in formal methods have historically been devoted to comparing a design against a set of requirements. The validation of the requirements themselves, however, has often been disregarded, and it can be considered a largely open problem, which poses several challenges. The first challenge is given by the fact that requirements are often written in natural language, and may thus contain a high degree of ambiguity. Despite the progresses in Natural Language Processing techniques, the task of understanding a set of requirements cannot be automatized, and must be carried out by domain experts, who are typically not familiar with formal languages. Furthermore, in order to retain a direct connection with the informal requirements, the formalization cannot follow standard model-based approaches. The second challenge lies in the formal validation of requirements. On one hand, it is not even clear which are the correctness criteria or the high-level properties that the requirements must fulfill. On the other hand, the expressivity of the language used in the formalization may go beyond the theoretical and/or practical capacity of state-of-the-art formal verification. In order to solve these issues, we propose a new methodology that comprises of a chain of steps, each supported by a specific tool. The main steps are the following. First, the informal requirements are split into basic fragments, which are classified into categories, and dependency and generalization relationships among them are identified. Second, the fragments are modeled using a visual language such as UML. The UML diagrams are both syntactically restricted (in order to guarantee a formal semantics), and enriched with a highly controlled natural language (to allow for modeling static and temporal constraints). Third, an automatic formal analysis phase iterates over the modeled requirements, by combining several, complementary techniques: checking consistency; verifying whether the

ONERA-NASA Cooperative Effort on Liner Impedance Eduction

NASA Technical Reports Server (NTRS)

Primus, Julien; Piot, Estelle; Simon, Frank; Jones, Michael G.; Watson, Willie R

2013-01-01

As part of a cooperation between ONERA and NASA, the liner impedance eduction methods developed by the two research centers are compared. The NASA technique relies on an objective function built on acoustic pressure measurements located on the wall opposite the test liner, and the propagation code solves the convected Helmholtz equation in uniform ow using a finite element method that implements a continuous Galerkin discretization. The ONERA method uses an objective function based either on wall acoustic pressure or on acoustic velocity acquired above the liner by Laser Doppler Anemometry, and the propagation code solves the linearized Euler equations by a discontinuous Galerkin discretization. Two acoustic liners are tested in both ONERA and NASA ow ducts and the measured data are treated with the corresponding impedance eduction method. The first liner is a wire mesh facesheet mounted onto a honeycomb core, designed to be linear with respect to incident sound pressure level and to grazing ow velocity. The second one is a conventional, nonlinear, perforate-over-honeycomb single layer liner. Configurations without and with ow are considered. For the nonlinear liner, the comparison of liner impedance educed by NASA and ONERA shows a sensitivity to the experimental conditions, namely to the nature of the source and to the sample width.

Ontology or formal ontology

NASA Astrophysics Data System (ADS)

Žáček, Martin

2017-07-01

Ontology or formal ontology? Which word is correct? The aim of this article is to introduce correct terms and explain their basis. Ontology describes a particular area of interest (domain) in a formal way - defines the classes of objects that are in that area, and relationships that may exist between them. Meaning of ontology consists mainly in facilitating communication between people, improve collaboration of software systems and in the improvement of systems engineering. Ontology in all these areas offer the possibility of unification of view, maintaining consistency and unambiguity.

Flight Mechanics Experiment Onboard NASA's Zero Gravity Aircraft

ERIC Educational Resources Information Center

Matthews, Kyle R.; Motiwala, Samira A.; Edberg, Donald L.; García-Llama, Eduardo

2012-01-01

This paper presents a method to promote STEM (Science, Technology, Engineering, and Mathematics) education through participation in a reduced gravity program with NASA (National Aeronautics and Space Administration). Microgravity programs with NASA provide students with a unique opportunity to conduct scientific research with innovative and…

Bridging In-school and Out-of-school Learning: Formal, Non-Formal, and Informal Education

NASA Astrophysics Data System (ADS)

Eshach, Haim

2007-04-01

The present paper thoroughly examines how one can effectively bridge in-school and out-of-school learning. The first part discusses the difficulty in defining out-of-school learning. It proposes to distinguish three types of learning: formal, informal, and non-formal. The second part raises the question of whether out-of-school learning should be dealt with in the in-school system, in view of the fact that we experience informal learning anyway as well as considering the disadvantages and difficulties teachers are confronted with when planning and carrying out scientific fieldtrips. The voices of the teachers, the students, and the non-formal institution staff are heard to provide insights into the problem. The third part discusses the cognitive and affective aspects of non-formal learning. The fourth part presents some models explaining scientific fieldtrip learning and based on those models, suggests a novel explanation. The fifth part offers some recommendations of how to bridge in and out-of-school learning. The paper closes with some practical ideas as to how one can bring the theory described in the paper into practice. It is hoped that this paper will provide educators with an insight so that they will be able to fully exploit the great potential that scientific field trips may offer.

Acquisition of Formal Operations: The Effects of Two Training Procedures.

ERIC Educational Resources Information Center

Rosenthal, Doreen A.

1979-01-01

A study of 11- and 12-year-old girls indicates that either of two training procedures, method training or dimension training, can aid in the transition from concrete operational to formal operational thought by promoting a hypothesis-testing attitude. (BH)

E-assessment and an e-training program among elderly care staff lacking formal competence: results of a mixed-methods intervention study.

PubMed

Nilsson, Annika; Engström, Maria

2015-05-06

Among staff working in elderly care, a considerable proportion lack formal competence for their work. Lack of formal competence, in turn, has been linked to higher staff ratings of stress symptoms, sleep disturbances and workload. 1) To describe the strengths and weaknesses of an e-assessment and subsequent e-training program used among elderly care staff who lack formal competence and 2) to study the effects of an e-training program on staff members' working life (quality of care and psychological and structural empowerment) and well-being (job satisfaction and psychosomatic health). The hypothesis was that staff who had completed the e-assessment and the e-training program would rate greater improvements in working life and well-being than would staff who had only participated in the e-assessments. An intervention study with a mixed-methods approach using quantitative (2010-2011) and qualitative data (2011) was conducted in Swedish elderly care. Participants included a total of 41 staff members. To describe the strengths and weaknesses of the e-assessment and the e-training program, qualitative data were gathered using semi-structured interviews together with a study-specific questionnaire. To study the effects of the intervention, quantitative data were collected using questionnaires on: job satisfaction, psychosomatic health, psychological empowerment, structural empowerment and quality of care in an intervention and a comparison group. Staff who completed the e-assessments and the e-training program primarily experienced strengths associated with this approach. The results were also in line with our hypotheses: Staff who completed the e-assessment and the e-training program rated improvements in their working life and well-being. Use of the e-assessments and e-training program employed in the present study could be one way to support elderly care staff who lack formal education by increasing their competence; increased competence, in turn, could improve their

NASA's Radioisotope Power Systems Program Status

NASA Technical Reports Server (NTRS)

Dudzinski, Leonard A.; Hamley, John A.; McCallum, Peter W.; Sutliff, Thomas J.; Zakrajsek, June F.

2013-01-01

NASA's Radioisotope Power Systems (RPS) Program began formal implementation in December 2010. The RPS Program's goal is to make available RPS for the exploration of the solar system in environments where conventional solar or chemical power generation is impractical or impossible to meet mission needs. To meet this goal, the RPS Program manages investments in RPS system development and RPS technologies. The current keystone of the RPS Program is the development of the Advanced Stirling Radioisotope Generator (ASRG). This generator will be about four times more efficient than the more traditional thermoelectric generators, while providing a similar amount of power. This paper provides the status of the RPS Program and its related projects. Opportunities for RPS generator development and targeted research into RPS component performance enhancements, as well as constraints dealing with the supply of radioisotope fuel, are also discussed in the context of the next ten years of planetary science mission plans.

Rule acquisition in formal decision contexts based on formal, object-oriented and property-oriented concept lattices.

PubMed

Ren, Yue; Li, Jinhai; Aswani Kumar, Cherukuri; Liu, Wenqi

2014-01-01

Rule acquisition is one of the main purposes in the analysis of formal decision contexts. Up to now, there have been several types of rules in formal decision contexts such as decision rules, decision implications, and granular rules, which can be viewed as ∧-rules since all of them have the following form: "if conditions 1,2,…, and m hold, then decisions hold." In order to enrich the existing rule acquisition theory in formal decision contexts, this study puts forward two new types of rules which are called ∨-rules and ∨-∧ mixed rules based on formal, object-oriented, and property-oriented concept lattices. Moreover, a comparison of ∨-rules, ∨-∧ mixed rules, and ∧-rules is made from the perspectives of inclusion and inference relationships. Finally, some real examples and numerical experiments are conducted to compare the proposed rule acquisition algorithms with the existing one in terms of the running efficiency.

Rule Acquisition in Formal Decision Contexts Based on Formal, Object-Oriented and Property-Oriented Concept Lattices

PubMed Central

Ren, Yue; Aswani Kumar, Cherukuri; Liu, Wenqi

2014-01-01

Rule acquisition is one of the main purposes in the analysis of formal decision contexts. Up to now, there have been several types of rules in formal decision contexts such as decision rules, decision implications, and granular rules, which can be viewed as ∧-rules since all of them have the following form: “if conditions 1,2,…, and m hold, then decisions hold.” In order to enrich the existing rule acquisition theory in formal decision contexts, this study puts forward two new types of rules which are called ∨-rules and ∨-∧ mixed rules based on formal, object-oriented, and property-oriented concept lattices. Moreover, a comparison of ∨-rules, ∨-∧ mixed rules, and ∧-rules is made from the perspectives of inclusion and inference relationships. Finally, some real examples and numerical experiments are conducted to compare the proposed rule acquisition algorithms with the existing one in terms of the running efficiency. PMID:25165744

NASA's What's Up Astronomy and Mission video series celebrates the Year of the Solar System: Fall 2010 - late summer 2012

NASA Astrophysics Data System (ADS)

Houston Jones, J.; Alice Wessen, Manager Of Solar System Eduction; Public Engagement

2010-12-01

NASA's What's Up video podcast supports the Year of the Solar System (YSS) October 2010 - August 2012. During YSS each podcast pairs a popular night sky viewing target (Moon, Comet, Planets, solar system features) with a mission event (launch, flyby, orbit insertion, landing). This product has proven popular with public, formal and informal audiences and will compliment and augment other programming material.

NASA Future Forum

NASA Image and Video Library

2011-08-11

Dr. Robert Braun, NASA Chief Technologist, second from left, makes a point, as panelists Leland Melvin, Assoicate Administrator for NASA Education, left, Dr. Laurie Leshin, NASA Deputy Associate Administrator Exploration Systems Mission Directortorate, and Dr. Waleed Abdalati, NASA Chief Scientist, right, look on during a panel discussion at the NASA Future Forum held at the Riggs Alumni Center on the campus of the University of Maryland, Thursday, Aug. 11, 2011 in College Park, Md. Photo Credit: (NASA/Paul E. Alers)

NASA Hydrogen Peroxide Propellant Hazards Technical Manual

NASA Technical Reports Server (NTRS)

Baker, David L.; Greene, Ben; Frazier, Wayne

2005-01-01

The Fire, Explosion, Compatibility and Safety Hazards of Hydrogen Peroxide NASA technical manual was developed at the NASA Johnson Space Center White Sands Test Facility. NASA Technical Memorandum TM-2004-213151 covers topics concerning high concentration hydrogen peroxide including fire and explosion hazards, material and fluid reactivity, materials selection information, personnel and environmental hazards, physical and chemical properties, analytical spectroscopy, specifications, analytical methods, and material compatibility data. A summary of hydrogen peroxide-related accidents, incidents, dose calls, mishaps and lessons learned is included. The manual draws from art extensive literature base and includes recent applicable regulatory compliance documentation. The manual may be obtained by United States government agencies from NASA Johnson Space Center and used as a reference source for hazards and safe handling of hydrogen peroxide.

2008 NASA Seal/Secondary Air System Workshop

NASA Technical Reports Server (NTRS)

Steinetz, Bruce M. (Editor); Hendricks, Robert C. (Editor); Delgado, Irebert R. (Editor)

2009-01-01

The 2008 NASA Seal/Secondary Air System Workshop covered the following topics: (i) Overview of NASA s new Orion project aimed at developing a new spacecraft that will fare astronauts to the International Space Station, the Moon, Mars, and beyond; (ii) Overview of NASA s fundamental aeronautics technology project; (iii) Overview of NASA Glenn s seal project aimed at developing advanced seals for NASA s turbomachinery, space, and reentry vehicle needs; (iv) Reviews of NASA prime contractor, vendor, and university advanced sealing concepts, test results, experimental facilities, and numerical predictions; and (v) Reviews of material development programs relevant to advanced seals development. Turbine engine studies have shown that reducing seal leakage as well as high-pressure turbine (HPT) blade tip clearances will reduce fuel burn, lower emissions, retain exhaust gas temperature margin, and increase range. Turbine seal development topics covered include a method for fast-acting HPT blade tip clearance control, noncontacting low-leakage seals, intershaft seals, and a review of engine seal performance requirements for current and future Army engine platforms.

48 CFR 1816.202-70 - NASA contract clause.

Code of Federal Regulations, 2012 CFR

2012-10-01

... 48 Federal Acquisition Regulations System 6 2012-10-01 2012-10-01 false NASA contract clause. 1816.202-70 Section 1816.202-70 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND SPACE ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES TYPES OF CONTRACTS Fixed-Price Contracts 1816.202-70 NASA...

48 CFR 1813.302-570 - NASA solicitation provisions.

Code of Federal Regulations, 2014 CFR

2014-10-01

... 48 Federal Acquisition Regulations System 6 2014-10-01 2014-10-01 false NASA solicitation provisions. 1813.302-570 Section 1813.302-570 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND... Acquisition Methods 1813.302-570 NASA solicitation provisions. (a)(1) The contracting officer may use the...

48 CFR 1816.406-70 - NASA contract clauses.

Code of Federal Regulations, 2010 CFR

2010-10-01

... 48 Federal Acquisition Regulations System 6 2010-10-01 2010-10-01 true NASA contract clauses. 1816.406-70 Section 1816.406-70 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND SPACE ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES TYPES OF CONTRACTS Incentive Contracts 1816.406-70 NASA...

48 CFR 1816.406-70 - NASA contract clauses.

Code of Federal Regulations, 2012 CFR

2012-10-01

... 48 Federal Acquisition Regulations System 6 2012-10-01 2012-10-01 false NASA contract clauses. 1816.406-70 Section 1816.406-70 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND SPACE ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES TYPES OF CONTRACTS Incentive Contracts 1816.406-70 NASA...

48 CFR 1813.302-570 - NASA solicitation provisions.

Code of Federal Regulations, 2011 CFR

2011-10-01

... 48 Federal Acquisition Regulations System 6 2011-10-01 2011-10-01 false NASA solicitation provisions. 1813.302-570 Section 1813.302-570 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND... Acquisition Methods 1813.302-570 NASA solicitation provisions. (a)(1) The contracting officer may use the...

48 CFR 1816.406-70 - NASA contract clauses.

Code of Federal Regulations, 2011 CFR

2011-10-01

... 48 Federal Acquisition Regulations System 6 2011-10-01 2011-10-01 false NASA contract clauses. 1816.406-70 Section 1816.406-70 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND SPACE ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES TYPES OF CONTRACTS Incentive Contracts 1816.406-70 NASA...

48 CFR 1816.406-70 - NASA contract clauses.

Code of Federal Regulations, 2014 CFR

2014-10-01

... 48 Federal Acquisition Regulations System 6 2014-10-01 2014-10-01 false NASA contract clauses. 1816.406-70 Section 1816.406-70 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND SPACE ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES TYPES OF CONTRACTS Incentive Contracts 1816.406-70 NASA...

48 CFR 1816.202-70 - NASA contract clause.

Code of Federal Regulations, 2011 CFR

2011-10-01

... 48 Federal Acquisition Regulations System 6 2011-10-01 2011-10-01 false NASA contract clause. 1816.202-70 Section 1816.202-70 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND SPACE ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES TYPES OF CONTRACTS Fixed-Price Contracts 1816.202-70 NASA...

48 CFR 1813.302-570 - NASA solicitation provisions.

Code of Federal Regulations, 2012 CFR

2012-10-01

... 48 Federal Acquisition Regulations System 6 2012-10-01 2012-10-01 false NASA solicitation provisions. 1813.302-570 Section 1813.302-570 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND... Acquisition Methods 1813.302-570 NASA solicitation provisions. (a)(1) The contracting officer may use the...

48 CFR 1816.202-70 - NASA contract clause.

Code of Federal Regulations, 2010 CFR

2010-10-01

... 48 Federal Acquisition Regulations System 6 2010-10-01 2010-10-01 true NASA contract clause. 1816.202-70 Section 1816.202-70 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND SPACE ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES TYPES OF CONTRACTS Fixed-Price Contracts 1816.202-70 NASA...

48 CFR 1816.202-70 - NASA contract clause.

Code of Federal Regulations, 2014 CFR

2014-10-01

... 48 Federal Acquisition Regulations System 6 2014-10-01 2014-10-01 false NASA contract clause. 1816.202-70 Section 1816.202-70 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND SPACE ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES TYPES OF CONTRACTS Fixed-Price Contracts 1816.202-70 NASA...

48 CFR 1813.302-570 - NASA solicitation provisions.

Code of Federal Regulations, 2010 CFR

2010-10-01

... 48 Federal Acquisition Regulations System 6 2010-10-01 2010-10-01 true NASA solicitation provisions. 1813.302-570 Section 1813.302-570 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND... Acquisition Methods 1813.302-570 NASA solicitation provisions. (a)(1) The contracting officer may use the...

48 CFR 1816.202-70 - NASA contract clause.

Code of Federal Regulations, 2013 CFR

2013-10-01

... 48 Federal Acquisition Regulations System 6 2013-10-01 2013-10-01 false NASA contract clause. 1816.202-70 Section 1816.202-70 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND SPACE ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES TYPES OF CONTRACTS Fixed-Price Contracts 1816.202-70 NASA...

48 CFR 1816.406-70 - NASA contract clauses.

Code of Federal Regulations, 2013 CFR

2013-10-01

... 48 Federal Acquisition Regulations System 6 2013-10-01 2013-10-01 false NASA contract clauses. 1816.406-70 Section 1816.406-70 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND SPACE ADMINISTRATION CONTRACTING METHODS AND CONTRACT TYPES TYPES OF CONTRACTS Incentive Contracts 1816.406-70 NASA...

48 CFR 1813.302-570 - NASA solicitation provisions.

Code of Federal Regulations, 2013 CFR

2013-10-01

... 48 Federal Acquisition Regulations System 6 2013-10-01 2013-10-01 false NASA solicitation provisions. 1813.302-570 Section 1813.302-570 Federal Acquisition Regulations System NATIONAL AERONAUTICS AND... Acquisition Methods 1813.302-570 NASA solicitation provisions. (a)(1) The contracting officer may use the...

Evaluation Framework for NASA's Educational Outreach Programs

NASA Technical Reports Server (NTRS)

Berg, Rick; Booker, Angela; Linde, Charlotte; Preston, Connie

1999-01-01

The objective of the proposed work is to develop an evaluation framework for NASA's educational outreach efforts. We focus on public (rather than technical or scientific) dissemination efforts, specifically on Internet-based outreach sites for children.The outcome of this work is to propose both methods and criteria for evaluation, which would enable NASA to do a more analytic evaluation of its outreach efforts. The proposed framework is based on IRL's ethnographic and video-based observational methods, which allow us to analyze how these sites are actually used.

NASA Social

NASA Image and Video Library

2012-12-04

A participant at a NASA Social in Washington engages in social media as he listens to astronaut Joe Acaba answer questions, Tuesday, Dec. 4, 2012 at NASA Headquarters. NASA astronaut Joe Acaba launched to the International Space Station on a Russian Soyuz spacecraft May 15, 2012, spending 123 days aboard as a flight engineer of the Expedition 31 and 32 crews. He recently returned to Earth on Sept. 17 after four months in low earth orbit. Photo Credit: (NASA/Carla Cioffi)

NASA Social

NASA Image and Video Library

2012-12-04

A participant at a NASA Social in Washington listens to astronaut Joe Acaba answer questions about his time living aboard the International Space Station, Tuesday, Dec. 4, 2012 at NASA Headquarters. NASA astronaut Acaba launched to the ISS on a Russian Soyuz spacecraft May 15, 2012, spending 123 days aboard as a flight engineer of the Expedition 31 and 32 crews. He recently returned to Earth on Sept. 17 after four months in low earth orbit. Photo Credit: (NASA/Carla Cioffi)

ISS NASA Social

NASA Image and Video Library

2013-02-20

NASA Astronaut Don Pettit, speaks about his experience onboard the International Space Station at a NASA Social exploring science on the ISS at NASA Headquarters, Wednesday, Feb. 20, 2013 in Washington. Photo Credit: (NASA/Carla Cioffi)

NASA Astrophysics Technology Needs

NASA Technical Reports Server (NTRS)

Stahl, H. Philip

2012-01-01

July 2010, NASA Office of Chief Technologist (OCT) initiated an activity to create and maintain a NASA integrated roadmap for 15 key technology areas which recommend an overall technology investment strategy and prioritize NASA?s technology programs to meet NASA?s strategic goals. Science Instruments, Observatories and Sensor Systems(SIOSS) roadmap addresses technology needs to achieve NASA?s highest priority objectives -- not only for the Science Mission Directorate (SMD), but for all of NASA.

Community Garden: A Bridging Program between Formal and Informal Learning

ERIC Educational Resources Information Center

Datta, Ranjan

2016-01-01

Community garden activities can play a significant role in bridging formal and informal learning, particularly in urban children's science and environmental education. It promotes relational methods of learning, discussing, and practicing that will integrate food security, social interactions, community development, environmental activism, and…

Structuring the formal definition of Ada

NASA Technical Reports Server (NTRS)

Hansen, Kurt W.

1986-01-01

The structure of the formal definition of Ada are described. At present, a difficult subset of Ada has been defined and the experience gained so far by this work is reported. Currently, the work continues towards the formal definition of the Ada language.

Modeling formalisms in Systems Biology

PubMed Central

2011-01-01

Systems Biology has taken advantage of computational tools and high-throughput experimental data to model several biological processes. These include signaling, gene regulatory, and metabolic networks. However, most of these models are specific to each kind of network. Their interconnection demands a whole-cell modeling framework for a complete understanding of cellular systems. We describe the features required by an integrated framework for modeling, analyzing and simulating biological processes, and review several modeling formalisms that have been used in Systems Biology including Boolean networks, Bayesian networks, Petri nets, process algebras, constraint-based models, differential equations, rule-based models, interacting state machines, cellular automata, and agent-based models. We compare the features provided by different formalisms, and discuss recent approaches in the integration of these formalisms, as well as possible directions for the future. PMID:22141422

On the formalization and reuse of scientific research.

PubMed

King, Ross D; Liakata, Maria; Lu, Chuan; Oliver, Stephen G; Soldatova, Larisa N

2011-10-07

The reuse of scientific knowledge obtained from one investigation in another investigation is basic to the advance of science. Scientific investigations should therefore be recorded in ways that promote the reuse of the knowledge they generate. The use of logical formalisms to describe scientific knowledge has potential advantages in facilitating such reuse. Here, we propose a formal framework for using logical formalisms to promote reuse. We demonstrate the utility of this framework by using it in a worked example from biology: demonstrating cycles of investigation formalization [F] and reuse [R] to generate new knowledge. We first used logic to formally describe a Robot scientist investigation into yeast (Saccharomyces cerevisiae) functional genomics [f(1)]. With Robot scientists, unlike human scientists, the production of comprehensive metadata about their investigations is a natural by-product of the way they work. We then demonstrated how this formalism enabled the reuse of the research in investigating yeast phenotypes [r(1) = R(f(1))]. This investigation found that the removal of non-essential enzymes generally resulted in enhanced growth. The phenotype investigation was then formally described using the same logical formalism as the functional genomics investigation [f(2) = F(r(1))]. We then demonstrated how this formalism enabled the reuse of the phenotype investigation to investigate yeast systems-biology modelling [r(2) = R(f(2))]. This investigation found that yeast flux-balance analysis models fail to predict the observed changes in growth. Finally, the systems biology investigation was formalized for reuse in future investigations [f(3) = F(r(2))]. These cycles of reuse are a model for the general reuse of scientific knowledge.

The Influence of Rural Location on Utilization of Formal Home Care: The Role of Medicaid

ERIC Educational Resources Information Center

McAuley, William J.; Spector, William D.; Van Nostrand, Joan; Shaffer, Tom

2004-01-01

Purpose: This research examines the impact of rural-urban residence on formal home-care utilization among older people and determines whether and how Medicaid coverage influences the association between, rural-urban location and risk of formal home-care use. Design and Methods: We combined data from the 1998 consolidated file of the Medical…

NASA Social

NASA Image and Video Library

2012-12-04

A participant at a NASA Social in Washington tweets as he listens to astronaut Joe Acaba answer questions about his time living aboard the International Space Station, Tuesday, Dec. 4, 2012 at NASA Headquarters. NASA astronaut Joe Acaba launched to the ISS on a Russian Soyuz spacecraft May 15, 2012, spending 123 days aboard as a flight engineer of the Expedition 31 and 32 crews. He recently returned to Earth on Sept. 17 after four months in low earth orbit. Photo Credit: (NASA/Carla Cioffi)

REQUIREMENTS PATTERNS FOR FORMAL CONTRACTS IN ARCHITECTURAL ANALYSIS AND DESIGN LANGUAGE (AADL) MODELS

DTIC Science & Technology

2017-04-17

Cyberphysical Systems, Formal Methods , Requirements Patterns, AADL, Assume Guarantee Reasoning Environment 16. SECURITY CLASSIFICATION OF: 17. LIMITATION OF...5 3. Methods , Assumptions, and Procedures...Rockwell Collins has been addressing these challenges by developing compositional reasoning methods that permit the verification of systems that exceed

NASA historical data book. Volume 4: NASA resources 1969-1978

NASA Technical Reports Server (NTRS)

Gawdiak, Ihor Y.; Fedor, Helen

1994-01-01

This is Volume 4, NASA Resources 1969-1978, of a series providing a 20-year statistical summary of NASA programs. This series is an important component of NASA published historical reference works, used by NASA personnel, managers, external researchers, and other government agencies. This volume combines statistical data of the component facilities with the data of the parent installation.

NASA historical data book. Volume 1: NASA resources 1958-1968

NASA Technical Reports Server (NTRS)

Vannimmen, Jane; Bruno, Leonard C.; Rosholt, Robert L.

1988-01-01

This is Volume 1, NASA Resources 1958-1968, of a multi-volume series providing a 20-year compilation of summary statistical and other data descriptive of NASA's programs in aeronautics and manned and unmanned spaceflight. This series is an important component of NASA published historical reference works, used by NASA personnel, managers, external researchers, and other government agencies.

37 CFR 251.41 - Formal hearings.

Code of Federal Regulations, 2010 CFR

2010-07-01

... ARBITRATION ROYALTY PANEL RULES AND PROCEDURES COPYRIGHT ARBITRATION ROYALTY PANEL RULES OF PROCEDURE Procedures of Copyright Arbitration Royalty Panels § 251.41 Formal hearings. (a) The formal hearings that will be conducted under the rules of this subpart are rate adjustment hearings and royalty fee...

Adolescent Learning in the Zoo: Embedding a Non-Formal Learning Environment to Teach Formal Aspects of Vertebrate Biology

NASA Astrophysics Data System (ADS)

Randler, Christoph; Kummer, Barbara; Wilhelm, Christian

2012-06-01

The aim of this study was to assess the outcome of a zoo visit in terms of learning and retention of knowledge concerning the adaptations and behavior of vertebrate species. Basis of the work was the concept of implementing zoo visits as an out-of-school setting for formal, curriculum based learning. Our theoretical framework centers on the self-determination theory, therefore, we used a group-based, hands-on learning environment. To address this questions, we used a treatment—control design (BACI) with different treatments and a control group. Pre-, post- and retention tests were applied. All treatments led to a substantial increase of learning and retention knowledge compared to the control group. Immediately after the zoo visit, the zoo-guide tour provided the highest scores, while after a delay of 6 weeks, the learner-centered environment combined with a teacher-guided summarizing scored best. We suggest incorporating the zoo as an out-of-school environment into formal school learning, and we propose different methods to improve learning in zoo settings.

NASA's Education Program

NASA Technical Reports Server (NTRS)

1993-01-01

NASA's current education programs, which will be examined under its Strategic Plan for Education are presented. It is NASA's first goal to maintain this base - revising, expanding, or eliminating programs as necessary. Through NASA's second goal, new education reform initiatives will be added which specifically address NASA mission requirements, national educational reform, and Federal Coordinating Council for Science, Engineering, and Technology (FCCSET) priorities. The chapters in this publication are divided by educational levels, with additional sections on programs to improve the technological competence of students and on an array of NASA published materials to supplement programs. The resource section lists NASA's national and regional Teacher Resource Centers and introduces the reader to NASA's Central Operation of Resources for Educators (CORE), which distributes materials in audiovisual format.

20 CFR 702.341 - Formal hearings; depositions; interrogatories.

Code of Federal Regulations, 2010 CFR

2010-04-01

... 20 Employees' Benefits 3 2010-04-01 2010-04-01 false Formal hearings; depositions; interrogatories... Adjudication Procedures Formal Hearings § 702.341 Formal hearings; depositions; interrogatories. The testimony of any witness, including any party represented by counsel, may be taken by deposition or...

20 CFR 702.341 - Formal hearings; depositions; interrogatories.

Code of Federal Regulations, 2011 CFR

2011-04-01

... 20 Employees' Benefits 3 2011-04-01 2011-04-01 false Formal hearings; depositions; interrogatories... PROCEDURE Adjudication Procedures Formal Hearings § 702.341 Formal hearings; depositions; interrogatories. The testimony of any witness, including any party represented by counsel, may be taken by deposition...

Evaluation of light extraction efficiency for the light-emitting diodes based on the transfer matrix formalism and ray-tracing method

NASA Astrophysics Data System (ADS)

Pingbo, An; Li, Wang; Hongxi, Lu; Zhiguo, Yu; Lei, Liu; Xin, Xi; Lixia, Zhao; Junxi, Wang; Jinmin, Li

2016-06-01

The internal quantum efficiency (IQE) of the light-emitting diodes can be calculated by the ratio of the external quantum efficiency (EQE) and the light extraction efficiency (LEE). The EQE can be measured experimentally, but the LEE is difficult to calculate due to the complicated LED structures. In this work, a model was established to calculate the LEE by combining the transfer matrix formalism and an in-plane ray tracing method. With the calculated LEE, the IQE was determined and made a good agreement with that obtained by the ABC model and temperature-dependent photoluminescence method. The proposed method makes the determination of the IQE more practical and conventional. Project supported by the National Natural Science Foundation of China (Nos.11574306, 61334009), the China International Science and Technology Cooperation Program (No. 2014DFG62280), and the National High Technology Program of China (No. 2015AA03A101).

ISS NASA Social

NASA Image and Video Library

2013-02-20

Marshall Porterfield, Life and Physical Sciences Division Director at NASA Headquarters, talks about the human body in microgravity and other life sciences at a NASA Social exploring science on the ISS at NASA Headquarters, Wednesday, Feb. 20, 2013 in Washington. Photo Credit: (NASA/Carla Cioffi)

ISS NASA Social

NASA Image and Video Library

2013-02-20

A NASA Social participant asks a question to the astronauts onboard the International Space Station in a live downlink from the ISS at a NASA Social exploring science on the ISS at NASA Headquarters, Wednesday, Feb. 20, 2013 in Washington. Photo Credit: (NASA/Carla Cioffi)

Products of composite operators in the exact renormalization group formalism

NASA Astrophysics Data System (ADS)

Pagani, C.; Sonoda, H.

2018-02-01

We discuss a general method of constructing the products of composite operators using the exact renormalization group formalism. Considering mainly the Wilson action at a generic fixed point of the renormalization group, we give an argument for the validity of short-distance expansions of operator products. We show how to compute the expansion coefficients by solving differential equations, and test our method with some simple examples.

Male-Female Differences in Formal Thought.

ERIC Educational Resources Information Center

Linn, Marcia C.

Two studies were conducted to clarify the influence of experiences and aptitudes on male-female differences in formal thought. Participants were 788 seventh-, ninth-, and eleventh-graders in three school districts differing in location, socioeconomic composition, and course offerings. Formal thought was measured with tasks involving proportional…

Propellant for the NASA Standard Initiator

NASA Technical Reports Server (NTRS)

Hohmann, Carl; Tipton, Bill, Jr.; Dutton, Maureen

2000-01-01

This paper discusses processes employed in manufacturing zirconium-potassium perchlorate propellant for the NASA standard initiator. It provides both a historical background on the NSI device-detailing problem areas and their resolution--and on propellant blending techniques. Emphasis is placed on the precipitation blending method. The findings on mixing equipment, processing, and raw materials are described. Also detailed are findings on the bridgewire slurry operation, one of the critical steps in the production of the NASA standard initiator.

Bayesian Inference for NASA Probabilistic Risk and Reliability Analysis

NASA Technical Reports Server (NTRS)

Dezfuli, Homayoon; Kelly, Dana; Smith, Curtis; Vedros, Kurt; Galyean, William

2009-01-01

This document, Bayesian Inference for NASA Probabilistic Risk and Reliability Analysis, is intended to provide guidelines for the collection and evaluation of risk and reliability-related data. It is aimed at scientists and engineers familiar with risk and reliability methods and provides a hands-on approach to the investigation and application of a variety of risk and reliability data assessment methods, tools, and techniques. This document provides both: A broad perspective on data analysis collection and evaluation issues. A narrow focus on the methods to implement a comprehensive information repository. The topics addressed herein cover the fundamentals of how data and information are to be used in risk and reliability analysis models and their potential role in decision making. Understanding these topics is essential to attaining a risk informed decision making environment that is being sought by NASA requirements and procedures such as 8000.4 (Agency Risk Management Procedural Requirements), NPR 8705.05 (Probabilistic Risk Assessment Procedures for NASA Programs and Projects), and the System Safety requirements of NPR 8715.3 (NASA General Safety Program Requirements).

NASA strategic plan

NASA Technical Reports Server (NTRS)

1994-01-01

The NASA Strategic Plan is a living document. It provides far-reaching goals and objectives to create stability for NASA's efforts. The Plan presents NASA's top-level strategy: it articulates what NASA does and for whom; it differentiates between ends and means; it states where NASA is going and what NASA intends to do to get there. This Plan is not a budget document, nor does it present priorities for current or future programs. Rather, it establishes a framework for shaping NASA's activities and developing a balanced set of priorities across the Agency. Such priorities will then be reflected in the NASA budget. The document includes vision, mission, and goals; external environment; conceptual framework; strategic enterprises (Mission to Planet Earth, aeronautics, human exploration and development of space, scientific research, space technology, and synergy); strategic functions (transportation to space, space communications, human resources, and physical resources); values and operating principles; implementing strategy; and senior management team concurrence.

14 CFR 302.404 - Formal complaints.

Code of Federal Regulations, 2010 CFR

2010-01-01

... 14 Aeronautics and Space 4 2010-01-01 2010-01-01 false Formal complaints. 302.404 Section 302.404 Aeronautics and Space OFFICE OF THE SECRETARY, DEPARTMENT OF TRANSPORTATION (AVIATION PROCEEDINGS) PROCEDURAL... business or the ends of justice. (e) Service. A formal complaint, and any amendments thereto, shall be...

NASA Safety Manual. Volume 3: System Safety

NASA Technical Reports Server (NTRS)

1970-01-01

This Volume 3 of the NASA Safety Manual sets forth the basic elements and techniques for managing a system safety program and the technical methods recommended for use in developing a risk evaluation program that is oriented to the identification of hazards in aerospace hardware systems and the development of residual risk management information for the program manager that is based on the hazards identified. The methods and techniques described in this volume are in consonance with the requirements set forth in NHB 1700.1 (VI), Chapter 3. This volume and future volumes of the NASA Safety Manual shall not be rewritten, reprinted, or reproduced in any manner. Installation implementing procedures, if necessary, shall be inserted as page supplements in accordance with the provisions of Appendix A. No portion of this volume or future volumes of the NASA Safety Manual shall be invoked in contracts.

NASA's Use of Human Behavior Models for Concept Development and Evaluation

NASA Technical Reports Server (NTRS)

Gore, Brian F.

2012-01-01

Overview of NASA's use of computational approaches and methods to support research goals, of human performance models, with a focus on examples of the methods used in Code TH and TI at NASA Ames, followed by an in depth review of MIDAS' current FAA work.

Formal Techniques for Synchronized Fault-Tolerant Systems

NASA Technical Reports Server (NTRS)

DiVito, Ben L.; Butler, Ricky W.

1992-01-01

We present the formal verification of synchronizing aspects of the Reliable Computing Platform (RCP), a fault-tolerant computing system for digital flight control applications. The RCP uses NMR-style redundancy to mask faults and internal majority voting to purge the effects of transient faults. The system design has been formally specified and verified using the EHDM verification system. Our formalization is based on an extended state machine model incorporating snapshots of local processors clocks.

Open NASA Earth Exchange (OpenNEX): A Public-Private Partnership for Climate Change Research

NASA Astrophysics Data System (ADS)

Nemani, R. R.; Lee, T. J.; Michaelis, A.; Ganguly, S.; Votava, P.

2014-12-01

NASA Earth Exchange (NEX) is a data, computing and knowledge collaborative that houses satellite, climate and ancillary data where a community of researchers can come together to share modeling and analysis codes, scientific results, knowledge and expertise on a centralized platform with access to large supercomputing resources. As a part of broadening the community beyond NASA-funded researchers, NASA through an agreement with Amazon Inc. made available to the public a large collection of Climate and Earth Sciences satellite data. The data, available through the Open NASA Earth Exchange (OpenNEX) platform hosted by Amazon Web Services (AWS) public cloud, consists of large amounts of global land surface imaging, vegetation conditions, climate observations and climate projections. In addition to the data, users of OpenNEX platform can also watch lectures from leading experts, learn basic access and use of the available data sets. In order to advance White House initiatives such as Open Data, Big Data and Climate Data and the Climate Action Plan, NASA over the past six months conducted the OpenNEX Challenge. The two-part challenge was designed to engage the public in creating innovative ways to use NASA data and address climate change impacts on economic growth, health and livelihood. Our intention was that the challenges allow citizen scientists to realize the value of NASA data assets and offers NASA new ideas on how to share and use that data. The first "ideation" challenge, closed on July 31st attracted over 450 participants consisting of climate scientists, hobbyists, citizen scientists, IT experts and App developers. Winning ideas from the first challenge will be incorporated into the second "builder" challenge currently targeted to launch mid-August and close by mid-November. The winner(s) will be formally announced at AGU in December of 2014. We will share our experiences and lessons learned over the past year from OpenNEX, a public-private partnership for

Issues in NASA program and project management

NASA Technical Reports Server (NTRS)

Hoffman, Edward J. (Editor)

1994-01-01

This volume is the eighth in an ongoing series addressing current topics and lessons learned in NASA program and project management. Articles in this volume cover the following topics: (1) power sources for the Galileo and Ulysses Missions; (2) managing requirements; (3) program control of the Tropical Rainfall Measuring Mission; (4) project management method; (5) career development for project managers; and (6) resources for NASA managers.