ALBERT

Description: The radiation chemistry, thermal stability, and vapor pressure of solid-phase carbonic acid (H2CO3) have been studied with mid-infrared spectroscopy. A new procedure for measuring this molecule's radiation stability has been used to obtain intrinsic IR band strengths and half-lives for radiolytic destruction. Results are compared to literature values. We report, for the first time, measurements of carbonic acid's vapor pressure and its heat of sublimation. We also report the first observation of a chemical reaction involving solid-phase carbonic acid. Possible applications of these findings are discussed, with an emphasis on the outer Solar System.

Description: We report on the application of an off-the-shelf verification platform to the RC4 stream cipher cryptographic software implementation (as available in the openSSL library), and introduce a deductive verification technique based on self-composition for proving the absence of error propagation.

Description: The EU Mobius project has been concerned with the security of Java applications, and of mobile devices such as smart phones that execute such applications. In this talk, I'll give a brief overview of the results obtained on on-device checking of various security-related program properties. I'll then describe in more detail how the concept of certified abstract interpretation and abstraction-carrying code can be applied to polyhedral-based analysis of Java byte code in order to verify properties pertaining to the usage of resources of a down-loaded application. Particular emphasis has been on finding ways of reducing the size of the certificates that accompany a piece of code.

Description: In this paper, we propose a proof-carrying code framework for program-generators. The enabling technique is abstract parsing, a static string analysis technique, which is used as a component for generating and validating certificates. Our framework provides an efficient solution for certifying program-generators whose safety properties are expressed in terms of the grammar representing the generated program. The fixed-point solution of the analysis is generated and attached with the program-generator on the code producer side. The consumer receives the code with a fixed-point solution and validates that the received fixed point is indeed a fixed point of the received code. This validation can be done in a single pass.

Description: We outline some conceptual challenges in extending the PCC paradigm to a concurrent and distributed setting, and sketch a generalized notion of module correctness based on viewing communication contracts as economic games. The model supports compositional reasoning about modular systems and is meant to apply not only to certification of executable code, but also of organizational workflows.

Description: 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.

Description: ISS SSP 50184 HRDL optical fiber communication subsystem, has system level requirements that were changed to accommodate large loss optical fiber links previously installed. SSQ22680 design is difficult to implement, no metal shell over socket/pin combination to protect the weak part of the pin. Additions to ISS are planned for the future. AVIM still used for interconnection in space flight applications without incident. Thermal cycling resulted in less than 0.25 dB max change in Insertion Loss for all types during cycling, nominal as compared to the AVIM. Vibration testing results conclusion; no significant changes, nominal as compared to AVIM.

Description: We investigated variations in the sensitivity of surface ozone formation in summer to precursor species concentrations of volatile organic compounds (VOCs) and nitrogen oxides (NO(x)) as inferred from the ratio of tropospheric columns of formaldehyde and nitrogen dioxide from the Aura Ozone Monitoring Instrument (OMI). The data indicate that ozone formation became: 1. more sensitive to NO(x) over most of the U.S, from 2005 to 2007 because of substantial decreases in NO(x) emissions primarily from stationary sources, and 2. more sensitive to NO(x) with increasing temperature, in part because emissions of highly reactive, biogenic isoprene increase with temperature, thus increasing the total VOC reactivity. Based on our interpretation of the data, current strategies implemented to reduce unhealthy levels of surface ozone should focus more on reducing NO(x) emissions, except in some downtown areas which have historically benefited from reductions in VOC emissions.

Description: The correctness of safety-critical embedded software is crucial, whereas non-functional properties like deadlock-freedom and real-time constraints are particularly important. The real-time calculus Timed Communicating Sequential Processes (CSP) is capable of expressing such properties and can therefore be used to verify embedded software. In this paper, we present our formalization of Timed CSP in the Isabelle/HOL theorem prover, which we have formulated as an operational coalgebraic semantics together with bisimulation equivalences and coalgebraic invariants. Furthermore, we apply these techniques in an abstract specification with real-time constraints, which is the basis for current work in which we verify the components of a simple real-time operating system deployed on a satellite.

Description: We present jFuzz, a automatic testing tool for Java programs. jFuzz is a concolic whitebox fuzzer, built on the NASA Java PathFinder, an explicit-state Java model checker, and a framework for developing reliability and analysis tools for Java. Starting from a seed input, jFuzz automatically and systematically generates inputs that exercise new program paths. jFuzz uses a combination of concrete and symbolic execution, and constraint solving. Time spent on solving constraints can be significant. We implemented several well-known optimizations and name-independent caching, which aggressively normalizes the constraints to reduce the number of calls to the constraint solver. We present preliminary results due to the optimizations, and demonstrate the effectiveness of jFuzz in creating good test inputs. The source code of jFuzz is available as part of the NASA Java PathFinder. jFuzz is intended to be a research testbed for investigating new testing and analysis techniques based on concrete and symbolic execution. The source code of jFuzz is available as part of the NASA Java PathFinder.

Description: The transition of space weather models or of information derived from space weather models to space weather forecasting is the last step of the chain from model development to model deployment in forecasting operations. As such, it is an extremely important element of the quest to increase our national capability to forecast and mitigate space weather hazards. It involves establishing customer requirements, and analyses of available models, which are, in principle, capable of delivering the required product. Models will have to be verified and validated prior to a selection of the best performing model. Further considerations include operational hardware, and the availability of data streams to drive the model. The final steps include the education of forecasters, and the implementation on gateway hardware prior to operational use. This presentation will provide a discussion of opportunities for rapid progress from the viewpoint of the Community Coordinated Modeling Center.

Description: NASA s Desert Research and Technology Studies (D-RATS) field test is a demonstration that combines operations development, technology advances and science in analog planetary surface conditions. The focus is testing preliminary operational concepts for extravehicular activity (EVA) systems by providing hands-on experience with simulated surface operations and EVA hardware and procedures. The DRATS activities also develop technical skills and experience for the engineers, scientists, technicians, and astronauts responsible for realizing the goals of the Lunar Surface Systems Program. The 2009 test is the twelfth for the D-RATS team.

Description: Orbital debris represents a significant and increasing risk to operational spacecraft. Here we report on photometric observations made in standard BVRI filters at the Cerro Tololo Inter-American Observatory (CTIO) in an effort to determine the physical characteristics of optically faint debris at geosynchronous Earth orbit (GEO). Our sample is taken from GEO objects discovered in a survey with the University of Michigan s 0.6-m Curtis-Schmidt telescope (known as MODEST, for Michigan Orbital DEbris Survey Telescope), and then followed up in real-time with the CTIO/SMARTS 0.9-m for orbits and photometry. For a sample of 50 objects, calibrated sequences in RB- V-I-R filters have been obtained with the CTIO/SMARTS 0.9-m. For objects that do not show large brightness variations, the colors are largely redder than solar in both B-R and R-I. The width of the color distribution may be intrinsic to the nature of the surfaces, but also could imply that we are seeing irregularly shaped objects and measuring the colors at different times with just one telescope. For irregularly shaped objects tumbling at unknown orientations and rates, such sequential filter measurements using one telescope are subject to large errors for interpretation. If all observations in all filters in a particular sequence are of the same surface at the same solar and viewing angles, then the colors are meaningful. Where this is not the case, interpretation of the observed colors is impossible. For a smaller sample of objects we have observed with synchronized CCD cameras on the two telescopes. The CTIO/SMARTS 0.9-m observes in B, and the Schmidt in R. The CCD cameras are electronically linked together so that the start time and duration of observations are both the same to better than 50 milliseconds. Now the observed B-R color is a true measure of the scattered illuminated area of the debris piece for that observation.

Description: We present an approach to systematically derive safety cases for automatically generated code from information collected during a formal, Hoare-style safety certification of the code. This safety case makes explicit the formal and informal reasoning principles, and reveals the top-level assumptions and external dependencies that must be taken into account; however, the evidence still comes from the formal safety proofs. It uses a generic goal-based argument that is instantiated with respect to the certified safety property (i.e., safety claims) and the program. This will be combined with a complementary safety case that argues the safety of the framework itself, in particular the correctness of the Hoare rules with respect to the safety property and the trustworthiness of the certification system and its individual components. Keywords: Automated code generation, Hoare logic, formal code certification, safety case, Goal Structuring Notation.

Description: Measurement of the microgravity acceleration environment on the International Space Station has been accomplished by two accelerometer systems since 2001. The Microgravity Acceleration Measurement System records the quasi-steady microgravity environment, including the influences of aerodynamic drag, vehicle rotation, and venting effects. Measurement of the vibratory/transient regime, comprised of vehicle, crew, and equipment disturbances, has been accomplished by the Space Acceleration Measurement System-II. Until the arrival of the Columbus Orbital Facility and the Japanese Experiment Module, the location of these sensors, and therefore, the measurement of the microgravity acceleration environment, has been limited to within the United States Laboratory. Japanese Aerospace Exploration Agency has developed a vibratory acceleration measurement system called the Microgravity Measurement Apparatus which will be deployed within the Japanese Experiment Module to make distributed measurements of the Japanese Experiment Module's vibratory acceleration environment. Two Space Acceleration Measurement System sensors from the United States Laboratory will be re-deployed to support vibratory acceleration data measurement within the Columbus Orbital Facility. The additional measurement opportunities resulting from the arrival of these new laboratories allows Principal Investigators with facilities located in these International Space Station research laboratories to obtain microgravity acceleration data in support of their sensitive experiments. The Principal Investigator Microgravity Services project, at NASA Glenn Research Center, in Cleveland, Ohio, has supported acceleration measurement systems and the microgravity scientific community through the processing, characterization, distribution, and archival of the microgravity acceleration data obtained from the International Space Station acceleration measurement systems. This paper summarizes the PIMS capabilities available to the International Space Station scientific community, introduces plans for extending microgravity analysis results to the newly arrived scientific laboratories, and provides summary information for known microgravity environment disturbers.

