Formal Analysis of Runway Safety Monitor

The Runway Safety Monitor (RSM) is a component of NASA's Runway Incursion Prevention System (RIPS) research, intended to be incorporated in the Integrated Display System (IDS), a suite of cockpit systems which NASA has been developing since 1993.

The goal of the Runway Safety Monitor is to detect runway incursions, defined by the FAA as

"any occurrence at an airport involving an aircraft, vehicle, person, or object on the ground, that creates a collision hazard or results in the loss of separation with an aircraft taking off, intending to take off, landing, or intending to land."

Since most air safety incidents occur on or near runways, the Runway Safety Monitor plays a key role in accident avoidance. RSM is not intended to prevent incursions, but to detect them and alert the pilots. Prevention is provided by other components of RIPS in the form of a number of IDS capabilities such as heads-up display, electronic moving map, cockpit display of traffic information, and taxi routing. Experimental studies conducted by Lockheed Martin show that incursion situations are less likely to occur when IDS technology is employed on aircraft.

RSM runs on a device installed in the cockpit and is activated prior to takeoff and landing procedures at airports. An independent copy of RSM runs on each aircraft. RSM monitors traffic in a zone surrounding the runway where the takeoff or landing is to take place. The zone is a 3D volume of space that runs up to 220 feet laterally from each edge of the runway, up to 400 feet of altitude above the runway, and 1.1 nautical miles from each runway end.

Using the model checker SMART we were able to analyze all possible scenarios in an abstract model of RSM and found situations of potential concern that happen with extremely low probability. These are almost impossible to expose during either testing procedures, which usually afford no more than a dozen test flights a day, or simulation sessions. The actual state space sizes of the order of 10^13 to 10^42 states, justifies the need for exhaustive analysis.

• Radu Siminiceanu and Gianfranco Ciardo, Formal Verification of the NASA Runway Safety Monitor, Proceedings of 4th Automated Verification of Critical Systems (AVoCS 2004), ENTCS 128(6), pages 179-194, 2004. BibTeX Reference .
• Sharon O. Beskenis, David F. Green, Paul V. Hyer, Edward J. Johnson, Integrated Display System for Low Visibility Landing and Surface Operations, NASA Langley CR 208446, 1998.
• David F. Green, Runway Safety Monitor Algorithm for Runway Incursion Detection and Alerting, NASA Langley CR 211416, 2002.
• J. Timmermann, Runway incursion prevention system, ADS-B and DGPS data link analysis, Dallas-Ft.Worth International Airport, NASA Langley CR 211242, 2001.

Note: The tag identifies links that are outside of the NASA domain.