In Partial Fulfillment of the Requirements for the Degree of
Master of Science
Will defend her thesis
The Small Aircraft Transportation System (SATS) protocol plans to increase air transportation access to smaller communities and improve the transportation of people, services and goods by effective use of over 5,000 small public airports in the USA. The SATS protocol was developed at the NASA Langley Research Center; its safety concerns have been analyzed and verified by Langley Researchers and MIT’s Theory of Computation Group using model checking, and I/O automata respectively. However, both works ignore the timing constraints of the protocol and only consider the order of the events assuming that the pilot is responsible for providing appropriate delays and separation assurance among events. In this study, we consider the delays and the deadlines, which may help provide safety assertions for simultaneous landing and departure of unmanned small aircrafts in these small airports. To do so, a class of Real Time Logic, LRTL, and its associated tool set are utilized to formally verify and analyze the timing constraints of the protocol.