Description: The Community Coordinated Modeling Center (CCMC) is a US inter-agency activity aiming at research in support of the generation of advanced space weather models. As one of its main functions, the CCMC provides to researchers the use of space science models, even if they are not model owners themselves. The second CCMC activity is to support Space Weather forecasting at national Space Weather Forecasting Centers. This second activity involved model evaluations, model transitions to operations, and the development of draft Space Weather forecasting tools. This presentation will focus on the latter element. Specifically, we will discuss the process of transition research models, or information generated by research models, to Space Weather Forecasting organizations. We will analyze successes as well as obstacles to further progress, and we will suggest avenues for increased transitioning success.

Description: In order to accomplish the full Vision for Space Exploration announced by former President George W. Bush in 2004, NASA will have to develop a new space transportation system and supporting infrastructure. The main portion of this supporting infrastructure will reside at the Kennedy Space Center (KSC) in Florida and will either be newly developed or a modification of existing vehicle processing and launch facilities, including Ground Support Equipment (GSE). This type of large-scale launch site development is unprecedented since the time of the Apollo Program. In order to accomplish this successfully within the limited budget and schedule constraints a combination of traditional and innovative strategies for Verification and Validation (V&V) have been developed. The core of these strategies consists of a building-block approach to V&V, starting with component V&V and ending with a comprehensive end-to-end validation test of the complete launch site, called a Ground Element Integration Test (GEIT). This paper will outline these strategies and provide the high level planning for meeting the challenges of implementing V&V on a large-scale development program. KEY WORDS: Systems, Elements, Subsystem, Integration Test, Ground Systems, Ground Support Equipment, Component, End Item, Test and Verification Requirements (TVR), Verification Requirements (VR)

Description: No abstract available

Description: If it is one thing that Florida has in abundance, it is sunshine and with that sunshine heat and humidity. For workers at the Kennedy Space Center that have to work outside in the heat and humidity, heat exhaustion/stroke is a real possibility. It might help people to know that Kennedy's Biomedical Laboratory has been testing some new Koolvests(Trademark) that can be worn underneath SCAPE suits. They have also been working on how to block out high noise levels; in fact, Don Doerr, chief of the Biomedical Lab, says, "The most enjoyable aspect is knowing that the Biomedical Lab and the skills of its employees have been used to support safe space flight, not only for the astronaut flight crew, but just as important for the ground processing personnel as well." The NASA Biomedical Laboratory has existed in the John F. Kennedy's Operations and Checkout Building since the Apollo Program. The primary mission of this laboratory has been the biomedical support to major, manned space programs that have included Apollo, Apollo-Soyuz, Skylab, and Shuttle. In this mission, the laboratory has been responsible in accomplishing much of the technical design, planning, provision, fabrication, and maintenance of flight and ground biomedical monitoring instrumentation. This includes the electronics in the launch flight suit and similar instrumentation systems in the spacecraft. (Note: The Lab checked out the system for STS-128 at Pad A using Firing room 4 and ground support equipment in the lab.) During Apollo, there were six engineers and ten technicians in the facility. This has evolved today to two NASA engineers and two NASA technicians, a Life Science Support contract physiologist and part-time support from an LSSC nurse and physician. Over the years, the lab has enjoyed collaboration with outside agencies and investigators. These have included on-site support to the Ames Research Center bed rest studies (seven years) and the European Space Agency studies in Toulouse, France (two years). The lab has also actively collaborated with the US Army Institute for Surgical Research, the USAF School of Aerospace Medicine, and the USN Naval Experimental Diving Unit. Because the lab often evaluates various forms of commercial-off-the-shelf life support equipment, the laboratory works closely with private companies, both domestic and foreign. The European companies seem to be more proactive and participatory with the advancement of personal protective equipment. Because these companies have viewed the space program's unique need for advanced forms of personal protective equipment, some have responded with new designs based on the prediction that these advances will soon find markets in the commercial sector. Using much of the same skills and equipment, the laboratory also addresses physiological testing of humans by supporting flight experiments and personnel involved with ground processing. While Johnson Space Center is primarily responsible for flight experiments, the Kennedy's Biomedical Lab provides the local support. However, as stated above, there are many challenges facing KSC workers that gain the attention of this lab in the measurement of the problem and the selection and testing of countermeasures. These include respiratory protection, whole body suits, hearing protection and heat stress, among many others.

Description: The Constellation Program is the medium by which we will maintain a presence in low Earth orbit, return to the moon for further exploration and develop procedures for Mars exploration. The foundation for its presence and success is built by the many individuals that have given of their time, talent and even lives to help propel the mission and objectives of NASA. The Exploration Systems Mission Directorate (ESMD) Faculty Fellows Program is a direct contributor to the success of directorate and Constellation Program objectives. It is through programs such as the ESMD Space Grant program that students are inspired and challenged to achieve the technological heights that will propel us to meet the goals and objectives of ESMD and the Constellation Program. It is through ESMD Space Grant programs that future NASA scientists, engineers, and mathematicians begin to dream of taking America to newer heights of space exploration. The ESMD Space Grant program is to be commended for taking the initiative to develop and implement programs that help solidify the mission of NASA. With the concerted efforts of the Kennedy Space Center educational staff, the 2009 ESMD Space Grant Summer Faculty Fellows Program allowed faculty to become more involved with NASA personnel relating to exploration topics for the senior design projects. The 2009 Project was specifically directed towards NASA's Strategic Educational Outcome 1. In-situ placement of Faculty Fellows at the NASA field Centers was essential; this allowed personal interactions with NASA scientists and engineers. In particular, this was critical to better understanding the NASA problems and begin developing a senior design effort to solve the problems. The Faculty Fellows are pleased that the ESMD Space Grant program is taking interest in developing the Senior Design courses at the university level. These courses are needed to help develop the NASA engineers and scientists of the very near future. It has been a pleasure to be part of the evaluation process to help ensure that these courses are developed in such a way that the students' educational objectives are maximized. Ultimately, with NASA-related content used as projects in the course, students will be exposed to space exploration concepts and issues while still in college. This will help to produce NASA engineers and scientists that are knowledgeable of space exploration. By the concerted efforts of these five senior design projects, NASA's ESMD Space Grant Project is making great strides at helping to develop talented engineers and scientists that will continue our exploration into space.

Description: Dynamic array bound checks are crucial elements for the security of a Java Virtual Machines. These dynamic checks are however expensive and several static analysis techniques have been proposed to eliminate explicit bounds checks. Such analyses require advanced numerical and symbolic manipulations that 1) penalize bytecode loading or dynamic compilation, 2) complexify the trusted computing base. Following the Foundational Proof Carrying Code methodology, our goal is to provide a lightweight bytecode verifier for eliminating array bound checks that is both efficient and trustable. In this work, we define a generic relational program analysis for an imperative, stackoriented byte code language with procedures, arrays and global variables and instantiate it with a relational abstract domain as polyhedra. The analysis has automatic inference of loop invariants and method pre-/post-conditions, and efficient checking of analysis results by a simple checker. Invariants, which can be large, can be specialized for proving a safety policy using an automatic pruning technique which reduces their size. The result of the analysis can be checked efficiently by annotating the program with parts of the invariant together with certificates of polyhedral inclusions. The resulting checker is sufficiently simple to be entirely certified within the Coq proof assistant for a simple fragment of the Java bytecode language. During the talk, we will also report on our ongoing effort to scale this approach for the full sequential JVM.

Description: In the late 1990s, proof-carrying code was able to produce machine-checkable safety proofs for machine-language programs even though (1) it was impractical to prove correctness properties of source programs and (2) it was impractical to prove correctness of compilers. But now it is practical to prove some correctness properties of source programs, and it is practical to prove correctness of optimizing compilers. We can produce more expressive proof-carrying code, that can guarantee correctness properties for machine code and not just safety. We will construct program logics for source languages, prove them sound w.r.t. the operational semantics of the input language for a proved-correct compiler, and then use these logics as a basis for proving the soundness of static analyses.

Description: Life as we know it requires water with a chemical activity (alpha) 〉or approx.0.6 and sources of nutrients and useful energy. Some biota can survive even if favorable conditions occur only intermittently, but the minimum required frequency of occurrences is poorly understood. Recent discoveries have vindicated the Mars exploration strategy to follow the water. Mars Global Surveyor s Thermal Emission Spectrometer (TES) found coarse-grained hematite at Meridiani Planum. Opportunity rover confirmed this and also found evidence of ancient sulfate-rich playa lakes and near-surface groundwater. Elsewhere, TES found evidence of evaporitic halides in topographic depressions. But alpha might not have approached 0.6 in these evaporitic sulfate- and halide-bearing waters. Mars Express (MEX) and Mars Reconnaissance Orbiter (MRO) found extensive sulfate evaporites in Meridiani and Valles Marineris. MEX found phyllosilicates at several sites, most notably Mawrth Valles and Nili Fossae. MRO's CRISM near-IR mapper extended the known diversity and geographic distribution of phyllosilicates to include numerous Noachian craters. Phyllosilicates typically occur at the base of exposed ancient rock sections or in sediments in early Hesperian craters. It is uncertain whether the phyllosilicates developed in surface or subsurface aqueous environments and how long aqueous conditions persisted. Spirit rover found remarkably pure ferric sulfate, indicating oxidation and transport of Fe and S, perhaps in fumaroles or hot springs. Spirit also found opaline silica, consistent with hydrothermal activity. CRISM mapped extensive silica deposits in the Valles Marineris region, consistent with aqueous weathering and deposition. CRISM also found ultramafic rocks and magnesite at Nili Fossae, consistent with serpentinization, a process that can sustain habitable environments on Earth. The report of atmospheric methane implies subsurface aqueous conditions. A working hypothesis is that aqueous environments persisted in the near-subsurface for hundreds of millions of years and might exist even today. Studies of Mars-analog environments must better understand subsurface nonphotosynthetic ecosystems and their biosignatures in mafic and ultramafic terranes. Studies must determine minimum needs for water activity and energy and also establish survival limits when conditions that support active metabolism and propagation become progressively less frequent over time.

