Formal analysis of parallel landing scenarios

The Airborne Information for Lateral Spacing (AILS) is a project being conducted at the NASA Langley Research Center. Its general objective is to reduce air traffic delays and increase airport efficiency by enabling approaches to closely spaced parallel runways under instrument meteorological conditions. In this paper, we apply formal techniques to study a critical component of the AILS concept which provides situational awareness to the crew of the aircraft involved on a closely parallel landing. In particular, we focus on the AILS alerting algorithm. This algorithm analyses aircraft states and makes time projections of possible collision scenarios. Based on these projections and risk criteria, the algorithm triggers a sequence of caution and warning alerts. To show that the algorithm satisfies its requirements, we define a mathematical model of collision trajectories. The alerting algorithm is analyzed in the context of the trajectory model to determine if the algorithm complies with its requirements for all possible states and collision trajectories