An approach to the verification of the Center-TRACON automation system

The Center-TRACON Automation System (CTAS) is a collection of planning and control software functions that generate landing schedules and advisories to assist air traffic controllers in handling traffic in the en-route and terminal areas. In this paper, we propose a formal safety analysis methodology to determine the correctness of CTAS with respect to safety. Four large classes of safety notions are identified for the CTAS problem: nominal, robust, structural and degraded. For nominal safety questions we seek conditions under which the system is guaranteed to be nominally safe.