Description: More than 140 gas-phase molecules have been detected in the interstellar (IS) medium or in circumstellar environments including inorganics, organics, ions, and radicals. The significant abundance of large, complex organic molecules, and families of isomers in these regions makes the origin and formation history of these species the subject of debate. Observationally determined condensed-phase species are H2O, CO, CO2, NH3 and CH30H, with CH4, HCOOH, OCS, OCN-, H2CO and NH4(+) present at trace levels. These ices can undergo energetic processing with cosmic rays or far-UV photons to form larger complex organics with abundance levels that make them undetectable in icy mantles. Once warmed, however, it is likely that these complex species would enter the gas-phase where they might be detected by Herschel or Alma. Understanding the role of radiation chemistry and thermal processing of ices and identifying new products are the goals of our laboratory research. In the Cosmic lee Laboratory at NASA Goddard Space Plight Center, we can study both the photo-and radiation chemistries of ices from 8 -- 300 K. Using dear- and mid-IR spectroscopy we can follow the destruction of primary molecules and the formation of radicals and secondary products as a function of energetic processing. During warming we can monitor the trapping of species and the results of any thermal chemistry. An overview of recent and past work will focus on complex secondary radiation products from small condensed-phase IS species. Likely reactions include dimerization, isomerization, H-addition and H-elimination. Another focus of our work is the development of reaction schemes for the formation of complex molecules and the use of such schemes to predict new molecules awaiting detection by Herschel and Alma.

Description: Assembly of the International Space Station is nearing completion in fall of 2010. Although assembly has been the primary objective of its first 11 years of operation, early science returns from the ISS have been growing at a steady pace. Laboratory facilities outfitting has increased dramatically 2008-2009 with the European Space Agency s Columbus and Japanese Aerospace Exploration Agency s Kibo scientific laboratories joining NASA s Destiny laboratory in orbit. In May 2009, the ISS Program met a major milestone with an increase in crew size from 3 to 6 crewmembers, thus greatly increasing the time available to perform on-orbit research. NASA will launch its remaining research facilities to occupy all 3 laboratories in fall 2009 and winter 2010. To date, early utilization of the US Operating Segment of the ISS has fielded nearly 200 experiments for hundreds of ground-based investigators supporting international and US partner research. With a specific focus on life sciences research, this paper will summarize the science accomplishments from early research aboard the ISS- both applied human research for exploration, and research on the effects of microgravity on life. We will also look ahead to the full capabilities for life sciences research when assembly of ISS is complete in 2010.

Description: As Earth science applications grow increasingly complex over time, maintenance of such software becomes a significant challenge. In general, the software subsystems were designed, implemented and integrated (over an extended period of time) by different groups that did not follow the same software design standard. The objective was understandably to obtain scientific results quickly, but this goal was often achieved at the expense of good software practices. With that pattern of development, the cost of incremental changes to the applications grow ominously large. This increase in effort, tends to squeeze development resources and largely prevent any systematic attempt to reintroduce better software practices and thereby enhance the maintainability of the software. In this paper, we present the process we used to incrementally refactor and componentize the Global Modeling Initiative code to make it more understandable, maintainable, flexible and extensible. The resulting product not only preserves the scientific integrity of the original code but also extends the capabilities of the code for several applications.

Description: The AIRS Science Team Version 5 retrieval algorithm has been finalized and is now operational at the Goddard DAAC in the processing (and reprocessing) of all AIRS data. The AIRS Science Team Version 5 retrieval algorithm contains a number of significant improvements over Version 4. Two very significant improvements are described briefly below. 1) The AIRS Science Team Radiative Transfer Algorithm (RTA) has now been upgraded to accurately account for effects of non-local thermodynamic equilibrium on the AIRS observations. This allows for use of AIRS observations in the entire 4.3 micron CO2 absorption band in the retrieval algorithm during both day and night. Following theoretical considerations, tropospheric temperature profile information is obtained almost exclusively from clear column radiances in the 4.3 micron CO2 band in the AIRS Version 5 temperature profile retrieval step. These clear column radiances are a derived product that are indicative of radiances AIRS channels would have seen if the field of view were completely clear. Clear column radiances for all channels are determined using tropospheric sounding 15 micron CO2 observations. This approach allows for the generation of accurate values of clear column radiances and T(p) under most cloud conditions. 2) Another very significant improvement in Version 5 is the ability to generate accurate case-by-case, level-by-level error estimates for the atmospheric temperature profile, as well as for channel-by-channel clear column radiances. These error estimates are used for quality control of the retrieved products. Based on error estimate thresholds, each temperature profiles is assigned a characteristic pressure, pg, down to which the profile is characterized as good for use for data assimilation purposes. We have conducted forecast impact experiments assimilating AIRS quality controlled temperature profiles using the NASA GEOS-5 data assimilation system, consisting of the NCEP GSI analysis coupled with the NASA FVGCM, at a spatial resolution of 0.5 deg by 0.5 deg. Assimilation of Quality Controlled AIRS temperature profiles down to pg resulted in significantly improved forecast skill compared to that obtained from experiments when all data used operationally by NCEP, except for AIRS data, is assimilated. These forecasts were also significantly better than to those obtained when AIRS radiances (rather than temperature profiles) are assimilated, which is the way AIRS data is used operationally by NCEP and ECMWF.

Description: Sub-orbital programs can push science to new limits by deploying the very latest in instrument concepts and technologies. Many space missions have sprung from sub-orbital programs, scientifically, technologically, and personally. I will illustrate the sub-orbital potential with examples from cosmology, interferometry, high-energy astrophysics, and others foreseen in NASA roadmaps.

Description: Scores of compounds are found in the International Space Station (ISS) atmospheric samples that are returned to the Johnson Space Center Toxicology Laboratory for analysis. Spacecraft Maximum Allowable Concentrations (SMACs) are set with the view that each compound is present as if there were no other compounds present. In order to apply SMACs to the interpretation of the analytical data, the toxicologist must employ some method of combining the potential effects of the aggregate of compounds found in the atmospheric samples. The simplest approach is to assume that each quantifiable compound has the potential for some effect in proportion to the applicable SMAC, and then add all the proportions. This simple paradigm disregards the fact that most compounds have potential to adversely affect only a few physiological systems, and their effects would be independent rather than additive. An improved approach to dealing with exposure to mixtures is to add the proportions only for compounds that adversely affect the same physiological system. For example, toxicants that cause respiratory irritation are separated from those that cause neurotoxicity or cardio-toxicity. Herein we analyze ISS air quality data according to toxicological groups with a view that this could be used for understanding any crew symptoms occurring at the time of the sample. In addition, this approach could be useful in post-flight longitudinal surveys where the flight surgeon may need to identify post-flight, follow-up medical studies because of on-orbit exposures that target specific physiological systems.

Description: A community modeling program, which provides a forum for exchange and integration between modelers, has excellent potential for furthering our Space Weather modeling and forecasting capabilities. The design of such a program is of great importance to its success. In this presentation, we will argue that the most effective community modeling program should be focused on Space Weather-related objectives, and that it should be open and inclusive. The tremendous successes of prior community research activities further suggest that the most effective implementation of a new community modeling program should be based on community leadership, rather than on domination by individual institutions or centers. This presentation will provide an experience-based justification for these conclusions.

Description: The Texas Space Grant Consortium (TSGC) and the Exploration Systems Mission Directorate (ESMD) both have programs that present design challenges for university senior design classes that offer great opportunities for educational outreach and workforce development. These design challenges have been identified by NASA engineers and researchers as real design problems faced by the Constellation Program in its exploration missions and architecture. Student teams formed in their senior design class select and then work on a design challenge for one or two semesters. The senior design class follows the requirements set by their university, but it must also comply with the Accreditation Board for Engineering and Technology (ABET) in order to meet the class academic requirements. Based on a one year fellowship at a TSGC university under the NASA Administrator's Fellowship Program (NAFP) and several years of experience, results and metrics are presented on the NASA Design Challenge Program.

Description: Manned space vehicles have a common requirement to remove the Carbon Dioxide (CO2) created by the metabolic processes of the crew. The Space Shuttle and International Space Station (ISS) each have systems in place to allow control and removal of CO2 from the habitable cabin environment. During periods where the Space Shuttle is docked to ISS, known as joint docked operations, the Space Shuttle and ISS share a common atmosphere environment. During this period there is an elevated production of CO2 caused by the combined metabolic activity of the Space Shuttle and ISS crew. This elevated CO2 production, combined with the large effective atmosphere created by the collective volumes of the docked vehicles, creates a unique set of requirements for CO2 removal. This paper will describe the individual CO2 control plans implemented by the Space Shuttle and ISS engineering teams, as well as the integrated plans used when both vehicles are docked. In addition, the paper will discuss some of the issues and anomalies experienced by both engineering teams.

Description: During MESSENGER'S second flyby of Mercury on October 6,2008, very intense reconnection was observed between the planet's magnetic field and a steady southward interplanetary magnetic field (IMF). The dawn magnetopause was threaded by a strong magnetic field normal to its surface, approx.14 nT, that implies a rate of reconnection approx.10 times the typical rate at Earth and a cross-magnetospheric electric potential drop of approx.30 kV. The highest magnetic field observed during this second flyby, approx.160 nT, was found at the core of a large dayside flux transfer event (FTE). This FTE is estimated to contain magnetic flux equal to approx.5% that of Mercury's magnetic tail or approximately one order of magnitude higher fraction of the tail flux than is typically found for FTEs at Earth. Plasmoid and traveling compression region (TCR) signatures were observed throughout MESSENGER'S traversal of Mercury's magnetotail with a repetition rate comparable to the Dungey cycle time of approx.2 min. The TCR signatures changed from south-north, indicating tailward motion, to north-south, indicating sunward motion, at a distance approx.2.6 RM (where RM is Mercury's radius) behind the terminator indicating that the near-Mercury magnetotail neutral line was crossed at that point. Overall, these new MESSENGER observations suggest that magnetic reconnection at the dayside magnetopause is very intense relative to what is found at Earth and other planets, while reconnection in Mercury's tail is similar to that in other planetary magnetospheres, but with a very short Dungey cycle time.

