Automating the Assembly of Aviation Safety Cases

Safety cases are among the state of the art in safety management mechanisms, providing an explicit way to reason about system and software safety. The intent is to provide convincing, valid, comprehensive assurance that a system is acceptably safe for a given application in a defined operating environment, by creating an argument structure that links claims about safety to a body of evidence. However, their construction is a largely manual, and therefore a time consuming, error prone, and expensive process. We present a methodology for automatically assembling safety cases which are auto-generated from the application of a formal method to software, with manually created safety cases derived from system safety analysis. Our approach emphasizes the heterogeneity of safety-relevant information, and we show how diverse content can be integrated into a single argument structure. To illustrate our methodology, we have applied it to the Swift Unmanned Aircraft System (UAS) being developed at the NASA Ames Research Center. We present an end-to-end fragment of the resulting interim safety case comprising an aircraft-level argument manually constructed from the safety analysis of the Swift UAS, which is automatically assembled with an auto-generated lower-level argument produced from a formal proof of correctness of the safety-relevant properties of the software autopilot.