Assuring Correctness, Completeness, and Performance for Model-Based Fault Diagnosis Systems

The robotic scientific and commercial spacecraft industries are currently trending towards the development of onboard autonomous capabilities for responding quickly to dynamic environments and rapidly changing situations. Model-based fault diagnosis (MBFD) is an approach to estimating a spacecraft's health state by continuously verifying accurate behavior and diagnosing off-nominal behavior. Proper functioning of MBFD depends on 1) the quality of the diagnostic system model that is analyzed and compared to commands and onboard measurements to estimate a system's health state, and 2) the correct functionality of the diagnosis engine interrogating the model and comparing its analyses to observed system behavior. Our goal is to develop Verification and Validation (V&V) techniques for a MBFD system to provide the necessary confidence in its ability to estimate the health of on-board spacecraft components and systems accurately and precisely. Our effort is investigating two areas. First, we build on our previously-reported work in developing techniques for checking the correctness and completeness of MBFD systems. Second, we develop techniques for analyzing performance characteristics of MBFD systems (e.g., runtime, memory usage) to provide assurance that they will function within the resource-constrained environments found on spacecraft. This paper describes work we have done in both areas. For the first area, we describe our approach to developing formal definitions for a correct and complete fault diagnosis system, the application of those definitions to a systematic way of checking the correctness and completeness of a diagnostic model independently from the diagnosis engine, and the results of these checks. We also discuss the ways in which V&V techniques are related to our correctness and completeness checking techniques for a MBFD system development process. For the second area, we develop analytical expressions as functions of key parameters to estimate runtime/processing performance bounds. In parallel, we define various model structures (topologies) to enable parameterized testing to determine how specific parameters affect performance, providing a way to identify the significant contributors. These analyses lay the foundation for developing techniques and tests for evaluating false-positive and false-negative metrics, which are used to characterize MBFD diagnosis performance.