Description: During International Space Station campout protocol ExtraVehicular Activity (EVA) preparations, the crew is isolated overnight in the small airlock volume in a reduced pressure, oxygen enriched atmosphere. As such, there are special considerations for the software in terms of air composition, pressure control and emergency responses. For one, the ISS software must monitor and manage two distinct atmospheres. Also, the small airlock volume is especially sensitive to small changes in the environment, and what would be a minor emergency in the larger vehicle volume can have catastrophic results in the isolated airlock. Finally, in cases of emergency, the crew needs to rapidly egress the airlock, which requires an aggressive automatic repressurization to equalize pressure on the hatch. This paper will describe the software which is modified for the airlock campout protocol. In addition, the paper will describe the software problems and hardware problems with software workarounds which have affected campout protocol.

Description: Potential Mars Sample Return missions would aspire to collect small core and regolith samples using a rover with a sample acquisition tool and sample caching system. Samples would need to be stored in individual sealed tubes in a canister that could be transfered to a Mars ascent vehicle and returned to Earth. A sample handling, encapsulation and containerization system (SHEC) has been developed as part of an integrated system for acquiring and storing core samples for application to future potential MSR and other potential sample return missions. Requirements and design options for the SHEC system were studied and a recommended design concept developed. Two families of solutions were explored: 1)transfer of a raw sample from the tool to the SHEC subsystem and 2)transfer of a tube containing the sample to the SHEC subsystem. The recommended design utilizes sample tool bit change out as the mechanism for transferring tubes to and samples in tubes from the tool. The SHEC subsystem design, called the Bit Changeout Caching(BiCC) design, is intended for operations on a MER class rover.

Description: The LISA space mission, designed to monitor low frequency gravitational waves, is also sensitive to passages of asteroids nearby one of its three spacecrafts. We report the expected rate of detections of asteroid passages, using the known catalog of asteroids and a modeled population. The method adopted consists of determining for each known asteroid the critical encounter distance capable of producing a detectable event, and then computing the rate of encounters within this distance. Results are then scaled to the modeled population using its differential distribution in absolute magnitude, correcting for selection effects. We find that an average of 2.0 +/- 0.1 events per year at a signal-to-noise ratio of 1 will be detected by LISA, including all the asteroids in the modeled population with absolute magnitude H 〈 22, roughly equivalent to all asteroids with a diameter larger than 100 m.

Description: Methods and apparatus to encode message input symbols in accordance with an accumulate-repeat-accumulate code with repetition three or four are disclosed. Block circulant matrices are used. A first method and apparatus make use of the block-circulant structure of the parity check matrix. A second method and apparatus use block-circulant generator matrices.

Description: The National Aeronautics and Space Administration of the United States of America (NASA) has arguably led this planet in space exploration and certainly has been one of two major leaders in those endeavors. NASA governance is institutionalized and managed in a series documents arranged in a hierarchy and flowing down to the work levels. A document tree of NASA s documentation in its totality would likely overwhelm and not be very informative. Taken in segments related to the various business topics and focusing in those segments, however, provides a logical and understandable relationship and flow of requirements and processes. That is the nature of this chapter, a selection of NASA documentation pertaining to space exploration and a description of how those documents together form the plan by which NASA business for space exploration is conducted. Information presented herein is taken from NASA publications and is available publicly and no information herein is protected by copyright or security regulations. While NASA documents are the source of information presented herein, any and all views expressed herein and any misrepresentations of NASA data that may occur herein are those of the author and should not be considered NASA official positions or statements, nor should NASA endorsement of anything presented in this work be assumed.

Description: Software Quality Assurance (SQA) is an important component of the software development process. SQA processes provide assurance that the software products and processes in the project life cycle conform to their specified requirements by planning, enacting, and performing a set of activities to provide adequate confidence that quality is being built into the software. Typical techniques include: (1) Testing (2) Simulation (3) Model checking (4) Symbolic execution (5) Management reviews (6) Technical reviews (7) Inspections (8) Walk-throughs (9) Audits (10) Analysis (complexity analysis, control flow analysis, algorithmic analysis) (11) Formal method Our work over the last few years has resulted in substantial knowledge about SQA techniques, especially the areas of technical reviews and inspections. But can we apply the same QA techniques to the system development process? If yes, what kind of tailoring do we need before applying them in the system engineering context? If not, what types of QA techniques are actually used at system level? And, is there any room for improvement.) After a brief examination of the system engineering literature (especially focused on NASA and DoD guidance) we found that: (1) System and software development process interact with each other at different phases through development life cycle (2) Reviews are emphasized in both system and software development. (Figl.3). For some reviews (e.g. SRR, PDR, CDR), there are both system versions and software versions. (3) Analysis techniques are emphasized (e.g. Fault Tree Analysis, Preliminary Hazard Analysis) and some details are given about how to apply them. (4) Reviews are expected to use the outputs of the analysis techniques. In other words, these particular analyses are usually conducted in preparation for (before) reviews. The goal of our work is to explore the interaction between the Quality Assurance (QA) techniques at the system level and the software level.

Description: In October and November of 2008, the Jet Propulsion Laboratory installed and tested essential elements of Delay/Disruption Tolerant Networking (DTN) technology on the Deep Impact spacecraft. This experiment, called Deep Impact Network Experiment (DINET), was performed in close cooperation with the EPOXI project which has responsibility for the spacecraft. During DINET some 300 images were transmitted from the JPL nodes to the spacecraft. Then, they were automatically forwarded from the spacecraft back to the JPL nodes, exercising DTN's bundle origination, transmission, acquisition, dynamic route computation, congestion control, prioritization, custody transfer, and automatic retransmission procedures, both on the spacecraft and on the ground, over a period of 27 days. All transmitted bundles were successfully received, without corruption. The DINET experiment demonstrated DTN readiness for operational use in space missions.

Description: SAPE is a Python-based multidisciplinary analysis tool for systems analysis of planetary entry, descent, and landing (EDL) for Venus, Earth, Mars, Jupiter, Saturn, Uranus, Neptune, and Titan. The purpose of SAPE is to provide a variable-fidelity capability for conceptual and preliminary analysis within the same framework. SAPE includes the following analysis modules: geometry, trajectory, aerodynamics, aerothermal, thermal protection system, and structural sizing. SAPE uses the Python language-a platform-independent open-source software for integration and for the user interface. The development has relied heavily on the object-oriented programming capabilities that are available in Python. Modules are provided to interface with commercial and government off-the-shelf software components (e.g., thermal protection systems and finite-element analysis). SAPE runs on Microsoft Windows and Apple Mac OS X and has been partially tested on Linux.

Description: The Materials and Processes (M&P) Branch of the Structural Engineering Division at Johnson Space Center (JSC) seeks to uphold the production of dependable space hardware through materials research, which fits into NASA's purpose of advancing human exploration, use, and development of space. The Space Environmental Effects projects fully support these Agency goals. Two tasks were assigned to support M&P. Both assignments were to further the research of material behavior outside of Earth's atmosphere in order to determine which materials are most durable and safe to use in space for mitigating risks. One project, the Materials on International Space Station Experiments (MISSE) task, was to compile data from International Space Station (ISS) experiments to pinpoint beneficial space hardware. The other project was researching the effects on composite materials of exposure to high doses of radiation for a Lunar habitat project.

Description: Software inspections provide a proven approach to quality assurance for software products of all kinds, including requirements, design, code, test plans, among others. Common to all inspections is the aim of finding and fixing defects as early as possible, and thereby providing cost savings by minimizing the amount of rework necessary later in the lifecycle. Measurement data, such as the number and type of found defects and the effort spent by the inspection team, provide not only direct feedback about the software product to the project team but are also valuable for process improvement activities. In this paper, we discuss NASA's use of software inspections and the rich set of data that has resulted. In particular, we present results from analysis of inspection data that illustrate the benefits of fully utilizing that data for process improvement at several levels. Examining such data across multiple inspections or projects allows team members to monitor and trigger cross project improvements. Such improvements may focus on the software development processes of the whole organization as well as improvements to the applied inspection process itself.

Description: Declarative specifications of digital systems often contain parts that can be automatically translated into executable code. Automated code generation may reduce or eliminate the kinds of errors typically introduced through manual code writing. For this approach to be effective, the generated code should be reasonably efficient and, more importantly, verifiable. This paper presents a prototype code generator for the Prototype Verification System (PVS) that translates a subset of PVS functional specifications into an intermediate language and subsequently to multiple target programming languages. Several case studies are presented to illustrate the tool's functionality. The generated code can be analyzed by software verification tools such as verification condition generators, static analyzers, and software model-checkers to increase the confidence that the generated code is correct.

Description: This report documents the generation of an outbound Earth to Moon transfer preliminary database consisting of four cases calculated twice a day for a 19 year period. The database was desired as the first step in order for NASA to rapidly generate Earth to Moon trajectories for the Constellation Program using the Mission Assessment Post Processor. The completed database was created running a flight trajectory and optimization program, called Copernicus, in batch mode with the use of newly created Matlab functions. The database is accurate and has high data resolution. The techniques and scripts developed to generate the trajectory information will also be directly used in generating a comprehensive database.

