Search NASASearch

Engineering topics

Pai, Ganesh

Publications and source records attributed to Pai, Ganesh.

Towards a Rigorous Basis for Specific Operations Risk Assessment of UAS

The Specific Operations Risk Assessment (SORA) guidance represents the consensus of various national aviation authorities on a common process to identify, qualitatively assess, and manage the safety risk posed by unmanned aircraft systems (UAS), when preparing the safety case required for regulatory approval to conduct certain types of operations. As such, it can be considered a de facto standard, being increasingly adopted by various relevant stakeholders. This paper first gives an overview of the SORA process and associated methods, identifying a number of inconsistencies in risk identification and assessment, also discussing plausible strategies to close the associated gaps. Then, we give a well-founded basis for the applicable concepts, such as barrier integrity, assurance, and robustness, following which we present a preliminary and simple probabilistic formalization of the underpinning barrier-based safety model. We illustrate our overall approach through a worked example, also discussing how a Bayesian framework can facilitate extending and enhancing our initial formalization. We conclude with a discussion of the opportunities afforded by our approach, such as a well-founded basis for barrier selection, whilst addressing the associated challenges. The main objective of this work is to complement the current SORA guidance through a principled, mathematicallybased approach to risk assessment, particularly when it is applied to higher-risk operational concepts that warrant greater rigor in safety assessment and assurance.

Safety Cases

Technology and Tool Development to Support Safety and Mission Assurance

The Assurance Case approach is being adopted in a number of safety-mission-critical application domains in the U.S., e.g., medical devices, defense aviation, automotive systems, and, lately, civil aviation. This paradigm refocuses traditional, process-based approaches to assurance on demonstrating explicitly stated assurance goals, emphasizing the use of structured rationale, and concrete product-based evidence as the means for providing justified confidence that systems and software are fit for purpose in safely achieving mission objectives. NASA has also been embracing assurance cases through the concepts of Risk Informed Safety Cases (RISCs), as documented in the NASA System Safety Handbook, and Objective Hierarchies (OHs) as put forth by the Agency's Office of Safety and Mission Assurance (OSMA). This talk will give an overview of the work being performed by the SGT team located at NASA Ames Research Center, in developing technologies and tools to engineer and apply assurance cases in customer projects pertaining to aviation safety. We elaborate how our Assurance Case Automation Toolset (AdvoCATE) has not only extended the state-of-the-art in assurance case research, but also demonstrated its practical utility. We have successfully developed safety assurance cases for a number of Unmanned Aircraft Systems (UAS) operations, which underwent, and passed, scrutiny both by the aviation regulator, i.e., the FAA, as well as the applicable NASA boards for airworthiness and flight safety, flight readiness, and mission readiness. We discuss our efforts in expanding AdvoCATE capabilities to support RISCs and OHs under a project recently funded by OSMA under its Software Assurance Research Program. Finally, we speculate on the applicability of our innovations beyond aviation safety to such endeavors as robotic, and human spaceflight.

Mission Assuranc

Model-Driven Development of Safety Architectures

We describe the use of model-driven development for safety assurance of a pioneering NASA flight operation involving a fleet of small unmanned aircraft systems (sUAS) flying beyond visual line of sight. The central idea is to develop a safety architecture that provides the basis for risk assessment and visualization within a safety case, the formal justification of acceptable safety required by the aviation regulatory authority. A safety architecture is composed from a collection of bow tie diagrams (BTDs), a practical approach to manage safety risk by linking the identified hazards to the appropriate mitigation measures. The safety justification for a given unmanned aircraft system (UAS) operation can have many related BTDs. In practice, however, each BTD is independently developed, which poses challenges with respect to incremental development, maintaining consistency across different safety artifacts when changes occur, and in extracting and presenting stakeholder specific information relevant for decision making. We show how a safety architecture reconciles the various BTDs of a system, and, collectively, provide an overarching picture of system safety, by considering them as views of a unified model. We also show how it enables model-driven development of BTDs, replete with validations, transformations, and a range of views. Our approach, which we have implemented in our toolset, AdvoCATE, is illustrated with a running example drawn from a real UAS safety case. The models and some of the innovations described here were instrumental in successfully obtaining regulatory flight approval.

Safety case

Towards a Formal Basis for Modular Safety Cases

Safety assurance using argument-based safety cases is an accepted best-practice in many safety-critical sectors. Goal Structuring Notation (GSN), which is widely used for presenting safety arguments graphically, provides a notion of modular arguments to support the goal of incremental certification. Despite the efforts at standardization, GSN remains an informal notation whereas the GSN standard contains appreciable ambiguity especially concerning modular extensions. This, in turn, presents challenges when developing tools and methods to intelligently manipulate modular GSN arguments. This paper develops the elements of a theory of modular safety cases, leveraging our previous work on formalizing GSN arguments. Using example argument structures we highlight some ambiguities arising through the existing guidance, present the intuition underlying the theory, clarify syntax, and address modular arguments, contracts, well-formedness and well-scopedness of modules. Based on this theory, we have a preliminary implementation of modular arguments in our toolset, AdvoCATE.

Safety

Argument-Based Airworthiness Assurance of Small UAS

