In: International Journal on Software Tools for Technology Transfer (STTT). . URL: http://dx.doi.org/10.1007/s10009-006-0004-z.
Abstract: 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 (stochastic and model checking analyzer for reliability and timing) SMART (Stochestic and model checking analyses for seliability and tunnig) to investigate a number of safety properties for the RSM. To mitigate the impact of state-space explosion, we built a highly discretized model 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 conceptual design of RSM. Our findings were forwarded to the design engineers, who undertook corrective action. Additionally, the results stress the efficiency attained by the new model checking algorithms implemented in SMART, and demonstrate their applicability to real-world systems. Attempts to verify RSM with similar NuSMV and SPIN models have failed due to excessive memory consumption.
Keywords: Formal verification; Model checkinga; Aviation safetya; Collision avoidance protocols.