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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

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


    Contributors:

    Published in:

    Publication date :

    2016-09-01




    Type of media :

    Conference paper , Article (Journal)


    Type of material :

    Electronic Resource


    Language :

    English




    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