Timing Analysis of Small Aircraft Transportation System (SATS)

The Small Aircraft Transportation System (SATS) protocol, developed at NASA, aims to increase air transportation access for smaller communities and improve the transportation of people, services, and goods by a more effective use of over 5,000 small public airports in the United States. By using model checking and I/O automata, a number of different groups have verified many of the operational properties of SATS. However, none of the published work considers the timing constraints of the protocol, delegating instead to the pilot the responsibility for providing appropriate delays and separation assurance among events. In this paper, we formally specify the delays and the deadlines for the landing component of the protocol for simultaneous approaches of several small aircraft. This helps increase pilot safety for landing in these small airports. Linear Real-Time Logic (LRTL), a subclass of Real-Time Logic, and its associated toolset are utilized to analyze and formally verify the timing constraints of the landing component of SATS. In addition, an algorithm for debugging a subset of LRTL models is proposed.