Formal verification of the NASA runway safety moni

Authors: Radu I Siminiceanu Gianfranco Ciardo

Publish Date: 2006/08/23

Volume: 9, Issue: 1, Pages: 63-76

PDF Link

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 statespace 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 realworld systems Attempts to verify RSM with similar NuSMV and SPIN models have failed due to excessive memory consumption

Keywords: