Probabilistic Formal Verification of the SATS Concept of Operation

被引：4

作者：

Sardar, Muhammad Usama ^{[1
]}

Afaq, Nida ^{[1
]}

Hoque, Khaza Anuarul ^{[2
]}

Johnson, Taylor T. ^{[2
]}

Hasan, Osman ^{[1
]}

机构：

[1] Natl Univ Sci & Technol, Sch Elect Engn & Comp Sci, Islamabad, Pakistan

[2] Univ Texas Arlington, Dept Comp Sci & Engn CSE, Arlington, TX USA

来源：

NASA FORMAL METHODS, NFM 2016 | 2016年 / 9690卷

关键词：

Formal verification; Probabilistic analysis; Model checking; SATS; SATS Concept of Operations; Aircraft safety; Aircraft separation; Landing and departure operations;

D O I：

10.1007/978-3-319-40648-0_15

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The objective of NASA's Small Aircraft Transportation System (SATS) Concept of Operations (ConOps) is to facilitate High Volume Operation (HVO) of advanced small aircraft operating in non-towered 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 ConOps environment in their models. 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 improving throughput at the airport. Important insights related to take-off and landing operations during the Instrument Meteorological Conditions (IMC) are also presented.

引用

页码：191 / 205

页数：15