Formal specification and verification of a coordination protocol for an automated air traffic control system
Formal specification and verification of a coordination protocol for an automated air traffic control system
复制标题
自动空中交通管制系统协调协议的正式规范和验证
DOI：
10.1016/j.scico.2014.04.002
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Kristin Yvonne Rozier
中科院分区：
文献类型：
--
作者：
Yang Zhao;Kristin Yvonne Rozier
飞机之间的安全间隔是空中交通管制的首要考虑因素。为了实现这一安全关键应用所需的保证级别，自动空域概念(AAC)提出了三个级别的冲突检测和解决方案。最近，提出了一个高级别的操作概念来定义AAC中各组件之间的合作。然而，拟议的协调议定书尚未得到正式研究。我们使用形式化验证技术来确保AAC设计在下一阶段生产之前不会留下潜在的灾难性设计缺陷。我们形式化高级操作概念，这是以前只用NuSMV和CadenceSMV的自然语言描述的，并通过检查我们从系统描述中派生的LTL和CTL的时序逻辑规范来执行模型验证。我们编写描述安全系统操作的LTL规范，并使用模型检查进行系统验证。我们使用规范调试来确保形式规范集和模型抽象集的正确性，以减少模型检查时间，并实现快速的设计时检查。我们分析了两个反例，揭示了运营概念中的意外紧急行为，这些行为引发了系统工程师为满足安全标准而进行的设计更改。我们的经验报告通过详细介绍包括所有型号和规格的完整的端到端设计时验证过程，说明了正式方法在实际安全关键系统开发中的应用。
Safe separation between aircraft is the primary consideration in air traffic control. To achieve the required level of assurance for this safety-critical application, the Automated Airspace Concept (AAC) proposes three levels of conflict detection and resolution. Recently, a high-level operational concept was proposed to define the cooperation between components in the AAC. However, the proposed coordination protocol has not been formally studied. We use formal verification techniques to ensure there are no potentially catastrophic design flaws remaining in the AAC design before the next stage of production.We formalize the high-level operational concept, which was previously described only in natural language, in both NuSMV and CadenceSMV, and performmodel validationby checking against temporal logic specifications in LTL and CTL that we derive from the system description. We write LTL specifications describing safe system operations and use model checking forsystem verification. We employspecification debuggingto ensure correctness of both sets of formal specifications andmodel abstractionto reduce model checking time and enable fast, design-time checking. We analyze two counterexamples revealing unexpected emergent behaviors in the operational concept that triggered design changes by system engineers to meet safety standards. Our experience report illuminates the application of formal methods in real safety-critical system development by detailing a complete end-to-end design-time verification process including all models and specifications.