Software safety analysis of a flight management system vertical navigation function - a status report

We have developed a formal, executable model of the requirements for portions of the vertical navigation (VNAV) function of a flight management system and have conducted a software safety analysis on the model. In particular, we have performed a functional hazard assessment in order to identify the potentially hazardous conditions associated with the VNAV function. We then conducted a fault tree analysis and a failure mode effects analysis in order to identify the general categories of errors that relate to safety. By comparing these general categories to the system architecture, we were able to develop a list of specific safety requirements for the VNAV function. We then used formal methods tools to verify that the VNAV model satisfied the safety requirements. We provide an overview of the safety analysis performed to date on the VNAV model, and compare and contrast these results to a similar analysis performed on the mode logic of a flight guidance system. Because the flight guidance system model was constructed entirely from Boolean logic it was easily analyzable with model checkers. The VNAV model involves continuous logic, (altitude and position values), and requires the use of theorem provers. The results of this analysis provide insight into the feasibility of integrating formal methods tools into the safety analysis process in a model based development environment.