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

摘要

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.