Description: Although NASA has conducted research on orbital debris since the 1960s, the NASA Orbital Debris Program Office is now considered to have been established in October 1979, following the recognition by senior NASA officials of orbital debris as a space environmental issue and the allocation by NASA Headquarters Advanced Programs Office to the Lyndon B. Johnson Space Center (JSC) of funds specifically dedicated for orbital debris investigations. In the 30 years since, the NASA Orbital Debris Program Office has pioneered the characterization of the orbital debris environment and its potential effects on current and future space systems, has developed comprehensive orbital debris mitigation measures, and has led efforts by the international aerospace community in addressing the challenges posed by orbital debris. In 1967 the Flight Analysis Branch at the Manned Spacecraft Center (renamed the Lyndon B. Johnson Space Center in 1973) evaluated the risks of collisions between an Apollo spacecraft and orbital debris. Three years later the same group calculated collision risks for the forthcoming Skylab space station, which was launched in 1973. By 1976, the nucleus of NASA s yet-to-be-formed orbital debris research efforts, including Andrew Potter, Burton Cour-Palais, and Donald Kessler, was found in JSC s Environmental Effects Office, examining the potential threat of orbital debris to large space platforms, in particular the proposed Solar Power Satellites (SPS).

Description: The J-2X Engine (built by Pratt & Whitney Rocketdyne,) in the Upper Stage of the Ares I Crew Launch Vehicle, will only start within a certain range of temperature and pressure for Liquid Hydrogen and Liquid Oxygen propellants. The purpose of the Simulink Integrated Performance Analysis Model is to verify that in all reasonable conditions the temperature and pressure of the propellants are within the required J-2X engine start boxes. In order to run the simulation, test variables must be entered at all reasonable values of parameters such as heat leak and mass flow rate. To make this testing process as efficient as possible in order to save the maximum amount of time and money, and to show that the J-2X engine will start when it is required to do so, a graphical user interface (GUI) was created to allow the input of values to be used as parameters in the Simulink Model, without opening or altering the contents of the model. The GUI must allow for test data to come from Microsoft Excel files, allow those values to be edited before testing, place those values into the Simulink Model, and get the output from the Simulink Model. The GUI was built using MATLAB, and will run the Simulink simulation when the Simulate option is activated. After running the simulation, the GUI will construct a new Microsoft Excel file, as well as a MATLAB matrix file, using the output values for each test of the simulation so that they may graphed and compared to other values.

Description: Using a commercial software CD and minimal up-mass, SNFM monitors the Payload local area network (LAN) to analyze and troubleshoot LAN data traffic. Validating LAN traffic models may allow for faster and more reliable computer networks to sustain systems and science on future space missions. Research Summary: This experiment studies the function of the computer network onboard the ISS. On-orbit packet statistics are captured and used to validate ground based medium rate data link models and enhance the way that the local area network (LAN) is monitored. This information will allow monitoring and improvement in the data transfer capabilities of on-orbit computer networks. The Serial Network Flow Monitor (SNFM) experiment attempts to characterize the network equivalent of traffic jams on board ISS. The SNFM team is able to specifically target historical problem areas including the SAMS (Space Acceleration Measurement System) communication issues, data transmissions from the ISS to the ground teams, and multiple users on the network at the same time. By looking at how various users interact with each other on the network, conflicts can be identified and work can begin on solutions. SNFM is comprised of a commercial off the shelf software package that monitors packet traffic through the payload Ethernet LANs (local area networks) on board ISS.

Description: The purpose of this project was to create Human-System Integration (HSI) scorecard software, which could be utilized to validate that human factors have been considered early in hardware/system specifications and design. The HSI scorecard is partially based upon the revised Human Rating Requirements (HRR) intended for NASA's Constellation program. This software scorecard will allow for quick appraisal of HSI factors, by using visual aids to highlight low and rapidly changing scores. This project consisted of creating a user-friendly Visual Basic program that could be easily distributed and updated, to and by fellow colleagues. Updating the Microsoft Word version of the HSI scorecard to a computer application will allow for the addition of useful features, improved easy of use, and decreased completion time for user. One significant addition is the ability to create Microsoft Excel graphs automatically from scorecard data, to allow for clear presentation of problematic areas. The purpose of this paper is to describe the rational and benefits of creating the HSI scorecard software, the problems and goals of project, and future work that could be done.

Description: A computer program has been developed to provide a common interface for all space mission data, and allows different types of data to be displayed in the same context. This software provides an infrastructure for representing any type of mission data.

Description: This report summarizes research accomplishments on the International Space Station (ISS) through the first 15 Expeditions. When research programs for early Expeditions were established, five administrative organizations were executing research on ISS: bioastronautics research, fundamental space biology, physical science, space product development, and space flight. The Vision for Space Exploration led to changes in NASA's administrative structures, so we have grouped experiments topically by scientific themes human research for exploration, physical and biological sciences, technology development, observing the Earth, and educating and inspiring the next generation even when these do not correspond to the administrative structure at the time at which they were completed. The research organizations at the time at which the experiments flew are preserved in the appendix of this document. These investigations on the ISS have laid the groundwork for research planning for Expeditions to come. Humans performing scientific investigations on ISS serve as a model for the goals of future Exploration missions. The success of a wide variety of investigations is an important hallmark of early research on ISS. Of the investigations summarized here, some are completed with results released, some are completed with preliminary results, and some remain ongoing.

Description: The FLUKA nuclear transport and reaction code can be developed into a practical tool for calculation of spacecraft and planetary surface asset SEE and TID environments. Nuclear reactions and secondary particle shower effects can be estimated with acceptable accuracy both in-flight and in test. More detailed electronic device and/or spacecraft geometries than are reported here are possible using standard FLUKA geometry utilities. Spacecraft structure and shielding mass. Effects of high Z elements in microelectronic structure as reported previously. Median shielding mass in a generic slab or concentric sphere target geometry are at least approximately applicable to more complex spacecraft shapes. Need the spacecraft shielding mass distribution function applicable to the microelectronic system of interest. SEE environment effects can be calculated for a wide range of spacecraft and microelectronic materials with complete nuclear physics. Evaluate benefits of low Z shielding mass can be evaluated relative to aluminum. Evaluate effects of high Z elements as constituents of microelectronic devices. The principal limitation on the accuracy of the FLUKA based method reported here are found in the limited accuracy and incomplete character of affordable heavy ion test data. To support accurate rate estimates with any calculation method, the aspect ratio of the sensitive volume(s) and the dependence must be better characterized.

Description: An universal and programmable logic gate based on G.sup.4-FET technology is disclosed, leading to the design of more efficient logic circuits. A new full adder design based on the G.sup.4-FET is also presented. The G.sup.4-FET can also function as a unique router device offering coplanar crossing of signal paths that are isolated and perpendicular to one another. This has the potential of overcoming major limitations in VLSI design where complex interconnection schemes have become increasingly problematic.

Description: Results are presented for 607 speckle interferometric observations of double stars, as well as 222 measures of single stars or unresolved pairs. All data were obtained in 2006 and 2007 at the Mount Wilson Observatory, using the 2.5 m Hooker telescope. Separations range from 0.06 to 6.31, with a median of 0.34. These three observing runs concentrated on binaries in need of confirmation (mainly Hipparcos and Tycho pairs), as well as systems in need of improved orbital elements. New orbital solutions have been determined for 35 systems as a result.

Description: Certifying compilers generate proofs for low-level code that guarantee safety properties of the code. Type information is an essential part of safety proofs. But the size of type information remains a concern for certifying compilers in practice. This paper demonstrates type representation techniques in a large-scale compiler that achieves both concise type information and efficient type checking. In our 200,000-line certifying compiler, the size of type information is about 36% of the size of pure code and data for our benchmarks, the best result to the best of our knowledge. The type checking time is about 2% of the compilation time.

Description: The NASA Orbital Debris Program Office (ODPO) developed a high fidelity debris evolutionary model, LEGEND (a LEO-to-GEO Environment Debris model), in 2004 to enhance its capability to better model the near-Earth environment. LEGEND can mimic the growth of the historical debris population and project it into the future based on user-defined scenarios. The first major LEGEND study concluded that even without any future launches, the LEO population would continue to increase due to mutual collisions among existing objects. In reality, the increase will be worse than this prediction because of ongoing satellite launches and unexpected major breakups. Even with a full implementation of the commonly-adopted mitigation measures, the LEO population growth is inevitable. To preserve the near-Earth environment for future generations, active debris removal (ADR) must be considered. A follow-up LEGEND ADR study was completed recently. The main results indicate that (1) the mass and collision probability of each object can be used to establish an effective removal selection criterion and (2) a removal rate of ~5 objects per year is sufficient to stabilize the LEO environment. Due to the limitation of removal techniques, however, different target selection criteria (in size, altitude, inclination, etc.) may be more practical. A careful evaluation of the effectiveness of different proposed techniques must be carried out to maximize the long-term benefit to the environment.

Description: Software programmer Jason Holmberg of Portland, Oregon, partnered with a Goddard Space Flight Center astrophysicist to develop a method for tracking the elusive whale shark using the unique spot patterns on the fish s skin. Employing a star-mapping algorithm originally designed for the Hubble Space Telescope, Holmberg created the Shepherd Project, a photograph database and pattern-matching system that can identify whale sharks by their spots and match images contributed to the database by photographers from around the world. The system has been adapted for tracking other rare and endangered animals, including polar bears and ocean sunfish.

Description: A diagnosable structured logic array and associated process is provided. A base cell structure is provided comprising a logic unit comprising a plurality of input nodes, a plurality of selection nodes, and an output node, a plurality of switches coupled to the selection nodes, where the switches comprises a plurality of input lines, a selection line and an output line, a memory cell coupled to the output node, and a test address bus and a program control bus coupled to the plurality of input lines and the selection line of the plurality of switches. A state on each of the plurality of input nodes is verifiably loaded and read from the memory cell. A trusted memory block is provided. The associated process is provided for testing and verifying a plurality of truth table inputs of the logic unit.

