Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “compiler verification”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

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

At least 91 records · Page 5

Symbolic LTL Compilation for Model Checking: Extended Abstract

In Linear Temporal Logic (LTL) model checking, we check LTL formulas representing desired behaviors against a formal model of the system designed to exhibit these behaviors. To accomplish this task, the LTL formulas must be translated into automata [21]. We focus on LTL compilation by investigating LTL satisfiability checking via a reduction to model checking. Having shown that symbolic LTL compilation algorithms are superior to explicit automata construction algorithms for this task [16], we concentrate here on seeking a better symbolic algorithm.We present experimental data comparing algorithmic variations such as normal forms, encoding methods, and variable ordering and examine their effects on performance metrics including processing time and scalability. Safety critical systems, such as air traffic control, life support systems, hazardous environment controls, and automotive control systems, pervade our daily lives, yet testing and simulation alone cannot adequately verify their reliability [3]. Model checking is a promising approach to formal verification for safety critical systems which involves creating a formal mathematical model of the system and translating desired safety properties into a formal specification for this model. The complement of the specification is then checked against the system model. When the model does not satisfy the specification, model-checking tools accompany this negative answer with a counterexample, which points to an inconsistency between the system and the desired behaviors and aids debugging efforts.

Rozier, Kristin Y.↗

Multipurpose Crew Restraints for Long Duration Space Flights

