Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Criticality Safety”

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 1,009 records · Page 56

A Byzantine-Fault Tolerant Self-Stabilizing Protocol for Distributed Clock Synchronization Systems

Embedded distributed systems have become an integral part of safety-critical computing applications, necessitating system designs that incorporate fault tolerant clock synchronization in order to achieve ultra-reliable assurance levels. Many efficient clock synchronization protocols do not, however, address Byzantine failures, and most protocols that do tolerate Byzantine failures do not self-stabilize. Of the Byzantine self-stabilizing clock synchronization algorithms that exist in the literature, they are based on either unjustifiably strong assumptions about initial synchrony of the nodes or on the existence of a common pulse at the nodes. The Byzantine self-stabilizing clock synchronization protocol presented here does not rely on any assumptions about the initial state of the clocks. Furthermore, there is neither a central clock nor an externally generated pulse system. The proposed protocol converges deterministically, is scalable, and self-stabilizes in a short amount of time. The convergence time is linear with respect to the self-stabilization period. Proofs of the correctness of the protocol as well as the results of formal verification efforts are reported.

Malekpour, Mahyar R.↗

Sensor Data Qualification for Autonomous Operation of Space Systems

NASA's new Exploration initiative for both robotic and manned missions will require higher levels of reliability, autonomy and reconfiguration capability to make the missions safe, successful and affordable. Future systems will require diagnostic reasoning to assess the health of the system in order to maintain the system s functionality. The diagnostic reasoning and assessment will involve data qualification, fault detection, fault isolation and remediation control. A team of researchers at the NASA Glenn Research Center is currently working on a Sensor Data Qualification (SDQ) system that will support these critical evaluation processes, for both automated and human-in-the-loop applications. Data qualification is required as a first step so that critical safety and operational decisions are based on good data. The SDQ system would monitor a network of related sensors to determine the health of individual sensors within that network. Various diagnostic systems such as the Caution and Warning System would then use the sensor health information with confidence. The proposed SDQ technology will be demonstrated on a variety of subsystems that are relevant to NASA s Exploration systems, which currently include an electrical power system and a cryogenic fluid management system. The focus of this paper is the development and demonstration of a SDQ application for a prototype power distribution unit that is representative of a Crew Exploration Vehicle electrical power system; this provides a unique and relevant environment in which to demonstrate the feasibility of the SDQ technology.

Maul, William A.↗

NASA's Core Trajectory Sub-System Project: Using JBoss Enterprise Middleware for Building Software Systems Used to Support Spacecraft Trajectory Operations

NASA's Johnson Space Center (JSC) / Flight Design and Dynamics Division (DM) has prototyped the use of Open Source middleware technology for building its next generation spacecraft mission support system. This is part of a larger initiative to use open standards and open source software as building blocks for future mission and safety critical systems. JSC is hoping to leverage standardized enterprise architectures, such as Java EE, so that its internal software development efforts can be focused on the core aspects of their problem domain. This presentation will outline the design and implementation of the Trajectory system and the lessons learned during the exercise.

Stensrud, Kjell C.↗

The Dangers of Failure Masking in Fault-Tolerant Software: Aspects of a Recent In-Flight Upset Event

On 1 August 2005, a Boeing Company 777-200 aircraft, operating on an international passenger flight from Australia to Malaysia, was involved in a significant upset event while flying on autopilot. The Australian Transport Safety Bureau's investigation into the event discovered that an anomaly existed in the component software hierarchy that allowed inputs from a known faulty accelerometer to be processed by the air data inertial reference unit (ADIRU) and used by the primary flight computer, autopilot and other aircraft systems. This anomaly had existed in original ADIRU software, and had not been detected in the testing and certification process for the unit. This paper describes the software aspects of the incident in detail, and suggests possible implications concerning complex, safety-critical, fault-tolerant software.

Johnson, C. W.↗

Toward a Formal Evaluation of Refactorings

Refactoring is a software development strategy that characteristically alters the syntactic structure of a program without changing its external behavior [2]. In this talk we present a methodology for extracting formal models from programs in order to evaluate how incremental refactorings affect the verifiability of their structural specifications. We envision that this same technique may be applicable to other types of properties such as those that concern the design and maintenance of safety-critical systems.

Paul, John↗

The Role of Trust and Interaction in Global Positioning System Related Accidents

