Results for “automated verification” — Page 8

NASA NTRSDate not supplied

NASA Delay Tolerant Networks: Operational, Evolving, an Ready for Expansion

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.

DTN↗

NASA NTRSDate not supplied

NASA Delay Tolerant Networks: Operational, Evolving, an Ready for Expansion

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.

DTN↗

NASA NTRS2013

Work Practice Simulation of Complex Human-Automation Systems in Safety Critical Situations: The Brahms Generalized berlingen Model

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.

complex systems↗

NASA NTRS2015

Reconfigurable Very Long Instruction Word (VLIW) Processor

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.

Velev, Miroslav N.↗

NASA NTRS2005

Formal Safety Certification of Aerospace Software

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.

Denney, Ewen↗

NASA NTRS2013

Verification and Validation Studies for the LAVA CFD Solver

The verification and validation of the Launch Ascent and Vehicle Aerodynamics (LAVA) computational fluid dynamics (CFD) solver is presented. A modern strategy for verification and validation is described incorporating verification tests, validation benchmarks, continuous integration and version control methods for automated testing in a collaborative development environment. The purpose of the approach is to integrate the verification and validation process into the development of the solver and improve productivity. This paper uses the Method of Manufactured Solutions (MMS) for the verification of 2D Euler equations, 3D Navier-Stokes equations as well as turbulence models. A method for systematic refinement of unstructured grids is also presented. Verification using inviscid vortex propagation and flow over a flat plate is highlighted. Simulation results using laminar and turbulent flow past a NACA 0012 airfoil and ONERA M6 wing are validated against experimental and numerical data.

Validation↗

NASA NTRS2004

Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software

We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then processed by an automated first-order theorem prover (ATP). For full automation, however, the obligations must be aggressively preprocessed and simplified We describe the unique requirements this places on the ATP and demonstrate how the individual simplification stages, which are implemented by rewriting, influence the ability of the ATP to solve the proof tasks. Experiments on more than 25,000 tasks were carried out using Vampire, Spass, and e-setheo.

Denney, Ewen↗

NASA NTRS2004

An Empirical Evaluation of Automated Theorem Provers in Software Certification

We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then processed by an automated first-order theorem prover (ATP). We discuss the unique requirements this application places on the ATPs, focusing on automation, proof checking, and usability. For full automation, however, the obligations must be aggressively preprocessed and simplified, and we demonstrate how the individual simplification stages, which are implemented by rewriting, influence the ability of the ATPs to solve the proof tasks. Our results are based on 13 certification experiments that lead to more than 25,000 proof tasks which have each been attempted by Vampire, Spass, e-setheo, and Otter. The proofs found by Otter have been proof-checked by IVY.

Denney, Ewen↗

NASA NTRS2017

Land surface Verification Toolkit (LVT)

LVT is a framework developed to provide an automated, consolidated environment for systematic land surface model evaluation Includes support for a range of in-situ, remote-sensing and other model and reanalysis products. Supports the analysis of outputs from various LIS subsystems, including LIS-DA, LIS-OPT, LIS-UE. Note: The Land Information System Verification Toolkit (LVT) is a NASA software tool designed to enable the evaluation, analysis and comparison of outputs generated by the Land Information System (LIS). The LVT software is released under the terms and conditions of the NASA Open Source Agreement (NOSA) Version 1.1 or later. Land Information System Verification Toolkit (LVT) NOSA.

surface model↗

DOE OSTI2025

Theorems in Service of Sound Composition, Rapid Modeling and Scalable Analysis

This project extends the state of the art in formal verification modeling with modules and automatically checkable data-sharing patterns such that component modules can retain their assurance case when composed within a larger system. For users, smaller models make reasoning easier and help to ensure they accurately reflect text specifications. For automated methods, smaller models give exponential benefits for verification algorithm execution time.

97 MATHEMATICS AND COMPUTING↗

NASA NTRS1989

A verification library for multibody simulation software

A multibody dynamics verification library, that maintains and manages test and validation data is proposed, based on RRC Robot arm and CASE backhoe validation and a comparitive study of DADS, DISCOS, and CONTOPS that are existing public domain and commercial multibody dynamic simulation programs. Using simple representative problems, simulation results from each program are cross checked, and the validation results are presented. Functionalities of the verification library are defined, in order to automate validation procedure.

Kim, Sung-Soo↗

NASA NTRS1992

The Automated Logistics Element Planning System (ALEPS)

ALEPS, which is being developed to provide the SSF program with a computer system to automate logistics resupply/return cargo load planning and verification, is presented. ALEPS will make it possible to simultaneously optimize both the resupply flight load plan and the return flight reload plan for any of the logistics carriers. In the verification mode ALEPS will support the carrier's flight readiness reviews and control proper execution of the approved plans. It will also support the SSF inventory management system by providing electronic block updates to the inventory database on the cargo arriving at or departing the station aboard a logistics carrier. A prototype drawer packing algorithm is described which is capable of generating solutions for 3D packing of cargo items into a logistics carrier storage accommodation. It is concluded that ALEPS will provide the capability to generate and modify optimized loading plans for the logistics elements fleet.