Description: NASA's strategic Goals: a) Develop a balanced overall program of science, exploration, and aeronautics consistent with the redirection of human spaceflight program to focus on exploration. b) Study Earth from space to advance scientific understanding and meet societal needs. NASA's partnership efforts in global modeling and data assimilation over the next decade will shorten the distance from observations to answers for important, leading-edge science questions. NASA's Applied Sciences program will continue the Agency's efforts in benchmarking the assimilation of NASA research results into policy and management decision-support tools that are vital for the Nation's environment, economy, safety, and security. NASA also is working with NOAH and inter-agency forums to transition mature research capabilities to operational systems, primarily the polar and geostationary operational environmental satellites, and to utilize fully those assets for research purposes.

Description: Most LEO debris lies in a limited number of inclination "bands" associated with specific useful orbits. Objects in such narrow inclination bands have all possible Right Ascensions of Ascending Node (RAANs), creating a different orbit plane for nearly every piece of debris. However, a low-orbiting satellite will always phase in RAAN faster than debris objects in higher orbits at the same inclination, potentially solving the problem. Such a low-orbiting base can serve as a "mother ship" that can tend and then send small, disposable common individual catcher/deboost devices--one for each debris object--as the facility drifts into the same RAAN as each higher object. The dV necessary to catch highly-eccentric orbit debris in the center of the band alternatively allows the capture of less-eccentric debris in a wider inclination range around the center. It is demonstrated that most LEO hazardous debris can be removed from orbit in three years, using a single LEO launch of one mother ship--with its onboard magazine of freeflying low-tech catchers--into each of ten identified bands, with second or potentially third launches into only the three highest-inclination bands. The nearly 1000 objects near the geostationary orbit present special challenges in mass, maneuverability, and ultimate disposal options, leading to a dramatically different architecture and technology suite than the LEO solution. It is shown that the entire population of near-GEO derelict objects can be gathered and tethered together within a 3 year period for future scrap-yard operations using achievable technologies and only two earth launches.

Description: Crewmembers on Mars missions will face new and unique challenges compared to those in close communications proximity to Mission Control centers. Crews on Mars will likely become more autonomous and responsible for their day-to-day planning. These explorers will need to make frequent real time decisions without the assistance of large ground support teams. Ground-centric control will no longer be an option due to the communications delays. As a result of the new decision making model, crew dynamics and leadership styles of future astronauts may become significantly different from the demands of today. As a volunteer for the Mars Society on two Mars analog missions, this presenter will discuss observations made during isolated, surface exploration simulations. The need for careful crew selections, not just based on individual skill sets, but on overall team interactions becomes apparent very quickly when the crew is planning their own days and deciding their own priorities. Even more important is the selection of a Mission Commander who can lead a team of highly skilled individuals with strong and varied opinions in a way that promotes crew consensus, maintains fairness, and prevents unnecessary crew fatigue.

Description: The performance of ISS spacecraft materials and systems on prolonged exposure to the low- Earth orbit (LEO) space flight are reported in this paper. In-flight data, flight crew observations, and the results of ground-based test and analysis directly supporting programmatic and operational decision-making are described. The space flight environments definitions (both natural and induced) used for ISS design, material selection, and verification testing are shown, in most cases, to be more severe than the actual flight environment accounting, in part, for the outstanding performance of ISS as a long mission duration spacecraft. No significant ISS material or system failures have been attributed to spacecraft-environments interactions. Nonetheless, ISS materials and systems performance data is contributing to our understanding of spacecraft material interactions with the spaceflight environment so as to reduce cost and risk for future spaceflight projects and programs. Orbital inclination (51.6 deg) and altitude (nominally near 360 km) determine the set of natural environment factors affecting the functional life of materials and systems on ISS. ISS operates in an electrically conducting environment (the F2 region of Earth s ionosphere) with well-defined fluxes of atomic oxygen, other charged and neutral ionospheric plasma species, solar UV, VUV, and x-ray radiation as well as galactic cosmic rays, trapped radiation, and solar cosmic rays. The LEO micrometeoroid and orbital debris environment is an especially important determinant of spacecraft design and operations. The magnitude of several environmental factors varies dramatically with latitude and longitude as ISS orbits the Earth. The high latitude orbital environment also exposes ISS to higher fluences of trapped energetic electrons, auroral electrons, solar cosmic rays, and galactic cosmic rays than would be the case in lower inclination orbits, largely as a result of the overall shape and magnitude of the geomagnetic field. As a result, ISS exposure to many environmental factors can vary dramatically along a particular orbital ground track, and from one ground track to the next, during any 24-hour period. The induced environment results from ISS interactions with the natural environment as well as environmental factors produced by ISS itself and visiting vehicles fleet. Examples include ram-wake effects, hypergolic thruster plume impingement, materials out-gassing, venting and dumping of fluids, and specific photovoltaic (PV) power system interactions with the ionospheric plasma (7-11). Vehicle size (L) and velocity (V), combined with the magnitude and direction of the geomagnetic field (B) produce operationally significant magnetic induction voltages (VxB.L) in ISS conducting structure during flight through high latitudes (〉 +45deg) during each orbit. Finally, an induced ionizing radiation environment is produced by cosmic ray interaction with the relatively thick ISS structure and shielding materials. The intent of this review article is, therefore, to provide a summary of selected aspects and elements of the ISS vehicle with regard to LEO space environment effects, associated with the much larger and more complicated vehicle that ISS has become since 1998, but also with an eye towards performance life extension to the year 2016 and beyond.

Description: This NASA conference publication contains the proceedings of the Third International Workshop on Proof-Carrying Code and Software Certification, held as part of LICS in Los Angeles, CA, USA, on August 15, 2009. Software certification demonstrates the reliability, safety, or security of software systems in such a way that it can be checked by an independent authority with minimal trust in the techniques and tools used in the certification process itself. It can build on existing validation and verification (V&V) techniques but introduces the notion of explicit software certificates, Vvilich contain all the information necessary for an independent assessment of the demonstrated properties. One such example is proof-carrying code (PCC) which is an important and distinctive approach to enhancing trust in programs. It provides a practical framework for independent assurance of program behavior; especially where source code is not available, or the code author and user are unknown to each other. The workshop wiII address theoretical foundations of logic-based software certification as well as practical examples and work on alternative application domains. Here "certificate" is construed broadly, to include not just mathematical derivations and proofs but also safety and assurance cases, or any fonnal evidence that supports the semantic analysis of programs: that is, evidence about an intrinsic property of code and its behaviour that can be independently checked by any user, intermediary, or third party. These guarantees mean that software certificates raise trust in the code itself, distinct from and complementary to any existing trust in the creator of the code, the process used to produce it, or its distributor. In addition to the contributed talks, the workshop featured two invited talks, by Kelly Hayhurst and Andrew Appel. The PCC 2009 website can be found at http://ti.arc.nasa.gov /event/pcc 091.

Description: Surprisingly little is known about Venus, our neighboring sister planet in the solar system, due to the challenges of operating in its extremely hot, corrosive, and dense environment. For example, after over two dozen missions to the planet, the longest-lived lander was the Soviet Venera 13, and it only survived two hours on the surface. Several conceptual Venus mission studies have been formulated in the past two decades proposing lander architectures that potentially extend lander lifetime. Most recently, the Venus Science and Technology Definition Team (STDT) was commissioned by NASA to study a Venus Flagship Mission potentially launching in the 2020- 2025 time-frame; the reference lander of this study is designed to survive for only a few hours more than Venera 13 launched back in 1981! Since Cytherean mission planners lack a viable approach to a long-lived surface architecture, specific scientific objectives outlined in the National Science Foundation Decadal Survey and Venus Exploration Advisory Group final report cannot be completed. These include: mapping the mineralogy and composition of the surface on a planetary scale determining the age of various rock samples on Venus, searching for evidence of changes in interior dynamics (seismometry) and its impact on climate and many other key observations that benefit with time scales of at least a full Venus day (Le. daylight/night cycle). This report reviews those studies and recommends a hybrid lander architecture that can survive for at least one Venus day (243 Earth days) by incorporating selective Stirling multi-stage active cooling and hybrid thermoacoustic power.

Description: Discovery by Cassini's plasma instrument of heavy positive and negative ions within Titan's upper atmosphere and ionosphere has advanced our understanding of ion neutral chemistry within Titan's upper atmosphere, primarily composed of molecular nitrogen, with approx.2.5% methane. The external energy flux transforms Titan's upper atmosphere and ionosphere into a medium rich in complex hydrocarbons, nitriles and haze particles extending from the surface to 1200 km altitudes. The energy sources are solar UV, solar X-rays, Saturn's magnetospheric ions and electrons, solar wind and shocked magnetosheath ions and electrons, galactic cosmic rays (CCR) and the ablation of incident meteoritic dust from Enceladus' E-ring and interplanetary medium. Here it is proposed that the heavy atmospheric ions detected in situ by Cassini for heights 〉950 km, are the likely seed particles for aerosols detected by the Huygens probe for altitudes 〈100km. These seed particles may be in the form of polycyclic aromatic hydrocarbons (PAH) containing both carbon and hydrogen atoms CnHx. There could also be hollow shells of carbon atoms, such as C60, called fullerenes which contain no hydrogen. The fullerenes may compose a significant fraction of the seed particles with PAHs contributing the rest. As shown by Cassini, the upper atmosphere is bombarded by magnetospheric plasma composed of protons, H(2+) and water group ions. The latter provide keV oxygen, hydroxyl and water ions to Titan's upper atmosphere and can become trapped within the fullerene molecules and ions. Pickup keV N(2+), N(+) and CH(4+) can also be implanted inside of fullerenes. Attachment of oxygen ions to PAH molecules is uncertain, but following thermalization O(+) can interact with abundant CH4 contributing to the CO and CO2 observed in Titan's atmosphere. If an exogenic keV O(+) ion is implanted into the haze particles, it could become free oxygen within those aerosols that eventually fall onto Titan's surface. The process of freeing oxygen within aerosols could be driven by cosmic ray interactions with aerosols at all heights. This process could drive pre-biotic chemistry within the descending aerosols. Cosmic ray interactions with grains at the surface, including water frost depositing on grains from cryovolcanism, would further add to abundance of trapped free oxygen. Pre-biotic chemistry could arise within surface microcosms of the composite organic-ice grains, in part driven by free oxygen in the presence of organics and any heat sources, thereby raising the astrobiological potential for microscopic equivalents of Darwin's "warm ponds" on Titan.