The Global Positioning System (GPS) uses a network of satellites to calculate the position of a receiver over time. This technology has revolutionized a wide range of safety-critical industries and leisure applications. These systems provide diverse benefits; supplementing the users existing navigation skills and reducing the uncertainty that often characterizes many route planning tasks. GPS applications can also help to reduce workload by automating tasks that would otherwise require finite cognitive and perceptual resources. However, the operation of these systems has been identified as a contributory factor in a range of recent accidents. Users often come to rely on GPS applications and, therefore, fail to notice when they develop faults or when errors occur in the other systems that use the data from these systems. Further accidents can stem from the over confidence that arises when users assume automated warnings will be issued when they stray from an intended route. Unless greater attention is paid to the role of trust and interaction in GPS applications then there is a danger that we will see an increasing number of these failures as positioning technologies become integral in the functioning of increasing numbers of applications.

Johnson, Chris W.↗

Ground Handling of Batteries at Test and Launch-site Facilities

Ground handling of flight as well as engineering batteries at test facilities and launch-site facilities is a safety critical process. Test equipment interfacing with the batteries should have the required controls to prevent a hazardous failure of the batteries. Test equipment failures should not induce catastrophic failures on the batteries. Transportation requirements for batteries should also be taken into consideration for safe transportation. This viewgraph presentation includes information on the safe handling of batteries for ground processing at test facilities as well as launch-site facilities.

Jeevarajan, Judith A.↗

Survey of Product-line Verification and Validation Techniques

This report presents the results from the first task of the SARP Center Initiative, 'Product Line Verification of Safety-Critical Software.' Task 1 is a literature survey of available techniques for product line verification and validation. Section 1 of the report provides an introduction to product lines and motivates the survey of verification techniques. It describes what is reused in product-line engineering and explains the goal of verifiable conformance of the developed system to its product-line specifications. Section 2 of the report describes six lifecycle steps in product-line verification and validation. This description is based on, and refers to, the best practices extracted from the readings. It ends with a list of verification challenges for NASA product lines (2.7) and verification enablers for NASA product lines (2.8) derived from the survey. Section 3 provides resource lists of related conferences, workshops, industrial and defense industry experiences and case studies of product lines, and academic/industrial consortiums. Section 4 is a bibliography of papers and tutorials with annotated entries for relevant papers not previously discussed in sections 2 or 3.

testing↗

A Test Generation Framework for Distributed Fault-Tolerant Algorithms

Heavyweight formal methods such as theorem proving have been successfully applied to the analysis of safety critical fault-tolerant systems. Typically, the models and proofs performed during such analysis do not inform the testing process of actual implementations. We propose a framework for generating test vectors from specifications written in the Prototype Verification System (PVS). The methodology uses a translator to produce a Java prototype from a PVS specification. Symbolic (Java) PathFinder is then employed to generate a collection of test cases. A small example is employed to illustrate how the framework can be used in practice.

Goodloe, Alwyn↗

Identifying Contingency Requirements using Obstacle Analysis on an Unpiloted Aerial Vehicle

This paper describes experience using Obstacle Analysis to identify contingency requirements on an unpiloted aerial vehicle. A contingency is an operational anomaly, and may or may not involve component failure. The challenges to this effort were: ( I ) rapid evolution of the system while operational, (2) incremental autonomy as capabilities were transferred from ground control to software control and (3) the eventual safety-criticality of such systems as they begin to fly over populated areas. The results reported here are preliminary but show that Obstacle Analysis helped (1) identify new contingencies that appeared as autonomy increased; (2) identify new alternatives for handling both previously known and new contingencies; and (3) investigate the continued validity of existing software requirements for contingency handling. Since many mobile, intelligent systems are built using a development process that poses the same challenges, the results appear to have applicability to other similar systems.

fault protection↗

Advanced Reference Counting Pointers for Better Performance

A computer program implements reference counting pointers (RCPs) that are lock-free, thread-safe, async-safe, and operational on a multiprocessor computer. RCPs are powerful and convenient means of managing heap memory in C++ software. Most prior RCP programs use locks to ensure thread safety and manage concurrency. The present program was developed in a continuing effort to explore ways of using the C++ programming language to develop safety-critical and mission- critical software. This effort includes exploration of lock-free algorithms because they offer potential to avoid some costly and difficult verification problems. Unlike previously published RCP software, the present program does not use locks (meaning that no thread can block progress on another thread): Instead, this program implements algorithms that exploit capabilities of central-processing- unit hardware so as to avoid locks. Once locks are eliminated, it becomes possible to realize the other attributes mentioned in the first sentence. In addition to the abovementioned attributes, this program offers several advantages over other RCP programs that use locks: It is smaller (and, hence, is faster and uses less memory), it is immune to priority inversion, and there is no way for it to cause a C++ exception.

