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.
Formal Verification for Mode Confusion in the Flight Deck Using Intent-Based Abstraction
Journal of Aerospace Information Systems ; 13 , 9 ; 343-356
2016-10-06
14 pages
Aufsatz (Zeitschrift)
Elektronische Ressource
Englisch
Intent-based Abstraction for Formal Verification of Flight Deck Mode Confusion (AIAA 2016-0129)
British Library Conference Proceedings | 2016
|