原文传递
Hybrid Verification of an Air Traffic Operational Concept
| 题名： | Hybrid Verification of an Air Traffic Operational Concept |
| 作者： | Munoz, Cesar A. |
| 关键词： | rational；operation；hybrid；concept；traffic；cati；fica；icat；mathematical；synchro |
| 摘要： | A concept of operations for air traffic management consists of a set of flight rules and procedures aimed to keep aircraft safely separated. This paper reports on the formal verification of separation properties of the NASA's Small Aircraft Transportation System, Higher Volume Operations (SATS HVO) concept for non-towered, non-radar airports. Based on a geometric description of the SATS HVO air space, we derive analytical formulas to compute spacing requirements on nominal approaches. Then, we model the operational concept by a hybrid non-deterministic asynchronous state transition system. Using an explicit state exploration technique, we show that the spacing requirements are always satisfied on nominal approaches. All the mathematical development presented in this paper has been formally verified in the Prototype Verification System (PVS). Keywords. Formal verification, hybrid systems, air traffic management, theorem proving |
| 报告类型： | 科技报告 |
相关文献
- Model Systems Engineering Documents for Adaptive Signal Control Technology Systems. Guidance Document.
- DAG-TM Concept Element 11 CNS Performance Assessment ADS-B Performance in the TRACON
- Fact Sheets of CTAS and NASA Decision-Support Tools and Concepts
- DAG-TM Concept Element 11 CNS Performance Assessment--ADS-B Performance in the TRACON.
- Analysis of Operational Hazards and Safety Requirements for Traffic Aware Strategic Aircrew Requests (TASAR).
- Prototype Tool and Focus Group Evaluation for an Advanced Trajectory-Based Operations Concept
检索历史
应用推荐
