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. A number of operational properties of SATS, such as event ordering, have been analyzed and verified by different groups using model checking and I/O automata. 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 four small aircraft. This helps increase pilot safety for landing in these small airports. A class of Real-Time Logic, Linear Real-Time Logic (LRTL), and its associated tool sets have been 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.