Presently, there are three avenues by which Unmanned Aircraft System (UAS) operations are authorized in the U.S. National Airspace System (NAS): obtaining either (i) a certificate of authorization (COA), or (ii) a special airworthiness certificate (SAC) in either the experimental, or the restricted category, or (iii) an exemption from an airworthiness certificate together with a civil COA. The first is meant primarily for public entities, such as NASA; the remaining two are the only available means for civil UAS operations. Recently, the Federal Aviation Administration (FAA) has also proposed a regulatory framework targeted for certain small UAS, specifically those weighing 55 pounds or less, although final rulemaking remains pending. We have previously shown how an assurance case can aggregate heterogeneous reasoning and safety evidence, with application to UAS safety. In this paper, we describe how assurance cases can serve as a common framework to justify overall system safety, unifying both operational aspects and airworthiness, in particular system design assurance. We also show how this approach can coexist with, and augment, existing safety analysis processes and best-practices, by transforming the artifacts they produce into structured assurance arguments. To illustrate the applicability and utility of our approach, we have been applying it for the design assurance of an unmanned rotorcraft system, intended for precision agriculture operations, as part of the NASA Unmanned Aircraft System (UAS) Integration in the National Airspace System (NAS) project.

Rotocraft

Dynamic Safety Cases for Through-Life Safety Assurance

We describe dynamic safety cases, a novel operationalization of the concept of through-life safety assurance, whose goal is to enable proactive safety management. Using an example from the aviation systems domain, we motivate our approach, its underlying principles, and a lifecycle. We then identify the key elements required to move towards a formalization of the associated framework.

Dynamic Safety Case

Formal Foundations for Hierarchical Safety Cases

Safety cases are increasingly being required in many safety-critical domains to assure, using structured argumentation and evidence, that a system is acceptably safe. However, comprehensive system-wide safety arguments present appreciable challenges to develop, understand, evaluate, and manage, partly due to the volume of information that they aggregate, such as the results of hazard analysis, requirements analysis, testing, formal verification, and other engineering activities. Previously, we have proposed hierarchical safety cases, hicases, to aid the comprehension of safety case argument structures. In this paper, we build on a formal notion of safety case to formalise the use of hierarchy as a structuring technique, and show that hicases satisfy several desirable properties. Our aim is to provide a formal, theoretical foundation for safety cases. In particular, we believe that tools for high assurance systems should be granted similar assurance to the systems to which they are applied. To this end, we formally specify and prove the correctness of key operations for constructing and managing hicases, which gives the specification for implementing hicases in AdvoCATE, our toolset for safety case automation. We motivate and explain the theory with the help of a simple running example, extracted from a real safety case and developed using AdvoCATE.

Hierarchy

Querying Safety Cases

Querying a safety case to show how the various stakeholders' concerns about system safety are addressed has been put forth as one of the benefits of argument-based assurance (in a recent study by the Health Foundation, UK, which reviewed the use of safety cases in safety-critical industries). However, neither the literature nor current practice offer much guidance on querying mechanisms appropriate for, or available within, a safety case paradigm. This paper presents a preliminary approach that uses a formal basis for querying safety cases, specifically Goal Structuring Notation (GSN) argument structures. Our approach semantically enriches GSN arguments with domain-specific metadata that the query language leverages, along with its inherent structure, to produce views. We have implemented the approach in our toolset AdvoCATE, and illustrate it by application to a fragment of the safety argument for an Unmanned Aircraft System (UAS) being developed at NASA Ames. We also discuss the potential practical utility of our query mechanism within the context of the existing framework for UAS safety assurance.

Safety Case

Preliminary Recommendations for the Collection, Storage, and Analysis of UAS Safety Data

Although the use of UASs in military and public service operations is proliferating, civilian use of UASs remains limited in the United States today. With efforts underway to accommodate and integrate UASs into the NAS, a proactive understanding of safety issues, i.e., the unique hazards and the corresponding risks that UASs pose not only through their operations for commercial purposes, but also to existing operations in the NAS, is especially important so as to (a) support the development of a sound regulatory basis, (b) regulate, design and properly equip UASs, and (c) effectively mitigate the risks posed. Data, especially about system and component failures, incidents, and accidents, provides valuable insight into how performance and operational capabilities/limitations contribute to hazards. Since the majority of UAS operations today take place in a context that is significantly different from the norm in civil aviation, i.e., with different operational goals and standards, identifying that which constitutes useful and sufficient data on UASs and their operations is a substantial research challenge.

Safety Data

Evidence Arguments for Using Formal Methods in Software Certification

We describe a generic approach for automatically integrating the output generated from a formal method/tool into a software safety assurance case, as an evidence argument, by (a) encoding the underlying reasoning as a safety case pattern, and (b) instantiating it using the data produced from the method/tool. We believe this approach not only improves the trustworthiness of the evidence generated from a formal method/tool, by explicitly presenting the reasoning and mechanisms underlying its genesis, but also provides a way to gauge the suitability of the evidence in the context of the wider assurance case. We illustrate our work by application to a real example-an unmanned aircraft system- where we invoke a formal code analysis tool from its autopilot software safety case, automatically transform the verification output into an evidence argument, and then integrate it into the former.

Argumentation

A Formal Basis for Safety Case Patterns

By capturing common structures of successful arguments, safety case patterns provide an approach for reusing strategies for reasoning about safety. In the current state of the practice, patterns exist as descriptive specifications with informal semantics, which not only offer little opportunity for more sophisticated usage such as automated instantiation, composition and manipulation, but also impede standardization efforts and tool interoperability. To address these concerns, this paper gives (i) a formal definition for safety case patterns, clarifying both restrictions on the usage of multiplicity and well-founded recursion in structural abstraction, (ii) formal semantics to patterns, and (iii) a generic data model and algorithm for pattern instantiation. We illustrate our contributions by application to a new pattern, the requirements breakdown pattern, which builds upon our previous work

Formal Methods