Description: Genesis solar wind array collectors were fractured upon landing hard in Utah in 2004. The fragments were retrieved from the damaged canister, imaged, repackaged and shipped to the Johnson Space Center curatorial facility [1]. As of January 2009, the collection consists of 3460 samples. Of these, 442 are comprised into "multiple" sample groupings, either affixed to adhesive paper (177) or collected in jars (17), culture trays (87), or sets of polystyrene vials (161). A focused characterization task was initiated in May 2008 to document the largest samples in the collection. The task consisted of two goals: to document sapphire based fragments greater than 2 cm in one dimension, and to document silicon based fragments greater than 1 cm in one direction.

Description: It is known that software testers, more often than not, lack the time needed to fully test the delivered software product within the time period allotted to them. When problems in the implementation phase of a development project occur, it normally causes the software delivery date to slide. As a result, testers either need to work longer hours, or supplementary resources need to be added to the test team in order to meet aggressive test deadlines. One solution to this problem is to provide testers with a test automation framework to facilitate the development of automated test solutions.

Description: This paper describes a set of four Earth atmosphere flight test experiments on prototype helium superpressure balloons designed for Mars. Three of the experiments explored the problem of aerial deployment and inflation, using the cold, low density environment of the Earth's stratosphere at an altitude of 30-32 km as a proxy for the Martian atmosphere. Auxiliary carrier balloons were used in three of these test flights to lift the Mars balloon prototype and its supporting system from the ground to the stratosphere where the experiment was conducted. In each case, deployment and helium inflation was initiated after starting a parachute descent of the payload at 5 Pa dynamic pressure, thereby mimicking the conditions expected at Mars after atmospheric entry and high speed parachute deceleration. Upward and downward looking video cameras provided real time images from the flights, with additional data provided by onboard temperature, pressure and GPS sensors. One test of a 660 cc pumpkin balloon was highly successful, achieving deployment, inflation and separation of the balloon from the flight train at the end of inflation; however, some damage was incurred on the balloon during this process. Two flight tests of 12 m diameter spherical Mylar balloons were not successful, although some lessons were learned based on the failure analyses. The final flight experiment consisted of a ground-launched 12 m diameter spherical Mylar balloon that ascended to the designed 30.3 km altitude and successfully floated for 9.5 hours through full noontime daylight and into darkness, after which the telemetry system ran out of electrical power and tracking was lost. The altitude excursions for this last flight were +/-75 m peak to peak, indicating that the balloon was essentially leak free and functioning correctly. This provides substantial confidence that this balloon design will fly for days or weeks at Mars if it can be deployed and inflated without damage.

Description: In this paper we will give a brief overview of how different missions implemented the fault protection application and the improvements along the way. We will then propose an architecture that supports the direct implementation of state-chart models into flight code. These state-chart models can be used to formally and naturally specify the behavior of all the major fault protection components - monitors, fault protection engine, and fault responses. The goal is a flexible, light-weight implementation of a traditional fault protection software system that is inexpensive to implement, reliable and understandable for both system and software developers.

Description: These software applications provide intuitive User Interfaces (UIs) with a consistent look and feel for interaction with, and control of, the Service Preparation Subsystem (SPS). The elements of the UIs described here are the File Manager, Mission Manager, and Log Monitor applications. All UIs provide access to add/delete/update data entities in a complex database schema without requiring technical expertise on the part of the end users. These applications allow for safe, validated, catalogued input of data. Also, the software has been designed in multiple, coherent layers to promote ease of code maintenance and reuse in addition to reducing testing and accelerating maturity.

Description: In this paper, we develop and formally verify practical algorithms for recovery from loss of separation. The formal verification is performed in the context of a criteria-based framework. This framework provides rigorous definitions of horizontal and vertical maneuver correctness that guarantee divergence and achieve horizontal and vertical separation. The algorithms are shown to be independently correct, that is, separation is achieved when only one aircraft maneuvers, and implicitly coordinated, that is, separation is also achieved when both aircraft maneuver. In this paper we improve the horizontal criteria over our previous work. An important benefit of the criteria approach is that different aircraft can execute different algorithms and implicit coordination will still be achieved, as long as they all meet the explicit criteria of the framework. Towards this end we have sought to make the criteria as general as possible. The framework presented in this paper has been formalized and mechanically verified in the Prototype Verification System (PVS).

Description: A software package that has been designed to allow authentication for determining if the rover(s) is/are within a set of boundaries or a specific area to access critical geospatial information by using GPS signal structures as a means to authenticate mobile devices into a network wirelessly and in real-time. The advantage lies in that the system only allows those with designated geospatial boundaries or areas into the server.

Description: MAGIC is a software tool capable of converting highly detailed 3D models from an open, standard format, VRML 2.0/97, into the proprietary DTS file format used by the Torque Game Engine from GarageGames. MAGIC is used to convert 3D simulations from authoritative sources into the data needed to run the simulations in NASA's Distributed Observer Network. The Distributed Observer Network (DON) is a simulation presentation tool built by NASA to facilitate the simulation sharing requirements of the Data Presentation and Visualization effort within the Constellation Program. DON is built on top of the Torque Game Engine (TGE) and has chosen TGE's Dynamix Three Space (DTS) file format to represent 3D objects within simulations.

Description: X-ray observations of solar wind charge exchange (SWCX) emission, a nuisance to astrophysicists, will dramatically enhance our ability to determine the structure and variability of the Earth's magnetosheath. Such observations could be made from the lunar surface or an Earth-orbiting spacecraft and will resolve key controversies about magnetopause physics as well as better characterize SWCX emission with the aim of avoiding or removing it from astrophysical observations.

Description: Validating Vegetable Production Unit (VPU) Plants, Protocols, Procedures and Requirements (P3R) Using Currently Existing Flight Resources (Lada-VPU-P3R) is a study to advance the technology required for plant growth in microgravity and to research related food safety issues. Lada-VPU-P3R also investigates the non-nutritional value to the flight crew of developing plants on-orbit. The Lada-VPU-P3R uses the Lada hardware on the ISS and falls under a cooperative agreement between National Aeronautics and Space Administration (NASA) and the Russian Federal Space Association (FSA). Research Summary: Validating Vegetable Production Unit (VPU) Plants, Protocols, Procedures and Requirements (P3R) Using Currently Existing Flight Resources (Lada-VPU-P3R) will optimize hardware and

Description: The HICO and RAIDS Experiment Payload - Remote Atmospheric and Ionospheric Detection System (HREP-RAIDS) experiment will provide atmospheric scientists with a complete description of the major constituents of the thermosphere (layer of the Earth's atmosphere) and ionosphere (uppermost layer of the Earth's atmosphere), global electron density profiles at altitudes between 100 - 350 kilometers.

Description: Materials on the International Space Station Experiment 6 (MISSE-6A and 6B) is a test bed for materials and coatings attached to the outside of the space station that are being evaluated for the effects of atomic oxygen, direct sunlight, radiation and extremes of heat and cold. This experiment allows the development and testing of new materials to better withstand the rigors of space environments. Results will provide a better understanding of the durability of various materials in space, leading to the design of stronger, more durable spacecraft components.

Description: Microgravity Acceleration Measurement System (MAMS) is an ongoing study of the small forces (vibrations and accelerations) on the ISS that result from the operation of hardware, crew activities, as well as dockings and maneuvering. Results will be used to generalize the types of vibrations affecting vibration-sensitive experiments. Investigators seek to better understand the vibration environment on the space station to enable future research.

Description: Education Payload Operation - Kit D (EPO-Kit D) includes education items that will be used to support the live International Space Station (ISS) education downlinks and Education Payload Operation (EPO) demonstrations onboard the ISS. The main objective of EPO-Kit D supports the National Aeronautics and Space Administration (NASA) goal of attracting students to study and seek careers in science, technology, engineering, and mathematics.

Description: Education Payload Operation - Demonstrations (EPO-Demos) are recorded video education demonstrations performed on the International Space Station (ISS) by crewmembers using hardware already onboard the ISS. EPO-Demos are videotaped, edited, and used to enhance existing NASA education resources and programs for educators and students in grades K-12. EPO-Demos are designed to support the NASA mission to inspire the next generation of explorers.

Description: A computer program calculates the two-dimensional trajectory (radial vs. axial position) of a finite-radius-of-curvature cutting tool on a lathe so as to cut a workpiece to a piecewise-continuous, analytically defined surface of revolution. (In the original intended application, the tool is a diamond cutter, and the workpiece is made of a crystalline material and is to be formed into an optical resonator disk.) The program also calculates an optimum cutting speed as F/L, where F is a material-dependent empirical factor and L is the effective instantaneous length of the cutting edge.

Description: Current techniques for validating and verifying program changes often consider the entire program, even for small changes, leading to enormous V&V costs over a program s lifetime. This is due, in large part, to the use of syntactic program techniques which are necessarily imprecise. Building on recent advances in symbolic execution of heap manipulating programs, in this paper, we develop techniques for performing abstract semantic differencing of program behaviors that offer the potential for improved precision.

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

Description: Proofs provide detailed justification for the validity of claims and are widely used in formal software development methods. However, they are often complex and difficult to understand, because they use machine-oriented formalisms; they may also be based on assumptions that are not justified. This causes concerns about the trustworthiness of using formal proofs as arguments in safety-critical applications. Here, we present an approach to develop safety cases that correspond to formal proofs found by automated theorem provers and reveal the underlying argumentation structure and top-level assumptions. We concentrate on natural deduction proofs and show how to construct the safety cases by covering the proof tree with corresponding safety case fragments.