Reinholtz, William↗

Probabilistic Structural Analysis Program

NASA/NESSUS 6.2c is a general-purpose, probabilistic analysis program that computes probability of failure and probabilistic sensitivity measures of engineered systems. Because NASA/NESSUS uses highly computationally efficient and accurate analysis techniques, probabilistic solutions can be obtained even for extremely large and complex models. Once the probabilistic response is quantified, the results can be used to support risk-informed decisions regarding reliability for safety-critical and one-of-a-kind systems, as well as for maintaining a level of quality while reducing manufacturing costs for larger-quantity products. NASA/NESSUS has been successfully applied to a diverse range of problems in aerospace, gas turbine engines, biomechanics, pipelines, defense, weaponry, and infrastructure. This program combines state-of-the-art probabilistic algorithms with general-purpose structural analysis and lifting methods to compute the probabilistic response and reliability of engineered structures. Uncertainties in load, material properties, geometry, boundary conditions, and initial conditions can be simulated. The structural analysis methods include non-linear finite-element methods, heat-transfer analysis, polymer/ceramic matrix composite analysis, monolithic (conventional metallic) materials life-prediction methodologies, boundary element methods, and user-written subroutines. Several probabilistic algorithms are available such as the advanced mean value method and the adaptive importance sampling method. NASA/NESSUS 6.2c is structured in a modular format with 15 elements.

Pai, Shantaram S.↗

A Verification-Driven Approach to Traceability and Documentation for Auto-Generated Mathematical Software

Model-based development and automated code generation are increasingly used for production code in safety-critical applications, but since code generators are typically not qualified, the generated code must still be fully tested, reviewed, and certified. This is particularly arduous for mathematical and control engineering software which requires reviewers to trace subtle details of textbook formulas and algorithms to the code, and to match requirements (e.g., physical units or coordinate frames) not represented explicitly in models or code. Both tasks are complicated by the often opaque nature of auto-generated code. We address these problems by developing a verification-driven approach to traceability and documentation. We apply the AUTOCERT verification system to identify and then verify mathematical concepts in the code, based on a mathematical domain theory, and then use these verified traceability links between concepts, code, and verification conditions to construct a natural language report that provides a high-level structured argument explaining why and how the code uses the assumptions and complies with the requirements. We have applied our approach to generate review documents for several sub-systems of NASA s Project Constellation.

Denney, Ewen W.↗

Machine-Checkable Timed CSP

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

Goethel, Thomas↗

Building a Formal Model of a Human-Interactive System: Insights into the Integration of Formal Methods and Human Factors Engineering

Both the human factors engineering (HFE) and formal methods communities are concerned with finding and eliminating problems with safety-critical systems. This work discusses a modeling effort that leveraged methods from both fields to use model checking with HFE practices to perform formal verification of a human-interactive system. Despite the use of a seemingly simple target system, a patient controlled analgesia pump, the initial model proved to be difficult for the model checker to verify in a reasonable amount of time. This resulted in a number of model revisions that affected the HFE architectural, representativeness, and understandability goals of the effort. If formal methods are to meet the needs of the HFE community, additional modeling tools and technological developments are necessary.

Bolton, Matthew L.↗

Applying Formal Methods to NASA Projects: Transition from Research to Practice

NASA project managers attempt to manage risk by relying on mature, well-understood process and technology when designing spacecraft. In the case of crewed systems, the margin for error is even tighter and leads to risk aversion. But as we look to future missions to the Moon and Mars, the complexity of the systems will increase as the spacecraft and crew work together with less reliance on Earth-based support. NASA will be forced to look for new ways to do business. Formal methods technologies can help NASA develop complex but cost effective spacecraft in many domains, including requirements and design, software development and inspection, and verification and validation of vehicle subsystems. To realize these gains, the technologies must be matured and field-tested so that they are proven when needed. During this discussion, current activities used to evaluate FM technologies for Orion spacecraft design will be reviewed. Also, suggestions will be made to demonstrate value to current designers, and mature the technology for eventual use in safety-critical NASA missions.

Othon, Bill↗

Monitoring Distributed Real-Time Systems: A Survey and Future Directions

Runtime monitors have been proposed as a means to increase the reliability of safety-critical systems. In particular, this report addresses runtime monitors for distributed hard real-time systems. This class of systems has had little attention from the monitoring community. The need for monitors is shown by discussing examples of avionic systems failure. We survey related work in the field of runtime monitoring. Several potential monitoring architectures for distributed real-time systems are presented along with a discussion of how they might be used to monitor properties of interest.

Goodloe, Alwyn E.↗