With permanent human presence onboard the International Space Station (ISS), a crew will be living and working in microgravity, interfacing with their physical environment. Without optimum restraints and mobility aids (R&MA' s), the crewmembers may be handicapped for perfonning some of the on-orbit tasks. In addition to weightlessness, the confined nature of a spacecraft environment results in ergonomic challenges such as limited visibility and access to the activity area and may cause prolonged periods of unnatural postures. Thus, determining the right set of human factors requirements and providing an ergonomically designed environment are crucial to astronauts' well-being and productivity. The purpose of this project is to develop requirements and guidelines, and conceptual designs, for an ergonomically designed multi-purpose crew restraint. In order to achieve this goal, the project would involve development of functional and human factors requirements, design concept prototype development, analytical and computer modeling evaluations of concepts, two sets of micro gravity evaluations and preparation of an implementation plan. It is anticipated that developing functional and design requirements for a multi-purpose restraint would facilitate development of ergonomically designed restraints to accommodate the off-nominal but repetitive tasks, and minimize the performance degradation due to lack of optimum setup for onboard task performance. In addition, development of an ergonomically designed restraint concept prototype would allow verification and validation of the requirements defined. To date, we have identified "unique" tasks and areas of need, determine characteristics of "ideal" restraints, and solicit ideas for restraint and mobility aid concepts. Focus group meetings with representatives from training, safety, crew, human factors, engineering, payload developers, and analog environment representatives were key to assist in the development of a restraint concept based on previous flight experiences, the needs of future tasks, and crewmembers' preferences. Also, a catalog with existing IVA/EVA restraint and mobility aids has been developed. Other efforts included the ISS crew debrief data on restraints, compilation of data from MIR, Skylab and ISS on restraints, and investigating possibility of an in-flight evaluation of current restraint systems. Preliminary restraint concepts were developed and presented to long duration crewmembers and focus groups for feedback. Currently, a selection criterion is being refined for prioritizing the candidate concepts. Next steps include analytical and computer modeling evaluations of the selected candidate concepts, prototype development, and microgravity evaluations.

Whitmore, Mihriban↗

Generating Customized Verifiers for Automatically Generated Code

Program verification using Hoare-style techniques requires many logical annotations. We have previously developed a generic annotation inference algorithm that weaves in all annotations required to certify safety properties for automatically generated code. It uses patterns to capture generator- and property-specific code idioms and property-specific meta-program fragments to construct the annotations. The algorithm is customized by specifying the code patterns and integrating them with the meta-program fragments for annotation construction. However, this is difficult since it involves tedious and error-prone low-level term manipulations. Here, we describe an annotation schema compiler that largely automates this customization task using generative techniques. It takes a collection of high-level declarative annotation schemas tailored towards a specific code generator and safety property, and generates all customized analysis functions and glue code required for interfacing with the generic algorithm core, thus effectively creating a customized annotation inference algorithm. The compiler raises the level of abstraction and simplifies schema development and maintenance. It also takes care of some more routine aspects of formulating patterns and schemas, in particular handling of irrelevant program fragments and irrelevant variance in the program structure, which reduces the size, complexity, and number of different patterns and annotation schemas that are required. The improvements described here make it easier and faster to customize the system to a new safety property or a new generator, and we demonstrate this by customizing it to certify frame safety of space flight navigation code that was automatically generated from Simulink models by MathWorks' Real-Time Workshop.

Denney, Ewen↗

NASA Operational Simulator for Small Satellites: Tools for Software Based Validation and Verification of Small Satellites

The NASA Operational Simulator for Small Satellites (NOS3) is a suite of tools to aid in areas such as software development, integration test (IT), mission operations training, verification and validation (VV), and software systems check-out. NOS3 provides a software development environment, a multi-target build system, an operator interface-ground station, dynamics and environment simulations, and software-based hardware models. NOS3 enables the development of flight software (FSW) early in the project life cycle, when access to hardware is typically not available. For small satellites there are extensive lead times on many of the commercial-off-the-shelf (COTS) components as well as limited funding for engineering test units (ETU). Considering the difficulty of providing a hardware test-bed to each developer tester, hardware models are modeled based upon characteristic data or manufacturers data sheets for each individual component. The fidelity of each hardware models is such that FSW executes unaware that physical hardware is not present. This allows binaries to be compiled for both the simulation environment, and the flight computer, without changing the FSW source code. For hardware models that provide data dependent on the environment, such as a GPS receiver or magnetometer, an open-source tool from NASA GSFC (42 Spacecraft Simulation) is used to provide the necessary data. The underlying infrastructure used to transfer messages between FSW and the hardware models can also be used to monitor, intercept, and inject messages, which has proven to be beneficial for VV of larger missions such as James Webb Space Telescope (JWST). As hardware is procured, drivers can be added to the environment to enable hardware-in-the-loop (HWIL) testing. When strict time synchronization is not vital, any number of combinations of hardware components and software-based models can be tested. The open-source operator interface used in NOS3 is COSMOS from Ball Aerospace. For testing, plug-ins are implemented in COSMOS to control the NOS3 simulations, while the command and telemetry tools available in COSMOS are used to communicate with FSW. NOS3 is actively being used for FSW development and component testing of the Simulation-to-Flight 1 (STF-1) CubeSat. As NOS3 matures, hardware models have been added for common CubeSat components such as Novatel GPS receivers, ClydeSpace electrical power systems and batteries, ISISpace antenna systems, etc. In the future, NASA IVV plans to distribute NOS3 to other CubeSat developers and release the suite to the open-source community.

Verification↗

Status of the AIAA Modeling and Simulation Format Standard

The current draft AIAA Standard for flight simulation models represents an on-going effort to improve the productivity of practitioners of the art of digital flight simulation (one of the original digital computer applications). This initial release provides the capability for the efficient representation and exchange of an aerodynamic model in full fidelity; the DAVE-ML format can be easily imported (with development of site-specific import tools) in an unambiguous way with automatic verification. An attractive feature of the standard is the ability to coexist with existing legacy software or tools. The draft Standard is currently limited in scope to static elements of dynamic flight simulations; however, these static elements represent the bulk of typical flight simulation mathematical models. It is already seeing application within U.S. and Australian government agencies in an effort to improve productivity and reduce model rehosting overhead. An existing tool allows import of DAVE-ML models into a popular simulation modeling and analysis tool, and other community-contributed tools and libraries can simplify the use of DAVE-ML compliant models at compile- or run-time of high-fidelity flight simulation.

Jackson, E. Bruce↗

Material Characterization and Modeling of Room Temperature Vulcanizing Silicone

Room Temperature Vulcanizing silicone (RTV) is a high-temperature adhesive that has successfully been used as a gap-filler between Thermal Protection System (TPS) tiles for heatshields on numerous missions. It is also used to bond instrumentation plugs such as temperature and pressure sensors into the heatshields. While RTV has been traditionally assumed to be a non-porous and non-ablating material, numerous experiments have shown that RTV pyrolyzes and becomes highly porous as it is heated. Heating RTV has also shown swelling, or intumescence, which can pose unique problems that lead to roughness induced boundary-layer transition, surface oxide formation and contamination of heat shield sensors. Therefore, it is crucial to understand and model the intumescence phenomenon of RTV. As data for RTV material properties is limited, the first step in modeling RTV is to collect material properties such as pyrolysis mass-loss, microstructure change, virgin and char porosity, etc. which was performed in our initial study. Additionally, thermomechanical properties such as Young’s modulus and Poisson ratio are required for modeling the intumescence of RTV, which were taken from literature and the coefficient of thermal expansion was collected using in-situ heating and Micro Computed Tomography (µ-CT) in previous studies. Finally, numerous other properties such as pyrolysis gas properties, virgin and char thermal conductivity and specific heat were compiled from previous experiments and literature into a material database that can be used for simulations. In Porous Material Analysis Toolbox based on OpenFOAM (PATO) [4], structural mechanics coupled with material response was used for simulating the intumescence of RTV as it is heated. However, since the permeability of the material is very low, the pyrolysis gas creates an internal pressure build-up as the material is being heated, significantly contributing to the deformation of the material. To correctly characterize this phenomenon, additional physics models were implemented into PATO's stress analysis solver, and results were compared with RTV dilatometry test data as a preliminary verification case. Future work will include experiments of RTV at the Plasmatron X facility and the in-situ heating cell with µ-CT, and improvement of simulation tools to more accurately model RTV intumescence.

TPS↗

Material Properties and Modeling of Room Temperature Vulcanizing Silicone

Room Temperature Vulcanizing silicone (RTV) is a high-temperature adhesive that has successfully been used as a gap-filler between Thermal Protection System (TPS) tiles for heatshields on numerous missions. It is also used to bond instrumentation plugs such as temperature and pressure sensors into the heatshields. While RTV has been traditionally assumed to be a non-porous and non-ablating material, numerous experiments have shown that RTV pyrolyzes and becomes highly porous as it is heated. Heating RTV has also shown swelling, or intumescence, which can pose unique problems that lead to roughness induced boundary-layer transition, surface oxide formation and contamination of heat shield sensors. Therefore, it is crucial to understand and model the intumescence phenomenon of RTV. As data for RTV material properties is limited, the first step in modeling RTV is to collect material properties such as pyrolysis mass-loss, microstructure change, virgin and char porosity, etc. which was performed in our initial study. Additionally, thermomechanical properties such as Young’s modulus and Poisson ratio are required for modeling the intumescence of RTV, which were taken from literature and the coefficient of thermal expansion was collected using in-situ heating and Micro Computed Tomography (µ-CT) in previous studies. Finally, numerous other properties such as pyrolysis gas properties, virgin and char thermal conductivity and specific heat were compiled from previous experiments and literature into a material database that can be used for simulations. In Porous Material Analysis Toolbox based on OpenFOAM (PATO) [4], structural mechanics coupled with material response was used for simulating the intumescence of RTV as it is heated. However, since the permeability of the material is very low, the pyrolysis gas creates an internal pressure build-up as the material is being heated, significantly contributing to the deformation of the material. To correctly characterize this phenomenon, additional physics models were implemented into PATO's stress analysis solver, and results were compared with RTV dilatometry test data as a preliminary verification case. Future work will include experiments of RTV at the Plasmatron X facility and the in-situ heating cell with µ-CT, and improvement of simulation tools to more accurately model RTV intumescence.

PATO↗

Rapid Diagnostics of Onboard Sequences

Keeping track of sequences onboard a spacecraft is challenging. When reviewing Event Verification Records (EVRs) of sequence executions on the Mars Exploration Rover (MER), operators often found themselves wondering which version of a named sequence the EVR corresponded to. The lack of this information drastically impacts the operators diagnostic capabilities as well as their situational awareness with respect to the commands the spacecraft has executed, since the EVRs do not provide argument values or explanatory comments. Having this information immediately available can be instrumental in diagnosing critical events and can significantly enhance the overall safety of the spacecraft. This software provides auditing capability that can eliminate that uncertainty while diagnosing critical conditions. Furthermore, the Restful interface provides a simple way for sequencing tools to automatically retrieve binary compiled sequence SCMFs (Space Command Message Files) on demand. It also enables developers to change the underlying database, while maintaining the same interface to the existing applications. The logging capabilities are also beneficial to operators when they are trying to recall how they solved a similar problem many days ago: this software enables automatic recovery of SCMF and RML (Robot Markup Language) sequence files directly from the command EVRs, eliminating the need for people to find and validate the corresponding sequences. To address the lack of auditing capability for sequences onboard a spacecraft during earlier missions, extensive logging support was added on the Mars Science Laboratory (MSL) sequencing server. This server is responsible for generating all MSL binary SCMFs from RML input sequences. The sequencing server logs every SCMF it generates into a MySQL database, as well as the high-level RML file and dictionary name inputs used to create the SCMF. The SCMF is then indexed by a hash value that is automatically included in all command EVRs by the onboard flight software. Second, both the binary SCMF result and the RML input file can be retrieved simply by specifying the hash to a Restful web interface. This interface enables command line tools as well as large sophisticated programs to download the SCMF and RMLs on-demand from the database, enabling a vast array of tools to be built on top of it. One such command line tool can retrieve and display RML files, or annotate a list of EVRs by interleaving them with the original sequence commands. This software has been integrated with the MSL sequencing pipeline where it will serve sequences useful in diagnostics, debugging, and situational awareness throughout the mission.

Starbird, Thomas W.↗

Search for Mars lander/rover/sample-return sites: A status review

Ten Mars sites were studied in the USA for four years. The sites are the Chasma Boreale (North Pole), Planum Australe (South Pole), Olympus Rupes, Mangala Valles, Memnonia Sulci, Candor Chasma, Kasel Valles, Nilosyrtis Mensae, Elysium Montes, and Apollinaris Patera. Seven sites are being studied by the USSR; their prime sites are located at the east mouth of Kasel Valles and near Uranius Patera. Thirteen geological maps of the first six USA sites are compiled and in review. Maps of the Mangala East and West sites at 1:1/2 million scale and a 1:2 million scale map show evidence of three episodes of small-channel formation interspersed with episodes of volcanism and tectonism that span the period from 3.5 to 0.6 b.y. ago. The tectonic and geological history of Mars, both ancient and modern, can be elucidated by sampling volcanic and fluvial geologic units at equatorial sites and layered deposits at polar sites. The evidence appears clear for multiple episodes of fluvial channeling, including some that are quite recent; this evidence contrasts with the theses of Baker and Partridge (1986) and many others that all channels are ancient. Verification of this hypothesis by Mars Observer will be an important step forward in the perception of the history of Mars.

Masursky, Harold↗

Test Cases for a Rectangular Supercritical Wing Undergoing Pitching Oscillations

Steady and unsteady measured pressures for a Rectangular Supercritical Wing (RSW) undergoing pitching oscillations have been presented. From the several hundred compiled data points, 27 static and 36 pitching oscillation cases have been proposed for computational Test Cases to illustrate the trends with Mach number, reduced frequency, and angle of attack. The wing was designed to be a simple configuration for Computational Fluid Dynamics (CFD) comparisons. The wing had an unswept rectangular planform plus a tip of revolution, a panel aspect ratio of 2.0, a twelve per cent thick supercritical airfoil section, and no twist. The model was tested over a wide range of Mach numbers, from 0.27 to 0.90, corresponding to low subsonic flows up to strong transonic flows. The higher Mach numbers are well beyond the design Mach number such as might be required for flutter verification beyond cruise conditions. The pitching oscillations covered a broad range of reduced frequencies. Some early calculations for this wing are given for lifting pressure as calculated from a linear lifting surface program and from a transonic small perturbation program. The unsteady results were given primarily for a mild transonic condition at M = 0.70. For these cases the agreement with the data was only fair, possibly resulting from the omission of viscous effects. Supercritical airfoil sections are known to be sensitive to viscous effects (for example, one case cited). Calculations using a higher level code with the full potential equations have been presented for one of the same cases, and with the Euler equations. The agreement around the leading edge was improved, but overall the agreement was not completely satisfactory. Typically for low-aspect-ratio rectangular wings, transonic shock waves on the wing tend to sweep forward from root to tip such that there are strong three-dimensional effects. It might also be noted that for most of the test, the model was tested with free transition, but a few points were taken with an added transition strip for comparison. Some unpublished results of a rigid wing of the same airfoil and planform that was tested on the pitch and plunge apparatus mount system (PAPA) showed effects of the lower surface transition Strip on flutter at the lower subsonic Mach numbers. Significant effects of a transition strip were also obtained on a wing with a thicker supercritical section on the PAPA mount system. Both of these flutter tests on the PAPA resulted in very low reduced frequencies that may be a factor in this influence of the transition strip. However, these results indicate that correlation studies for RSW may require some attention to the estimation of transition location to accurately treat viscous effects. In this report several Test Cases are selected to illustrate trends for a variety of different conditions with emphasis on transonic flow effects. An overview of the model and tests is given and the standard formulary for these data is listed. Sample data points are presented in both tabular and graphical form. A complete tabulation and plotting of all the Test Cases is given. Only the static pressures and the real and imaginary parts of the first harmonic of the unsteady pressures are available. All the data for the test are available in electronic file form. The Test Cases are also available as separate electronic files.

Bennett, Robert M.↗

Algorithm Optimally Orders Forward-Chaining Inference Rules

People typically develop knowledge bases in a somewhat ad hoc manner by incrementally adding rules with no specific organization. This often results in a very inefficient execution of those rules since they are so often order sensitive. This is relevant to tasks like Deep Space Network in that it allows the knowledge base to be incrementally developed and have it automatically ordered for efficiency. Although data flow analysis was first developed for use in compilers for producing optimal code sequences, its usefulness is now recognized in many software systems including knowledge-based systems. However, this approach for exhaustively computing data-flow information cannot directly be applied to inference systems because of the ubiquitous execution of the rules. An algorithm is presented that efficiently performs a complete producer/consumer analysis for each antecedent and consequence clause in a knowledge base to optimally order the rules to minimize inference cycles. An algorithm was developed that optimally orders a knowledge base composed of forwarding chaining inference rules such that independent inference cycle executions are minimized, thus, resulting in significantly faster execution. This algorithm was integrated into the JPL tool Spacecraft Health Inference Engine (SHINE) for verification and it resulted in a significant reduction in inference cycles for what was previously considered an ordered knowledge base. For a knowledge base that is completely unordered, then the improvement is much greater.

James, Mark↗

A Study of Rapidly Developing Low Cloud Ceilings in a Stable Atmosphere at the Florida Spaceport

Forecasters at the Space Meteorology Group (SMG) issue 30 to 90 minute forecasts for low cloud ceilings at the Shuttle Landing Facility (KTTS) in Kennedy Space Center, FL for all Space Shuttle missions. Mission verification statistics have shown cloud ceilings to be the biggest forecast challenge. SMG forecasters are especially concerned with rapidly developing cloud ceilings below 8000 ft. in a stable, capped thermodynamic environment because ceilings below 8000 ft restrict Shuttle landing operations and are the most challenging to predict accurately. This project involves the development of a database of these cases over east-central Florida in order to identify the onset, location, and if possible, dissipation times of rapidly-developing low cloud ceilings. Another goal is to document the atmospheric regimes favoring this type of cloud development to improve forecast skill of such events during Space Shuttle launch and landing operations. A 10-year database of stable, rapid low cloud development days during the daylight hours was compiled for the Florida cool-season months by examining the Cape Canaveral Air Force Station sounding data, and identifying days that had high boundary layer relative humidity associated with a thermally-capped environment below 8000 ft. Archived hourly surface observations from KTTS and Melbourne, Orlando, Sanford, and Ocala, FL were then examined for the onset of cloud ceilings below 8000 ft between 1100 and 2000 UTC. Once the database was supplemented with the hourly surface cloud observations, visible satellite imagery was examined in 30-minute intervals to confirm event occurrences. This paper will present results from some of the rapidly developing cloud ceiling cases and the prevailing meteorological conditions associated with these events, focusing on potential pre-curser information that may help improve their prediction.

FROM↗

Lockheed Martin Skunk Works Single Stage to Orbit/Reusable Launch Vehicle

Lockheed Martin Skunk Works has compiled an Annual Performance Report of the X-33/RLV Program. This report consists of individual reports from all industry team members, as well as NASA team centers. This portion of the report is comprised of a status report of Lockheed Martin's contribution to the program. The following is a summary of the Lockheed Martin Centers involved and work reviewed under their portion of the agreement: (1) Lockheed Martin Skunk Works - Vehicle Development, Operations Development, X-33 and RLV Systems Engineering, Manufacturing, Ground Operations, Reliability, Maintainability/Testability, Supportability, & Special Analysis Team, and X-33 Flight Assurance; (2) Lockheed Martin Technical Operations - Launch Support Systems, Ground Support Equipment, Flight Test Operations, and RLV Operations Development Support; (3) Lockheed Martin Space Operations - TAEM and A/L Guidance and Flight Control Design, Evaluation of Vehicle Configuration, TAEM and A/L Dispersion Analysis, Modeling and Simulations, Frequency Domain Analysis, Verification and Validation Activities, and Ancillary Support; (4) Lockheed Martin Astronautics-Denver - Systems Engineering, X-33 Development; (5) Sanders - A Lockheed Martin Company - Vehicle Health Management Subsystem Progress, GSS Progress; and (6) Lockheed Martin Michoud Space Systems - X-33 Liquid Oxygen (LOX) Tank, Key Challenges, Lessons Learned, X-33/RLV Composite Technology, Reusable Cyrogenic Insulation (RCI) and Vehicle Health Monitoring, Main Propulsion Systems (MPS), Structural Testing, X-33 System Integration and Analysis, and Cyrogenic Systems Operations.

Source record↗

Development and Demonstration of an Ada Test Generation System

In this project we have built a prototype system that performs Feasible Path Analysis on Ada programs: given a description of a set of control flow paths through a procedure, and a predicate at a program point feasible path analysis determines if there is input data which causes execution to flow down some path in the collection reaching the point so that tile predicate is true. Feasible path analysis can be applied to program testing, program slicing, array bounds checking, and other forms of anomaly checking. FPA is central to most applications of program analysis. But, because this problem is formally unsolvable, syntactic-based approximations are used in its place. For example, in dead-code analysis the problem is to determine if there are any input values which cause execution to reach a specified program point. Instead an approximation to this problem is computed: determine whether there is a control flow path from the start of the program to the point. This syntactic approximation is efficiently computable and conservative: if there is no such path the program point is clearly unreachable, but if there is such a path, the analysis is inconclusive, and the code is assumed to be live. Such conservative analysis too often yields unsatisfactory results because the approximation is too weak. As another example, consider data flow analysis. A du-pair is a pair of program points such that the first point is a definition of a variable and the second point a use and for which there exists a definition-free path from the definition to the use. The sharper, semantic definition of a du-pair requires that there be a feasible definition-free path from the definition to the use. A compiler using du-pairs for detecting dead variables may miss optimizations by not considering feasibility. Similarly, a program analyzer computing program slices to merge parallel versions may report conflicts where none exist. In the context of software testing, feasibility analysis plays an important role in identifying testing requirements which are infeasible. This is especially true for data flow testing and modified condition/decision coverage. Our system uses in an essential way symbolic analysis and theorem proving technology, and we believe this work represents one of the few successful uses of a theorem prover working in a completely automatic fashion to solve a problem of practical interest. We believe this work anticipates an important trend away from purely syntactic-based methods for program analysis to semantic methods based on symbolic processing and inference technology. Other results demonstrating the practical use of automatic inference is being reported in hardware verification, although there are significant differences between the hardware work and ours. However, what is common and important is that general purpose theorem provers are being integrated with more special-purpose decision procedures to solve problems in analysis and verification. We are pursuina commercial opportunities for this work, and will use and extend the work in other projects we are engaged in. Ultimately we would like to rework the system to analyze C, C++, or Java as a key step toward commercialization.

Source record↗

NOS3: NASA Operational Simulator for Small Satellites

The NASA Operational Simulator for Small Satellites (NOS3) is a suite of open-source software tools to aid in areas such as software development, integration & test (I&T), mission operations/training, verification and validation (V&V), and software systems check-out. NOS3 provides a software development environment, a multi-target build system, operational interface/ground software, dynamics and environment simulations, and software-based hardware models. NOS3 has just recently been open-sourced by NASA and is available for immediate use. It enables the development of flight software (FSW) early in the project life cycle when hardware availability is limited. Small satellite development suffers from extensive lead times on many of the commercial-off-the-shelf (COTS) components as well as limited funding for engineering test units (ETUs). To alleviate the need to provide a hardware test-bed for each developer/tester, NOS3 hardware models are based upon characteristic data or manufacturer's data sheets for each individual component. The NOS3 hardware models' fidelity is such that FSW executes unaware that physical hardware is not present. This allows FSW binaries to be compiled for both the simulation environment and the flight computer without changing the FSW source code. For hardware models that provide data which is dependent upon the environment and spacecraft dynamics, such as a GPS receiver or magnetometer, an open-source tool from NASA GSFC (42 Spacecraft Simulator) is used to provide the necessary data. The underlying infrastructure used to transfer messages between FSW and the hardware models can also be used to monitor, intercept, and inject messages, which has proven to be beneficial for V&V of larger missions such as James Webb Space Telescope (JWST). As hardware is selected and becomes available, drivers can be added to the NOS3 environment to enable hardware-in-the-loop (HWIL) testing. When strict time synchronization is not vital, any number of combinations of hardware components and software-based models can be tested. NOS3 was actively used for FSW development and component testing of the Simulation-to-Flight 1 (STF-1) CubeSat and the Lunar IceCube CubeSat. As NOS3 matures, hardware models have been added for common small satellite components such as GPS receivers, electrical power systems and batteries, and antenna systems.

Suder, Mark↗

Virtual Satellite

Virtual Satellite (VirtualSat) is a computer program that creates an environment that facilitates the development, verification, and validation of flight software for a single spacecraft or for multiple spacecraft flying in formation. In this environment, enhanced functionality and autonomy of navigation, guidance, and control systems of a spacecraft are provided by a virtual satellite that is, a computational model that simulates the dynamic behavior of the spacecraft. Within this environment, it is possible to execute any associated software, the development of which could benefit from knowledge of, and possible interaction (typically, exchange of data) with, the virtual satellite. Examples of associated software include programs for simulating spacecraft power and thermal- management systems. This environment is independent of the flight hardware that will eventually host the flight software, making it possible to develop the software simultaneously with, or even before, the hardware is delivered. Optionally, by use of interfaces included in VirtualSat, hardware can be used instead of simulated. The flight software, coded in the C or C++ programming language, is compilable and loadable into VirtualSat without any special modifications. Thus, VirtualSat can serve as a relatively inexpensive software test-bed for development test, integration, and post-launch maintenance of spacecraft flight software.

Hammrs, Stephan R.↗

CropEx Web-Based Agricultural Monitoring and Decision Support

CropEx is a Web-based agricultural Decision Support System (DSS) that monitors changes in crop health over time. It is designed to be used by a wide range of both public and private organizations, including individual producers and regional government offices with a vested interest in tracking vegetation health. The database and data management system automatically retrieve and ingest data for the area of interest. Another stores results of the processing and supports the DSS. The processing engine will allow server-side analysis of imagery with support for image sub-setting and a set of core raster operations for image classification, creation of vegetation indices, and change detection. The system includes the Web-based (CropEx) interface, data ingestion system, server-side processing engine, and a database processing engine. It contains a Web-based interface that has multi-tiered security profiles for multiple users. The interface provides the ability to identify areas of interest to specific users, user profiles, and methods of processing and data types for selected or created areas of interest. A compilation of programs is used to ingest available data into the system, classify that data, profile that data for quality, and make data available for the processing engine immediately upon the data s availability to the system (near real time). The processing engine consists of methods and algorithms used to process the data in a real-time fashion without copying, storing, or moving the raw data. The engine makes results available to the database processing engine for storage and further manipulation. The database processing engine ingests data from the image processing engine, distills those results into numerical indices, and stores each index for an area of interest. This process happens each time new data is ingested and processed for the area of interest, and upon subsequent database entries, the database processing engine qualifies each value for each area of interest and conducts a logical processing of results indicating when and where thresholds are exceeded. Reports are provided at regular, operator-determined intervals that include variances from thresholds and links to view raw data for verification, if necessary. The technology and method of development allow the code base to easily be modified for varied use in the real-time and near-real-time processing environments. In addition, the final product will be demonstrated as a means for rapid draft assessment of imagery.

Harvey. Craig↗

Security Vulnerability Profiles of NASA Mission Software: Empirical Analysis of Security Related Bug Reports

NASA develops, runs, and maintains software systems for which security is of vital importance. Therefore, it is becoming an imperative to develop secure systems and extend the current software assurance capabilities to cover information assurance and cybersecurity concerns of NASA missions. The results presented in this report are based on the information provided in the issue tracking systems of one ground mission and one flight mission. The extracted data were used to create three datasets: Ground mission IVV issues, Flight mission IVV issues, and Flight mission Developers issues. In each dataset, we identified the software bugs that are security related and classified them in specific security classes. This information was then used to create the security vulnerability profiles (i.e., to determine how, why, where, and when the security vulnerabilities were introduced) and explore the existence of common trends. The main findings of our work include:- Code related security issues dominated both the Ground and Flight mission IVV security issues, with 95 and 92, respectively. Therefore, enforcing secure coding practices and verification and validation focused on coding errors would be cost effective ways to improve mission's security. (Flight mission Developers issues dataset did not contain data in the Issue Category.)- In both the Ground and Flight mission IVV issues datasets, the majority of security issues (i.e., 91 and 85, respectively) were introduced in the Implementation phase. In most cases, the phase in which the issues were found was the same as the phase in which they were introduced. The most security related issues of the Flight mission Developers issues dataset were found during Code Implementation, Build Integration, and Build Verification; the data on the phase in which these issues were introduced were not available for this dataset.- The location of security related issues, as the location of software issues in general, followed the Pareto principle. Specifically, for all three datasets, from 86 to 88 the security related issues were located in two to four subsystems.- The severity levels of most security issues were moderate, in all three datasets.- Out of 21 primary security classes, five dominated: Exception Management, Memory Access, Other, Risky Values, and Unused Entities. Together, these classes contributed from around 80 to 90 of all security issues in each dataset. This again proves the Pareto principle of uneven distribution of security issues, in this case across CWE classes, and supports the fact that addressing these dominant security classes provides the most cost efficient way to improve missions' security. The findings presented in this report uncovered the security vulnerability profiles and identified the common trends and dominant classes of security issues, which in turn can be used to select the most efficient secure design and coding best practices compiled by the part of the SARP project team associated with the NASA's Johnson Space Center. In addition, these findings provide valuable input to the NASA IVV initiative aimed at identification of the two 25 CWEs of ground and flight missions.

vulnerability↗