Muhammad Usama Sardar, Nida Afaq and Khaza Anuarul Hoque
Abstract
The objective of NASA's Small Aircraft Transportation System (SATS) concept of operation is to facilitate high volume operations (HVO) of advanced small aircraft at non-towered and non-radar airports. Given the safety-critical nature of SATS, its analysis accuracy is extremely important. However, the commonly used analysis techniques, like simulation and traditional model checking, do not ascertain a 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 concept of operation's environment in their models. To overcome these limitations, we propose to use probabilistic model checking for the verification of SATS concept of operation. We used the synchronously parallel automata to model the SATS concept of operation while allowing simultaneous entry of two aircraft into the Self Controlled Area (SCA). This model is then utilized to formally verify safety properties of SATS at the time of both take-off and landing during the Instrument Meteorological Conditions (IMC). The distinguishing features of our work include the ability to analyze the collision risk in different zones of the airport in terms of probabilities of collision and the verification of increased throughput for a new model of SATS that supports simultaneously moving aircraft.
PRISM Model
Contact Information
|