Using model-based assurance to strengthen diagnostic procedures

In previous work we described Diagnostic Tree for Verification (DTV), a partially automated software engineering technique by which diagnostic trees generated from system models are used to help check out diagnostic procedures. Diagnostic procedures are instructions used to isolate failures during operations. Assuring such procedures manually is time-consuming and costly. This paper reports our recent experience in applying DTV to diagnostic procedures for lighting failures in NASA´s Habitat Demonstration Unit (HDU), a prototype for astronauts´ living quarters. DTV identified missing and inconsistent instructions, as well as more-efficient sequences of diagnostic steps. Unexpectedly, the most significant benefit was finding assumptions that will not remain true as the system evolves. We describe both the challenges faced in applying DTV and how its independent perspective helped in assuring the procedures´ adequacy and quality. Finally, the paper discusses more generally how software systems that are model-based, rapidly evolving and safety-critical appear most likely to benefit from this approach.