Towards Probabilistic Formal Analysis of SATS-Simultaneously Moving Aircraft (SATS-SMA)

The objective of NASA’s Small Aircraft Transportation System (SATS) Concept of Operations (ConOps) is to facilitate high volume operation of advanced small aircraft operating in non-towered, non-radar airports. This system can provide improved and accessible air travel at a lower cost. Given the safety-critical nature of SATS, its analysis accuracy is extremely important. However, the commonly used analysis techniques, like pilot/computer simulation and traditional model checking, do not ascertain an error-free and complete verification of SATS due to the wide range of possibilities involved in SATS or the inability to capture the randomized and unpredictable aspects of the SATS ConOps environment in their models. Another limitation of these studies is that a limited speed range was used in the analysis. To overcome these limitations, we propose to formulate the SATS ConOps as a fully synchronous and probabilistic model, i.e., SATS-SMA, that supports simultaneously moving aircraft. The distinguishing features of our work include the preservation of safety of aircraft while providing a precise timing model, which is closer to reality compared to the previous hybrid analyses. Important insights related to the aircraft take-off and landing operations during the instrument meteorological conditions are also presented.