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.
In this paper, an analytical approach for studying the contact dynamics of space-based vehicles during docking/berthing maneuvers is presented. Methods for modeling physical contact between docking/berthing mechanisms, examples of how these models have been used to evaluate the dynamic behavior of automated capture mechanisms, and experimental verification of predicted results are shown.
The first Conference of C Language Production Systems (CLIPS) hosted by the NASA-Lyndon B. Johnson Space Center in August 1990 is presented. Articles included engineering applications, intelligent tutors and training, intelligent software engineering, automated knowledge acquisition, network applications, verification and validation, enhancements to CLIPS, space shuttle quality control/diagnosis applications, space shuttle and real-time applications, and medical, biological, and agricultural applications.
This describes a knowledge base (KB) partitioning approach to solve the problem of real-time performance using the CLIPS AI shell when containing large numbers of rules and facts. This work is funded under the joint USAF/NASA Advanced Launch System (ALS) Program as applied research in expert systems to perform vehicle checkout for real-time controller and diagnostic monitoring tasks. The Expert System advanced development project (ADP-2302) main objective is to provide robust systems responding to new data frames of 0.1 to 1.0 second intervals. The intelligent system control must be performed within the specified real-time window, in order to meet the demands of the given application. Partitioning the KB reduces the complexity of the inferencing Rete net at any given time. This reduced complexity improves performance but without undo impacts during load and unload cycles. The second objective is to produce highly reliable intelligent systems. This requires simple and automated approaches to the KB verification & validation task. Partitioning the KB reduces rule interaction complexity overall. Reduced interaction simplifies the V&V testing necessary by focusing attention only on individual areas of interest. Many systems require a robustness that involves a large number of rules, most of which are mutually exclusive under different phases or conditions. The ideal solution is to control the knowledge base by loading rules that directly apply for that condition, while stripping out all rules and facts that are not used during that cycle. The practical approach is to cluster rules and facts into associated 'blocks'. A simple approach has been designed to control the addition and deletion of 'blocks' of rules and facts, while allowing real-time operations to run freely. Timing tests for real-time performance for specific machines under R/T operating systems have not been completed but are planned as part of the analysis process to validate the design.
As our society becomes technologically more complex, computers are being used in greater and greater numbers of high consequence systems. Giving a machine control over the lives of humans can be disturbing, especially if the software that is run on such a machine has bugs. Formal reasoning is one of the most powerful techniques available to demonstrate the correctness of a piece of software. When reasoning about software and its development, one frequently encounters expressions that contain partial functions. As might be expected, the presence of partial functions introduces an additional dimension of difficulty to the reasoning framework. This difficulty produces an especially strong impact in the case of high consequence systems. An ability to use formal methods for constructing software is essential if we want to obtain greater confidence in such systems through formal reasoning. This is only reasonable under automation of software development and verification. However, the ubiquitous presence of partial functions prevents a uniform application to software of any tools not specifically accounting for partial functions. In this paper we will describe a framework for reasoning about software, based on the nonstrict explicit domain approach, that is applicable to a large class of software/hardware systems. In this framework the Hoare triples containing partial functions can be reasoned about automatically in a well-defined and uniform manner.
This paper presents the specification and verification in the Prototype Verification System (PVS) of a protocol intended to facilitate communication in an experimental remotely operated vehicle used by NASA researchers. The protocol is defined as a stack-layered com- position of simpler protocols. It can be seen as the vertical composition of protocol layers, where each layer performs input and output message processing, and the horizontal composition of different processes concurrently inhabiting the same layer, where each process satisfies a distinct requirement. It is formally proven that the protocol components satisfy certain delivery guarantees. Compositional techniques are used to prove these guarantees also hold in the composed system. Although the protocol itself is not novel, the methodology employed in its verification extends existing techniques by automating the tedious and usually cumbersome part of the proof, thereby making the iterative design process of protocols feasible.
A sextant provides manual capability to perform star/planet-limb sightings and offers a cheap, simple, robust backup navigation source for exploration missions independent from the ground. Sextant sightings from spacecraft were first exercised in Gemini and flew as the lost-communication backup for all Apollo missions. This study characterized error sources of navigation-grade sextants for feasibility of taking star and planetary limb sightings from inside a spacecraft. A series of similar studies was performed in the early/mid-1960s in preparation for Apollo missions. This study modernized and updated those findings in addition to showing feasibility using Linear Covariance analysis techniques. The human eyeball is a remarkable piece of optical equipment and provides many advantages over camera-based systems, including dynamic range and detail resolution. This technique utilizes those advantages and provides important autonomy to the crew in the event of lost communication with the ground. It can also provide confidence and verification of low-TRL automated onboard systems. The technique is extremely flexible and is not dependent on any particular vehicle type. The investigation involved procuring navigation-grade sextants and characterizing their performance under a variety of conditions encountered in exploration missions. The JSC optical sensor lab and Orion mockup were the primary testing locations. For the accuracy assessment, a group of test subjects took sextant readings on calibrated targets while instrument/operator precision was measured. The study demonstrated repeatability of star/planet-limb sightings with bias and standard deviation around 10 arcseconds, then used high-fidelity simulations to verify those accuracy levels met the needs for targeting mid-course maneuvers in preparation for Earth reen.
In this tutorial, we present the FRET tool for writing, understanding, formalizing and analyzing requirements. In practice, requirements are typically written in natural language, which is ambiguous and consequently not amenable to formal analysis. Since formal, mathematical notations are unintuitive, requirements in FRET are entered in a restricted, natural language, called FRETish with precise unambiguous meaning. This tutorial explains how requirements can be captured in FRETish and subsequently formalized in temporal logics and in the synchronous data flow language Lustre. We show, through multiple examples, how FRET assists users in understanding FRETish requirements and clarifying subtle semantic issues through English and diagrammatic explanations as well as interactive simulation. FInally, this tutorial describes how FRET can be used to perform realizability checking for identifying conflicting requirements and the connection of FRET with (1) the CoCoSim automated analysis tool for the verification of Simulink and Stateflow models, and (2) the Copilot runtime monitoring tool for the analysis of C programs.
Space station productivity is treated from a systems point of view, considering the functions and attributes of space station development, formation, and operation that affect productivity. An optimum planning method is needed to assure that the station will have mission flexibility, technology advancement, maintainability, and evolutionary capability. Advanced technology will be designed into the housekeeping and utility functions of the station. Greater risk taking may be allowed into designs if the potential benefits of the advanced system support the risk, and if the system can be buffered from causing a failure cascade throughout the station. A common data base is needed to store and track all designs, developments, and changes in the station subsystems. Systems that can be automated and free the human inhabitants for more productive work are favored, as are modular components that are highly fault-free. Human control must also be possible, especially during check-out and verification, and also for teaching the automated systems new or modified tasks.
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.
This paper describes the development, design, and implementation of the Requirements, Verification, and Compliance (RVC) database used on the International Space Welding Experiment (ISWE) project managed at Marshall Space Flight Center. The RVC is a systems engineer's tool for automating and managing the following information: requirements; requirements traceability; verification requirements; verification planning; verification success criteria; and compliance status. This information normally contained within documents (e.g. specifications, plans) is contained in an electronic database that allows the project team members to access, query, and status the requirements, verification, and compliance information from their individual desktop computers. Using commercial-off-the-shelf (COTS) database software that contains networking capabilities, the RVC was developed not only with cost savings in mind but primarily for the purpose of providing a more efficient and effective automated method of maintaining and distributing the systems engineering information. In addition, the RVC approach provides the systems engineer the capability to develop and tailor various reports containing the requirements, verification, and compliance information that meets the needs of the project team members. The automated approach of the RVC for capturing and distributing the information improves the productivity of the systems engineer by allowing that person to concentrate more on the job of developing good requirements and verification programs and not on the effort of being a "document developer".
Assurance cases are being increasingly acknowledged as away to build trust in complex systems with autonomous capabilities. An assurance case is a comprehensive, defensible, and valid justification that a system will function as intended for a specific mission and operating environment. Formal verification is often reserved for the most critical components of such systems. However, formal verification tools are often complex, and their usage is subject to many constraints and contextual dependencies. This can raise challenges both for performing the verification as well as reflecting the verification results appropriately in the assurance case, especially for non-expert users of the verification tool. To address these challenges, we present a tool-supported methodology for integrating formal verification results in an assurance case by capturing key verification method information in a rigorously constructed assurance case. In particular, we capture the tool specification in terms of its inputs, outputs, and assurance constraints as assumptions over inputs and guarantees provided over its outputs. The tool specification is parametrized over the inputs and outputs to both guide the intended application of the tool, as well as to check that the tool has been applied following the stated assumptions and that the guarantees hold. We define a generic tool assurance argument pattern that enables integration of the verification results in the assurance case by allowing custom refinement and automated instantiation for each tool use. We demonstrate our methodology on two formal verification tools and their applications to the verification of neural network properties for the aircraft domain.
Sparse distributed memory is a generalized random access memory (RAM) for long binary words. Such words can be written into and read from the memory, and they can be used to address the memory. The main attribute of the memory is sensitivity to similarity, meaning that a word can be read back not only by giving the original right address but also by giving one close to it as measured by the Hamming distance between addresses. Large memories of this kind are expected to have wide use in speech and scene analysis, in signal detection and verification, and in adaptive control of automated equipment. The memory can be realized as a simple, massively parallel computer. Digital technology has reached a point where building large memories is becoming practical. The research is aimed at resolving major design issues that have to be faced in building the memories. The design of a prototype memory with 256-bit addresses and from 8K to 128K locations for 256-bit words is described. A key aspect of the design is extensive use of dynamic RAM and other standard components.
Sparse distributed memory is a generalized random access memory (RAM) for long (1000 bit) binary words. Such words can be written into and read from the memory, and they can also be used to address the memory. The main attribute of the memory is sensitivity to similarity, meaning that a word can be read back not only by giving the original write address but also by giving one close to it as measured by the Hamming distance between addresses. Large memories of this kind are expected to have wide use in speech recognition and scene analysis, in signal detection and verification, and in adaptive control of automated equipment, in general, in dealing with real world information in real time. The memory can be realized as a simple, massively parallel computer. Digital technology has reached a point where building large memories is becoming practical. Major design issues were resolved which were faced in building the memories. The design is described of a prototype memory with 256 bit addresses and from 8 to 128 K locations for 256 bit words. A key aspect of the design is extensive use of dynamic RAM and other standard components.
The future of humanity’s presence beyond Earth depends on the successful commercialization of space. For commercialization to succeed, companies need cost-efficient architectures to support their business models and minimize risks for human capital, design, development, and operations. An ongoing challenge to any space enterprise is the reality that terrestrial network technologies are insufficient to provide reliable communications between assets in space. Whether you need to ensure your valuable data is safely transmitted to the ground or reliably delivered between platforms in orbit, ensuring data integrity over intermittent communication links is a necessity. Current solutions to space communications rely heavily on manual recording, storing, and retrieval of data from spacecraft. The current standard in space communication protocols, Consultative Committee for Space Data Systems (CCSDS) Space Packet standard, is reliant on inflexible network architectures based around mission-critical infrastructure to ensure data delivery. However, by automating the recording, storing, retrieval, and verification of data with Delay Tolerant Networks (DTN), the operator is freed from the dependence on manual data management and expensive mission critical infrastructure. NASA has been developing delay tolerant systems since the late 1990’s. Multiple DTN implementations have been established during that time, each suited to different use cases. Most notably, the DTN deployment for the International Space Station (ISS) includes demonstration of two DTN technologies: Interplanetary Overlay Network (ION) and Delay Tolerant Network Marshall Enterprise (DTNME). Beyond ISS, there are even more NASA DTN deployments being considered. Now that DTN implementations are maturing, it is appropriate to reflect upon these decades of work, review the integration and performance of the existing ISS deployment, and explore the future possibilities for DTN deployment industry-wide. The ISS DTN deployment is a complex architecture consisting of different DTN implementations for the onboard and ground network environments. The ION DTN implementation is being used in the on-board network. The Huntsville Operations Support Center (HOSC) DTN implementation, DTNME, is used by the ground network supporting ISS and will soon be a second onboard gateway too. The two implementations work cooperatively to provide high fidelity data services to flight operations users and payload developers across the globe. Though the two implementations yield a quality service, limitations are evident. Data rate, data storage, and device management are constrained by the services themselves and the complex nature of the deployment. Evolution of operations concepts will improve system capabilities and stability, but significant improvement will require additional development to the implementations themselves and to the overall deployment architecture. Taking advantage of the ongoing development and operation of the ISS DTN service will be central to the success of the future evolutions of NASA DTN deployments while demonstrating the benefits of DTN’s low-cost reliable data communication protocols for the growing commercial space industry. A broad effort on DTN integration and support is necessary to promote expansion beyond existing applications. NASA is developing several useful DTN implementations across a number of different systems: ION, DTNME, High-Rate DTN (HDTN), Bundle Protocol Library (BPLib), and others. To prevent fragmentation, DTN implementation teams need to communicate, collaborate, and integrate with one another to build a solid operational foundation for new DTN deployments. The establishment of a group that can assist new DTN users with understanding the purpose of each DTN implementation, provide best practices, and serve as a general knowledge base is paramount. Potential use of DTN on Gateway and other future NASA missions further drives the need for streamlined communication between DTN implementation teams. A well-integrated and highly engaged NASA DTN working group should help provide system architects the best DTN solutions for future commercial space efforts. This paper will first review the history of DTN implementations, explore the shortcoming of current space networking solutions given available limits in technology, and therefore establish the need for Delay Tolerant Networking in space communications. Secondly, the authors will explore NASA’s array of DTN implementations and highlight their usefulness to space applications. Thirdly, this paper will establish general DTN implementation distinguishing factors. Fourthly, the authors will discuss attempts to create a generic DTN comparison matrix, and the authors will review potential future topics in DTN innovation and collaboration, highlighting several key future efforts. Finally, this paper will describe how the institution of a NASA DTN Working Group will benefit DTN adoption across the governmental and commercial space sector. The goal of this paper is to encourage enthusiasm for DTN, share strategies for improving DTN on both current and future applications, promote the collaboration of DTN implementation groups within the international space operations community, and open the conversations about DTN, priorities, complexities, and innovation to the wider spaceflight industry.
The future of humanity’s presence beyond Earth depends on the successful commercialization of space. For commercialization to succeed, companies need cost-efficient architectures to support their business models and minimize risks for human capital, design, development, and operations. An ongoing challenge to any space enterprise is the reality that terrestrial network technologies are insufficient to provide reliable communications between assets in space. Whether you need to ensure your valuable data is safely transmitted to the ground or reliably delivered between platforms in orbit, ensuring data integrity over intermittent communication links is a necessity. Current solutions to space communications rely heavily on manual recording, storing, and retrieval of data from spacecraft. The current standard in space communication protocols, Consultative Committee for Space Data Systems (CCSDS) Space Packet standard, is reliant on inflexible network architectures based around mission-critical infrastructure to ensure data delivery. However, by automating the recording, storing, retrieval, and verification of data with Delay Tolerant Networks (DTN), the operator is freed from the dependence on manual data management and expensive mission critical infrastructure. NASA has been developing delay tolerant systems since the late 1990’s. Multiple DTN implementations have been established during that time, each suited to different use cases. Most notably, the DTN deployment for the International Space Station (ISS) includes demonstration of two DTN technologies: Interplanetary Overlay Network (ION) and Delay Tolerant Network Marshall Enterprise (DTNME). Beyond ISS, there are even more NASA DTN deployments being considered. Now that DTN implementations are maturing, it is appropriate to reflect upon these decades of work, review the integration and performance of the existing ISS deployment, and explore the future possibilities for DTN deployment industry-wide. The ISS DTN deployment is a complex architecture consisting of different DTN implementations for the onboard and ground network environments. The ION DTN implementation is being used in the on-board network. The Huntsville Operations Support Center (HOSC) DTN implementation, DTNME, is used by the ground network supporting ISS and will soon be a second onboard gateway too. The two implementations work cooperatively to provide high fidelity data services to flight operations users and payload developers across the globe. Though the two implementations yield a quality service, limitations are evident. Data rate, data storage, and device management are constrained by the services themselves and the complex nature of the deployment. Evolution of operations concepts will improve system capabilities and stability, but significant improvement will require additional development to the implementations themselves and to the overall deployment architecture. Taking advantage of the ongoing development and operation of the ISS DTN service will be central to the success of the future evolutions of NASA DTN deployments while demonstrating the benefits of DTN’s low-cost reliable data communication protocols for the growing commercial space industry. A broad effort on DTN integration and support is necessary to promote expansion beyond existing applications. NASA is developing several useful DTN implementations across a number of different systems: ION, DTNME, High-Rate DTN (HDTN), Bundle Protocol Library (BPLib), and others. To prevent fragmentation, DTN implementation teams need to communicate, collaborate, and integrate with one another to build a solid operational foundation for new DTN deployments. The establishment of a group that can assist new DTN users with understanding the purpose of each DTN implementation, provide best practices, and serve as a general knowledge base is paramount. Potential use of DTN on Gateway and other future NASA missions further drives the need for streamlined communication between DTN implementation teams. A well-integrated and highly engaged NASA DTN working group should help provide system architects the best DTN solutions for future commercial space efforts. This paper will first review the history of DTN implementations, explore the shortcoming of current space networking solutions given available limits in technology, and therefore establish the need for Delay Tolerant Networking in space communications. Secondly, the authors will explore NASA’s array of DTN implementations and highlight their usefulness to space applications. Thirdly, this paper will establish general DTN implementation distinguishing factors. Fourthly, the authors will discuss attempts to create a generic DTN comparison matrix, and the authors will review potential future topics in DTN innovation and collaboration, highlighting several key future efforts. Finally, this paper will describe how the institution of a NASA DTN Working Group will benefit DTN adoption across the governmental and commercial space sector. The goal of this paper is to encourage enthusiasm for DTN, share strategies for improving DTN on both current and future applications, promote the collaboration of DTN implementation groups within the international space operations community, and open the conversations about DTN, priorities, complexities, and innovation to the wider spaceflight industry.
The transition from the current air traffic system to the next generation air traffic system will require the introduction of new automated systems, including transferring some functions from air traffic controllers to on-board automation. This report describes a new design verification and validation (V&V) methodology for assessing aviation safety. The approach involves a detailed computer simulation of work practices that includes people interacting with flight-critical systems. The research is part of an effort to develop new modeling and verification methodologies that can assess the safety of flight-critical systems, system configurations, and operational concepts. The 2002 Ueberlingen mid-air collision was chosen for analysis and modeling because one of the main causes of the accident was one crew's response to a conflict between the instructions of the air traffic controller and the instructions of TCAS, an automated Traffic Alert and Collision Avoidance System on-board warning system. It thus furnishes an example of the problem of authority versus autonomy. It provides a starting point for exploring authority/autonomy conflict in the larger system of organization, tools, and practices in which the participants' moment-by-moment actions take place. We have developed a general air traffic system model (not a specific simulation of Überlingen events), called the Brahms Generalized Ueberlingen Model (Brahms-GUeM). Brahms is a multi-agent simulation system that models people, tools, facilities/vehicles, and geography to simulate the current air transportation system as a collection of distributed, interactive subsystems (e.g., airports, air-traffic control towers and personnel, aircraft, automated flight systems and air-traffic tools, instruments, crew). Brahms-GUeM can be configured in different ways, called scenarios, such that anomalous events that contributed to the Überlingen accident can be modeled as functioning according to requirements or in an anomalous condition, as occurred during the accident. Brahms-GUeM thus implicitly defines a class of scenarios, which include as an instance what occurred at Überlingen. Brahms-GUeM is a modeling framework enabling "what if" analysis of alternative work system configurations and thus facilitating design of alternative operations concepts. It enables subsequent adaption (reusing simulation components) for modeling and simulating NextGen scenarios. This project demonstrates that BRAHMS provides the capacity to model the complexity of air transportation systems, going beyond idealized and simple flights to include for example the interaction of pilots and ATCOs. The research shows clearly that verification and validation must include the entire work system, on the one hand to check that mechanisms exist to handle failures of communication and alerting subsystems and/or failures of people to notice, comprehend, or communicate problematic (unsafe) situations; but also to understand how people must use their own judgment in relating fallible systems like TCAS to other sources of information and thus to evaluate how the unreliability of automation affects system safety. The simulation shows in particular that distributed agents (people and automated systems) acting without knowledge of each others' actions can create a complex, dynamic system whose interactive behavior is unexpected and is changing too quickly to comprehend and control.
Future NASA missions will depend on radiation-hardened, power-efficient processing systems-on-a-chip (SOCs) that consist of a range of processor cores custom tailored for space applications. Aries Design Automation, LLC, has developed a processing SOC that is optimized for software-defined radio (SDR) uses. The innovation implements the Institute of Electrical and Electronics Engineers (IEEE) RazorII voltage management technique, a microarchitectural mechanism that allows processor cores to self-monitor, self-analyze, and selfheal after timing errors, regardless of their cause (e.g., radiation; chip aging; variations in the voltage, frequency, temperature, or manufacturing process). This highly automated SOC can also execute legacy PowerPC 750 binary code instruction set architecture (ISA), which is used in the flight-control computers of many previous NASA space missions. In developing this innovation, Aries Design Automation has made significant contributions to the fields of formal verification of complex pipelined microprocessors and Boolean satisfiability (SAT) and has developed highly efficient electronic design automation tools that hold promise for future developments.
In principle, formal methods offer many advantages for aerospace software development: they can help to achieve ultra-high reliability, and they can be used to provide evidence of the reliability claims which can then be subjected to external scrutiny. However, despite years of research and many advances in the underlying formalisms of specification, semantics, and logic, formal methods are not much used in practice. In our opinion this is related to three major shortcomings. First, the application of formal methods is still expensive because they are labor- and knowledge-intensive. Second, they are difficult to scale up to complex systems because they are based on deep mathematical insights about the behavior of the systems (t.e., they rely on the "heroic proof"). Third, the proofs can be difficult to interpret, and typically stand in isolation from the original code. In this paper, we describe a tool for formally demonstrating safety-relevant aspects of aerospace software, which largely circumvents these problems. We focus on safely properties because it has been observed that safety violations such as out-of-bounds memory accesses or use of uninitialized variables constitute the majority of the errors found in the aerospace domain. In our approach, safety means that the program will not violate a set of rules that can range for the simple memory access rules to high-level flight rules. These different safety properties are formalized as different safety policies in Hoare logic, which are then used by a verification condition generator along with the code and logical annotations in order to derive formal safety conditions; these are then proven using an automated theorem prover. Our certification system is currently integrated into a model-based code generation toolset that generates the annotations together with the code. However, this automated formal certification technology is not exclusively constrained to our code generator and could, in principle, also be integrated with other code generators such as RealTime Workshop or even applied to legacy code. Our approach circumvents the historical problems with formal methods by increasing the degree of automation on all levels. The restriction to safety policies (as opposed to arbitrary functional behavior) results in simpler proof problems that can generally be solved by fully automatic theorem proves. An automated linking mechanism between the safety conditions and the code provides some of the traceability mandated by process standards such as DO-178B. An automated explanation mechanism uses semantic markup added by the verification condition generator to produce natural-language explanations of the safety conditions and thus supports their interpretation in relation to the code. It shows an automatically generated certification browser that lets users inspect the (generated) code along with the safety conditions (including textual explanations), and uses hyperlinks to automate tracing between the two levels. Here, the explanations reflect the logical structure of the safety obligation but the mechanism can in principle be customized using different sets of domain concepts. The interface also provides some limited control over the certification process itself. Our long-term goal is a seamless integration of certification, code generation, and manual coding that results in a "certified pipeline" in which specifications are automatically transformed into executable code, together with the supporting artifacts necessary for achieving and demonstrating the high level of assurance needed in the aerospace domain.