Schwaab, Douglas G.↗

NASA NTRS1994

The Stanford how things work project

We provide an overview of the Stanford How Things Work (HTW) project, an ongoing integrated collection of research activities in the Knowledge Systems Laboratory at Stanford University. The project is developing technology for representing knowledge about engineered devices in a form that enables the knowledge to be used in multiple systems for multiple reasoning tasks and reasoning methods that enable the represented knowledge to be effectively applied to the performance of the core engineering task of simulating and analyzing device behavior. The central new capabilities currently being developed in the project are automated assistance with model formulation and with verification that a design for an electro-mechanical device satisfies its functional specification.

Fikes, Richard↗

NASA NTRS2018

High Accuracy Coronagraph Flight Model For WFIRST–CGI Raw Contrast Sensitivity Analysis

A high-accuracy high-fidelity flight wavefront control (WFC) model is developed for detailed raw contrast sensitivity analysis of WFIRST-CGI. Built upon features of recently testbed validated model, it is further refined to combine a full Fresnel propagation diffraction model for high accuracy contrast truth evaluation, and an economical compact model for WFC purposes. Extensive individual raw contrast error sensitivities are evaluated systematically, both as known imperfections and as unknown calibration errors, for both spectroscopy mode and wide field-of-view mode with shaped pupil coronagraph. More than 90 distinct error items were identified, including system aberrations, optical misalignment, component manufacturing error, telescope interface related errors, etc. The result forms the basis for raw contrast error budget flow down to a sub-system level, where detailed specifications needed to aid in component design and manufacturing, mechanical alignment and instrument integration, and verification and validation operations. Evaluations are mostly automated, making it relatively easy for repeat runs of revised design or at new desired error quantity. Top error sensitivities and contrast floor contributors are discussed and several observations are noted.

Poberezhskiy, Ilya↗

NASA NTRS2022

Integrating FRET with Copilot: Automated Translation of Natural Language Requirements to Runtime Monitors

Runtime verification (RV) enables monitoring systems at runtime, to detect property violations early and limit their potential consequences. To provide the level of assurance required for ultra-critical systems, monitor specifications must faithfully reflect the original mission requirements, which are often written in ambiguous natural language. This paper presents an end-to-end framework to capture requirements in structured natural language and generate monitors that capture their semantics faithfully. We leverage NASA’s Formal Requirement Elicitation Tool (FRET), and the RV system Copilot. We extend FRET with mechanisms to capture additional information needed to generate monitors, and introduce OGMA, a new tool to bridge the gap between FRET and Copilot. With this framework, users can write requirements in an intuitive format and obtain real-time C monitors suitable for use in embedded systems. Our tool chain is available as open source.

FRET↗

NASA NTRSDate not supplied

Feature-Guided Analysis of Neural Networks

Applying standard software engineering practices to neural networks is challenging due to the lack of high-level abstractions describing a neural network’s behavior. To address this challenge, we propose to extract high-level task-specific features from the neural network internal representation, based on monitoring the neural network activations.The extracted feature representations can serve as a link to high-level requirements and can be leveraged to enable fundamental software engineering activities, such as automated testing, debugging, requirements analysis, and formal verification, leading to better engineering of neural networks. Using two case studies, we present initial empirical evidence demonstrating the feasibility of our ideas.

Features↗

NASA NTRS2004

Assume-Guarantee Verification of Source Code with Design-Level Assumptions

Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. To address the 'state explosion' problem associated with this technique, we propose to integrate assume-guarantee verification at different phases of system development. During design, developers build abstract behavioral models of the system components and use them to establish key properties of the system. To increase the scalability of model checking at this level, we have developed techniques that automatically decompose the verification task by generating component assumptions for the properties to hold. The design-level artifacts are subsequently used to guide the implementation of the system, but also to enable more efficient reasoning at the source code-level. In particular we propose to use design-level assumptions to similarly decompose the verification of the actual system implementation. We demonstrate our approach on a significant NASA application, where design-level models were used to identify; and correct a safety property violation, and design-level assumptions allowed us to check successfully that the property was presented by the implementation.

Giannakopoulou, Dimitra↗

NASA NTRS1993

Mission Operations and Command Assurance: Automating an Operations TQM Task

A long-term program is in progress at JPL to reduce cost and risk of mission operations through defect prevention and error management. A major element of this program, Mission Operations and Command Assurance (MO&QA), provides a system level function on flight projects to instill quality in mission operations. MO&CA embodies the Total Quality Management (TQM) principle of Continuous Process Inprovement (CPI) and uses CPI in applying automation to mission operations to reduce risk and costs. MO&CA has led efforts to apply and has implemented automation in areas that impact the daily flight project environment including Incident Surprise Anomoly tracking and reporting; command data verification, tracking, and reporting; and command support data usage. MO&CA's future work in automation will take into account that future missions systems must be designed to avoid increasing error through the introduction of automation, while adapting to the demands of smaller flight teams.

automation↗