Description: Ensemble ReST is a software system that eases the development, deployment, and maintenance of server-side application programs to perform functions that would otherwise be performed by client software. Ensemble ReST takes advantage of the proven disciplines of ReST (Representational State Transfer. ReST leverages the standardized HTTP protocol to enable developers to offer services to a diverse variety of clients: from shell scripts to sophisticated Java application suites

Description: MONTE (Mission Operations and Navigation Toolkit Environment) Release 7.3 is an extensible software system designed to support trajectory and navigation analysis/design for space missions. MONTE is intended to replace the current navigation and trajectory analysis software systems, which, at the time of this reporting, are used by JPL's Navigation and Mission Design section. The software provides an integrated, simplified, and flexible system that can be easily maintained to serve the needs of future missions in need of navigation services.

Description: Beginning with OSTA-1 in November 1981 and ending with Neurolab in March 1998, a total of 36 Shuttle missions carried various Spacelab components such as the Spacelab module, pallet, instrument pointing system, or mission peculiar experiment support structure. The experiments carried out during these flights included astrophysics, solar physics, plasma physics, atmospheric science, Earth observations, and a wide range of microgravity experiments in life sciences, biotechnology, materials science, and fluid physics which includes combustion and critical point phenomena. In all, some 764 experiments were conducted by investigators from the U.S., Europe, and Japan. The purpose of this Spacelab Science Results Study is to document the contributions made in each of the major research areas by giving a brief synopsis of the more significant experiments and an extensive list of the publications that were produced. We have also endeavored to show how these results impacted the existing body of knowledge, where they have spawned new fields, and if appropriate, where the knowledge they produced has been applied.

Description: A computer program loads configuration code into a Xilinx field-programmable gate array (FPGA), reads back and verifies that code, reloads the code if an error is detected, and monitors the performance of the FPGA for errors in the presence of radiation. The program consists mainly of a set of VHDL files (wherein "VHDL" signifies "VHSIC Hardware Description Language" and "VHSIC" signifies "very-high-speed integrated circuit").

Description: The XVD [X-Windows VICAR (video image communication and retrieval) Display] computer program offers an interactive display of VICAR and PDS (planetary data systems) images. It is designed to efficiently display multiple-GB images and runs on Solaris, Linux, or Mac OS X systems using X-Windows.

Description: This document is designed as a manual for a user who wants to operate the Pro/ENGINEER (ProE) Wildfire 3.0 with the NASA Space Radiation Program's (SRP) custom-designed Toolkit, called 'Fishbowl', for the ray tracing of complex spacecraft geometries given by a ProE CAD model. The analysis of spacecraft geometry through ray tracing is a vital part in the calculation of health risks from space radiation. Space radiation poses severe risks of cancer, degenerative diseases and acute radiation sickness during long-term exploration missions, and shielding optimization is an important component in the application of radiation risk models. Ray tracing is a technique in which 3-dimensional (3D) vehicle geometry can be represented as the input for the space radiation transport code and subsequent risk calculations. In ray tracing a certain number of rays (on the order of 1000) are used to calculate the equivalent thickness, say of aluminum, of the spacecraft geometry seen at a point of interest called the dose point. The rays originate at the dose point and terminate at a homogenously distributed set of points lying on a sphere that circumscribes the spacecraft and that has its center at the dose point. The distance a ray traverses in each material is converted to aluminum or other user-selected equivalent thickness. Then all equivalent thicknesses are summed up for each ray. Since each ray points to a direction, the aluminum equivalent of each ray represents the shielding that the geometry provides to the dose point from that particular direction. This manual will first list for the user the contact information for help in installing ProE and Fishbowl in addition to notes on the platform support and system requirements information. Second, the document will show the user how to use the software to ray trace a Pro/E-designed 3-D assembly and will serve later as a reference for troubleshooting. The user is assumed to have previous knowledge of ProE and CAD modeling.

Description: This software toolkit is designed to model complex systems for the implementation of embedded Integrated System Health Management (ISHM) capability, which focuses on determining the condition (health) of every element in a complex system (detect anomalies, diagnose causes, and predict future anomalies), and to provide data, information, and knowledge (DIaK) to control systems for safe and effective operation.

Description: Proof-carrying code (PCC) provides a 'gold standard' for establishing formal and objective confidence in program behavior. However, in order to extend the benefits of PCC - and other formal certification techniques - to realistic systems, we must establish the correspondence of a mathematical proof of a program's semantics and its actual behavior. In this paper, we argue that assurance cases are an effective means of establishing such a correspondence. To this end, we present an assurance case pattern for arguing that a proof is free from various proof hazards. We also instantiate this pattern for a proof-based mechanism to provide evidence about a generic medical device software.

Description: Proofs provide detailed justification for the validity of claims and are widely used in formal software development methods. However, they are often complex and difficult to understand, because they use machine-oriented formalisms; they may also be based on assumptions that are not justified. This causes concerns about the trustworthiness of using formal proofs as arguments in safety-critical applications. Here, we present an approach to develop safety cases that correspond to formal proofs found by automated theorem provers and reveal the underlying argumentation structure and top-level assumptions. We concentrate on natural deduction proofs and show how to construct the safety cases by covering the proof tree with corresponding safety case fragments.

Description: This slide presentation reviews the approach to the development of the Global Precipitation Measurement algorithm. This presentation includes information about the responsibilities for the development of the algorithm, and the calibration. Also included is information about the orbit, and the sun angle. The test of the algorithm code will be done with synthetic data generated from the Precipitation Processing System (PPS).

Description: This slide presentation reviews the applicability of CodeSonar to the Space Network software. CodeSonar is a commercial off the shelf system that analyzes programs written in C, C++ or Ada for defects in the code. Software engineers use CodeSonar results as an input to the existing source code inspection process. The study is focused on large scale software developed using formal processes. The systems studied are mission critical in nature but some use commodity computer systems.

Description: The National Aeronautics and Space Administration (NASA) was established in 1958, and its Marshall Space Flight Center was founded in 1960, as space-related work was transferred from the Army Ballistic Missile Agency at Redstone Arsenal, where Marshall is located. With this heritage, Marshall contributes almost 50 years of systems engineering experience with human-rated launch vehicles and scientific spacecraft to fulfill NASA's mission exploration and discovery. These complex, highly specialized systems have provided vital platforms for expanding the knowledge base about Earth, the solar system, and cosmos; developing new technologies that also benefit life on Earth; and opening new frontiers for America's strategic space goals. From Mercury and Gemini, to Apollo and the Space Shuttle, Marshall's systems engineering expertise is an unsurpassed foundational competency for NASA and the nation. Current assignments comprise managing Space Shuttle Propulsion systems; developing environmental control and life support systems and coordinating science operations on the International Space Station; and a number of exploration-related responsibilities. These include managing and performing science missions, such as the Lunar Crater Observation and Sensing Satellite and the Lunar Reconnaissance Orbiter slated to launch for the Moon in April 2009, to developing the Ares I crew launch vehicle upper stage and integrating the vehicle stack in house, as well as designing the Ares V cargo launch vehicle and contributing to the development of the Altair Lunar Lander and an International Lunar Network with communications nodes and other infrastructure.

Description: The Virtual Diagnostics Interface (ViDI) methodology combines two-dimensional image processing and three-dimensional computer modeling to provide comprehensive in-situ visualizations commonly utilized for in-depth planning of wind tunnel and flight testing, real time data visualization of experimental data, and unique merging of experimental and computational data sets in both real-time and post-test analysis. The preparation of such visualizations encompasses the realm of interactive three-dimensional environments, traditional and state of the art image processing techniques, database management and development of toolsets with user friendly graphical user interfaces. ViDI has been under development at the NASA Langley Research Center for over 15 years, and has a long track record of providing unique and insightful solutions to a wide variety of experimental testing techniques and validation of computational simulations. This report will address the various aspects of ViDI and how it has been applied to test programs as varied as NASCAR race car testing in NASA wind tunnels to real-time operations concerning Space Shuttle aerodynamic flight testing. In addition, future trends and applications will be outlined in the paper.

Description: This paper offers a local distributed algorithm for expectation maximization in large peer-to-peer environments. The algorithm can be used for a variety of well-known data mining tasks in a distributed environment such as clustering, anomaly detection, target tracking to name a few. This technology is crucial for many emerging peer-to-peer applications for bioinformatics, astronomy, social networking, sensor networks and web mining. Centralizing all or some of the data for building global models is impractical in such peer-to-peer environments because of the large number of data sources, the asynchronous nature of the peer-to-peer networks, and dynamic nature of the data/network. The distributed algorithm we have developed in this paper is provably-correct i.e. it converges to the same result compared to a similar centralized algorithm and can automatically adapt to changes to the data and the network. We show that the communication overhead of the algorithm is very low due to its local nature. This monitoring algorithm is then used as a feedback loop to sample data from the network and rebuild the model when it is outdated. We present thorough experimental results to verify our theoretical claims.

Description: We present a novel algorithm for interface generation of software components. Given a component, our algorithm uses learning techniques to compute a permissive interface representing legal usage of the component. Unlike our previous work, this algorithm does not require knowledge about the component s environment. Furthermore, in contrast to other related approaches, our algorithm computes permissive interfaces even in the presence of non-determinism in the component. Our algorithm is implemented in the JavaPathfinder model checking framework for UML statechart components. We have also added support for automated assume-guarantee style compositional verification in JavaPathfinder, using component interfaces. We report on the application of the presented approach to the generation of interfaces for flight software components.

Description: We describe a framework for model-based analysis and test case generation in the context of a heterogeneous model-based development paradigm that uses and combines Math- Works and UML 2.0 models and the associated code generation tools. This paradigm poses novel challenges to analysis and test case generation that, to the best of our knowledge, have not been addressed before. The framework is based on a common intermediate representation for different modeling formalisms and leverages and extends model checking and symbolic execution tools for model analysis and test case generation, respectively. We discuss the application of our framework to software models for a NASA flight mission.