SEARCH · Engineering Papers
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.
Under a NASA-Ames Space Act Agreement, Coryphaeus Software and Simauthor, Inc., developed an Aviation Performance Measuring System (APMS). This software, developed for the aerospace and airline industry, enables the replay of Digital Flight Data Recorder (DFDR) data in a flexible, user-configurable, real-time, high fidelity 3D (three dimensional) environment.
Runtime Assurance (RTA) is a design-time architecture for safety-critical systems where an internal monitor acts upon detecting a violation of a property. The simplex architecture is an instance of RTA, where the action taken is to hand control of the overall system to a trusted controller when an untrusted one violates a safety property. Simplex RTA is emerging as a method for allowing AI/ML and other unverified software to be integrated into safety-critical applications like aircraft. To this end, the American Society for Testing and Materials (ASTM) and NASA have each published guidelines on the use of RTA in such systems. In the simplex RTA framework, a system has an advanced controller (AC) and a reversionary controller (RC). The system is allowed to operate with the AC until a runtime monitor detects that some property has been violated and then the RC takes over. Assuming that the sample rate of the monitor will detect improper functioning with enough time for the RC to correct the impending problem, and that the RC is trusted, the system will operate as intended. This use of the simplex RTA framework can allow for the integration of untrusted, but possibly more performant, controllers in a safe way. This paper presents a formalization of a simplex RTA framework in the Prototype Verification System (PVS) theorem prover using an embedding of differential dynamic logic (DDL) called Plaidypvs. A novel feature of this framework is that it can be instantiated at different levels of abstraction. This feature allows for the formal verification of a system with an untrusted black box component, such as an AI/ML controller. This paper does not address the many difficulties in deploying RTA in an industrial-level system. Instead, the focus is on the formal verification of the simplex RTA framework in the language of hybrid programs. Hybrid programs are programs that include both discrete and continuous dynamics and can be used to model complex cyber-physical systems. Plaidypvs is a tool that enables formalization of hybrid programs in the PVS theorem prover. Plaidypvs enables the verification of the general simplex RTA framework and then, by specializing some components of the hybrid program, verifying instances of the framework while treating the untrusted component as a black box. A selection of Unmanned Aircraft Systems (UAS) operations are shown as instances of the general RTA framework in PVS. This offers the benefit of design time verification of relevant safety properties to the system, and it also gives requirements on the sample rate of sensors that determine the time interval in which the ‘switch’ property of the RTA framework is checked.
The Embedded System Safety Analysis Assistant (ESSAA) is a knowledge-based tool that can assist in identifying disaster scenarios. Imbedded software issues hazardous control commands to the surrounding hardware. ESSAA is intended to work from outputs to inputs, as a complement to simulation and verification methods. Rather than treating the software in isolation, it examines the context in which the software is to be deployed. Given a specified disasterous outcome, ESSAA works from a qualitative, abstract model of the complete system to infer sets of environmental conditions and/or failures that could cause a disasterous outcome. The scenarios can then be examined in depth for plausibility using existing techniques.
The area of software analysis, testing and verification is now undergoing a revolution thanks to the use of automated and scalable support for logical methods. A well-recognized premise is that at the core of software analysis engines is invariably a component using logical formulas for describing states and transformations between system states. The process of using this information for discovering and checking program properties (including such important properties as safety and security) amounts to automatic theorem proving. In particular, theorem provers that directly support common software constructs offer a compelling basis. Such provers are commonly called satisfiability modulo theories (SMT) solvers. Z3 is a state-of-the-art SMT solver. It is developed at Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories such as arithmetic, bit-vectors, lists, records and arrays. The talk describes some of the technology behind modern SMT solvers, including the solver Z3. Z3 is currently mainly targeted at solving problems that arise in software analysis and verification. It has been applied to various contexts, such as systems for dynamic symbolic simulation (Pex, SAGE, Vigilante), for program verification and extended static checking (Spec#/Boggie, VCC, HAVOC), for software model checking (Yogi, SLAM), model-based design (FORMULA), security protocol code (F7), program run-time analysis and invariant generation (VS3). We will describe how it integrates support for a variety of theories that arise naturally in the context of the applications. There are several new promising avenues and the talk will touch on some of these and the challenges related to SMT solvers. Proceedings
With the advances in high-computing platform (e.g., advanced graphical processing units or multi-core processors), computationally-intensive software techniques such as the ones used in artificial intelligence or formal methods have provided us with an opportunity to further increase safety in the aviation industry. Some of these techniques have facilitated building safety at design time, like in aircraft engines or software verification and validation, and others can introduce safety benefits during operations as long as we adapt our processes. In this talk, I will present how NASA is taking advantage of these new software techniques to build in safety at design time through advanced software verification and validation, which can be applied earlier and earlier in the design life cycle and thus help also reduce the cost of aviation assurance. I will then show how run-time techniques (such as runtime assurance or data analytics) offer us a chance to catch even more complex problems, even in the face of changing and unpredictable environments. These new techniques will be extremely useful as our aviation systems become more complex and more autonomous.
Preliminary and detailed design studies were performed to mature composite structural design concepts for the Ares V Interstage structure as a part of NASA s Advanced Composite Technologies Project. Aluminum honeycomb sandwich and hat-stiffened composite panel structural concepts were considered. The structural design and analysis studies were performed using HyperSizer design sizing software and MSC Nastran finite element analysis software. System-level design trade studies were carried out to predict weight and margins of safety for composite honeycomb-core sandwich and composite hat-stiffened skin design concepts. Details of both preliminary and detailed design studies are presented in the paper. For the range of loads and geometry considered in this work, the hat-stiffened designs were found to be approximately 11-16 percent lighter than the sandwich designs. A down-select process was used to choose the most favorable structural concept based on a set of figures of merit, and the honeycomb sandwich design was selected as the best concept based on advantages in manufacturing cost.
Space ROS is a matured version of ROS 2 using flight software engineering practices to facilitate mission- and safety-critical applications. Our goal is to reduce the barrier to maturation and infusion of software developed using the popular ROS framework.
An important objective of the Semi-Span Super-Sonic Transport (S4T) wind tunnel model program was the demonstration of Flutter Suppression (FS), Gust Load Alleviation (GLA), and Ride Quality Enhancement (RQE). It was critical to evaluate the stability and robustness of these control laws analytically before testing them and experimentally while testing them to ensure safety of the model and the wind tunnel. MATLAB based software was applied to evaluate the performance of closed-loop systems in terms of stability and robustness. Existing software tools were extended to use analytical representations of the S4T and the control laws to analyze and evaluate the control laws prior to testing. Lessons were learned about the complex windtunnel model and experimental testing. The open-loop flutter boundary was determined from the closed-loop systems. A MATLAB/Simulink Simulation developed under the program is available for future work to improve the CPE process. This paper is one of a series of that comprise a special session, which summarizes the S4T wind-tunnel program.
The Planning Execution Monitoring (PEM) architecture is a design concept for developing autonomous cockpit command and control software. The PEM architecture is designed to reduce the operations costs in the space transportation system through the use of automation while improving safety and operability of the system. Specifically, the PEM autonomous framework enables automatic performance of many vehicle operations that would typically be performed by a human. Also, this framework supports varying levels of autonomous control, ranging from fully automatic to fully manual control. The PEM autonomous framework interfaces with the core flight software to perform flight procedures. It can either assist human operators in performing procedures or autonomously execute routine cockpit procedures based on the operational context. Most importantly, the PEM autonomous framework promotes and simplifies the capture, verification, and validation of the flight operations knowledge. Through a hierarchical decomposition of the domain knowledge, the vehicle command and control capabilities are divided into manageable functional "chunks" that can be captured and verified separately. These functional units, each of which has the responsibility to manage part of the vehicle command and control, are modular, re-usable, and extensible. Also, the functional units are self-contained and have the ability to plan and execute the necessary steps for accomplishing a task based upon the current mission state and available resources. The PEM architecture has potential for application outside the realm of spaceflight, including management of complex industrial processes, nuclear control, and control of complex vehicles such as submarines or unmanned air vehicles.
1. Kennedy Space Center (KSC) is developing a mobile launching system with autonomous propellant loading capabilities for liquid-fueled rockets. An autonomous system will be responsible for monitoring and controlling the storage, loading and transferring of cryogenic propellants. The Physics Simulation Software will reproduce the sensor data seen during the delivery of cryogenic fluids including valve positions, pressures, temperatures and flow rates. The simulator will provide insight into the functionality of the propellant systems and demonstrate the effects of potential faults. This will provide verification of the communications protocols and the autonomous system control. 2. The High Pressure Gas Facility (HPGF) stores and distributes hydrogen, nitrogen, helium and high pressure air. The hydrogen and nitrogen are stored in cryogenic liquid state. The cryogenic fluids pose several hazards to operators and the storage and transfer equipment. Constant monitoring of pressures, temperatures and flow rates are required in order to maintain the safety of personnel and equipment during the handling and storage of these commodities. The Gas House Autonomous System Monitoring software will be responsible for constantly observing and recording sensor data, identifying and predicting faults and relaying hazard and operational information to the operators.
Fault tolerance and safety verification of control systems are essential for the success of autonomous robotic systems. A control architecture called Mission Data System (MDS), developed at the Jet Propulsion Laboratory, takes a goal-based control approach. In this paper, a method for converting goal network control programs into linear hybrid systems is developed. The linear hybrid system can then be verified for safety in the presence of failures using existing symbolic model checkers. An example task is simulated in MDS and successfully verified using HyTech, a symbolic model checking software for linear hybrid systems.
Within the pressurized elements of the International Space Station (ISS), requirements exist to ensure a safe, habitable environment for the crew. In order to provide this environment, thermal control components work in conjunction with software controls to provide heat rejection for subsystem avionics equipment, for the environmental control system and for experiment payloads. It is essential to ISS operations, mission success and crew safety that necessary testing incorporates the extreme conditions to ensure proper performance. This paper provides a general description and methodology applied to thermal related Hardware/Software Integration (HSI) tests for the ISS Node 2 module. A detailed test plan was developed and implemented with two objectives: the first was for risk mitigation of the thermal control algorithms and software qualification, and the second was for data collection which will substantiate thermalhydraulic models of the Internal Active Thermal Control System (IATCS). Analytical models are utilized to determine on-orbit performance for conditions and scenarios where the simulation of actual on-orbit system performance is limited by test configuration constraints. Node 2 IATCS HSI activities were performed at the Alenia Spazio facility in Torino, Italy with participation from the National Aeronautics and Space Administration (NASA), Alenia Spazio, Jacobs Engineering Sverdrup (JE Sverdrup) and Boeing.
Within the past decade, software has become an increasingly common element in computing systems. In particular, the role of software used in the aerospace industry, especially in life- or safety-critical applications, is rapidly expanding. This intensifies the need to use effective techniques for achieving and verifying the reliability of avionics software. Although certain software development processes and techniques are mandated by government regulating agencies, no one methodology has been shown to consistently produce reliable software. The knowledge base for designing reliable software simply has not reached the maturity of its hardware counterpart. In an effort to increase our understanding of software, the Langley Research Center conducted a series of experiments over 15 years with the goal of understanding why and how software fails. As part of this program, the effectiveness of current industry standards for the development of avionics is being investigated. This study involves the generation of a controlled environment to conduct scientific experiments on software processes.
An inverse differential GPS system has been developed for Sounding Rocket use which includes the flight unit and a ground station capable of extracting GPS data from sounding rocket telemetry, performing a real time differential solution and graphically displaying the rocket's path relative to a predicted trajectory plot. Accuracy has been proven to within less than 10 meters. Postprocessing has increased the precision to within 10 - 20 centimeters. The system has been successfully flown several times and delivered to the Sounding Program Office for routine field use. In addition to providing position, velocity and time GPS data has been used on sounding rockets for vehicle performance analysis, effecting a one hundred fold improvement in data time tagging, and steering an optical tracking device to intercept payloads launched from over the horizon. Precise velocity separation information and timing has been provided to multiple payload systems. Future plans include its use for Range Safety and enabling of interferometric techniques. The technology and software developed also has potential application to small satellite navigation and formation flying.
For about two decades, compliance with Software Considerations in Airborne Systems and Equipment Certification (DO-178B) has been the primary means for receiving regulatory approval for using software on commercial airplanes. A new edition of the standard, DO-178C, was published in December 2011, and regulatory bodies have started the process towards recognizing this edition. The stated purpose of DO-178C remains unchanged from its predecessor: providing guidance “for the production of software for airborne systems and equipment that performs its intended function with a level of confidence in safety that complies with airworthiness requirements.” Within the text of the guidance, little or no rationale is given for how a particular objective or collection of objectives contributes to achieving this purpose. Thus the assurance case for the document is implicit. This paper discusses a current effort to make the implicit explicit. In particular, the paper describes the current status of the research seeking to identify the specific arguments contained in, or implied by, the DO-178C guidance that implicitly justify the assumption that the document meets its stated purpose.
For about two decades, compliance with Software Considerations in Airborne Systems and Equipment Certification (DO-178B/ED-12B) has been the primary means for receiving regulatory approval for using software on commercial airplanes. A new edition of the standard, DO-178C/ED-12C, was published in December 2011, and recognized by regulatory bodies in 2013. The purpose remains unchanged: to provide guidance 'for the production of software for airborne systems and equipment that performs its intended function with a level of confidence in safety that complies with airworthiness requirements.' The text of the guidance does not directly explain how its collection of objectives contributes to achieving this purpose; thus, the assurance case for the document is implicit. This paper presents an explicit assurance case developed as part of research jointly sponsored by the Federal Aviation Administration and the National Aeronautics and Space Administration.
Projected increases in new vehicle types, new missions, and the continual growth in traditional (e.g., airlines, general aviation) aviation will require changes to the current air traffic system, particularly to accommodate the desire of operators to be more involved in air traffic decisions. To address these challenges, the National Airspace System needs to undergo a transformation to a more scalable, flexible, user-focused system that addresses safety and security requirements and resiliency for current and new users. A system designed to integrate modular software services, provided by users, third parties and government for air traffic management functions, will be scalable and more easily allow modernization and for collaboration between users and service providers. ATM-X is responding to NASA's pivot towards integrating projected new, diverse entrants into the NAS, while also leveraging NASA's prior ATM achievements that continue to improve traditional airspace operations. This project is a two-phased approach to conduct research and focused evaluations to assess the feasibility of a service-based approach and to identify critical design considerations to enable airspace access for new entrants, integrated with current traditional operations. Phase 1 research will be conducted to determine what is needed to reach the ATM-X goals based on specific use-cases to enable large-scale, passenger-carrying Urban Air Mobility operations in a metroplex environment, and also to improve traditional operations in the Northeast Region leveraging mature NASA technologies. Some of these evaluations will be conducted in simulations and field activities. Phase 2 will build upon Phase 1 towards more defined, focused research and field demonstrations in real-world environments to integrate multiple elements of a scalable, service-based ATM-X concept.
This presentation goes over some of the tools developed at NASA Ames in the Robust Software Engineering group for the assurance and certification of autonomous systems. The research themes presented include improving safety and risk assessment as early as possible in the lifecycle, elicitation and formalization of requirements to facilitate traceability throughout the lifecycle, especially when formal methods are used, algorithms, tools and techniques for the V&V of ML-enabled systems, advanced testing, use of runtime monitoring to ease use of untrusted components, and contribution to draft regulatory standards and assistance in producing and presenting certification evidences.