Formal Verification of the NASA Runway Safety Monitor

The Runway Safety Monitor (RSM) designed by Lockheed Martin is part of NASA's effort to reduce aviation accidents. We developed a Petri net model of the RSM protocol and used the model checking functions of our tool SMART to investigate behaviors that can be classified as missed alarm scenarios in RSM. To apply discrete-state techniques and mitigate the impact of the resulting state-space explosion phenomenon, our model uses a highly discretized view of the system obtained by partitioning the monitored runway zone into a grid of smaller volumes and by considering scenarios involving only two aircraft. The model also assumes that there are no communication failures, such as bad input from radar or lack of incoming data, thus it relies on a consistent view of reality by all participants. In spite of these simplifications, we were able to expose potential problems in the RSM conceptual design. Our findings were forwarded to the design engineers, who undertook corrective action. The results stress the high level of efficiency attained by the new model checking algorithms implemented in our tool SMART, and demonstrate their applicability to real-world systems. Attempts to verify RSM with NuSMV and SPIN have failed due to excessive memory consumption.