As the flight deck has become highly automated, mode confusion between the pilot and the automation has emerged as an important issue for aviation safety. This paper presents a formal verification framework that can be used to efficiently detect a wide range of mode-confusion problems in the pilot–automation system and provide safety guarantees. To facilitate this, a novel formal modeling of the automation and pilot is proposed to efficiently verify the pilot–automation system. The automation of the aircraft is modeled as a deterministic hybrid system, and the pilot is modeled as an intent-based finite state machine. Due to the high dimension of the aircraft’s continuous states and the large number of flight-mode combinations, formal verification of the hybrid system is computationally formidable, leading to the state-space explosion problem. To tackle this problem, a computationally efficient abstraction method for the hybrid model is proposed using intent inference, from which an intent-based finite state machine for the automation is obtained. The intent-based finite state machines for the automation and pilot are synchronously composed to systematically and comprehensively verify the pilot–automation system using the NuSMV model-checking tool. The proposed framework is demonstrated with two real pilot–automation interaction incidents/accidents.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal Verification for Mode Confusion in the Flight Deck Using Intent-Based Abstraction


    Beteiligte:

    Erschienen in:

    Erscheinungsdatum :

    2016-10-06


    Format / Umfang :

    14 pages




    Medientyp :

    Aufsatz (Zeitschrift)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Intent-based Abstraction for Formal Verification of Flight Deck Mode Confusion

    Suraj Nandiganahalli, Jayaprakash / Lee, Sangjin / Hwang, Inseok | AIAA | 2016


    Intent-based Abstraction for Formal Verification of Flight Deck Mode Confusion (AIAA 2016-0129)

    Nandiganahalli, Jayaprakash Suraj / Lee, Sangjin / Hwang, Inseok | British Library Conference Proceedings | 2016


    Flight Deck Mode Confusion Detection using Intent-based Probabilistic Model Checking

    Suraj Nandiganahalli, Jayaprakash / Lee, Sangjin / Hwang, Inseok | AIAA | 2017


    Intent Inference-Based Flight-Deck Human-Automation Mode-Confusion Detection

    Lee, Sangjin / Hwang, Inseok / Leiden, Kenneth | AIAA | 2015


    Automation Intent Inference Using the GFHMM for Flight Deck Mode Confusion Detection

    Lyu, Hao / Nandiganahalli, Jayaprakash Suraj / Hwang, Inseok | AIAA | 2018