Intent-based Abstraction for Formal Verification of Flight Deck Mode Confusion
Jayaprakash Suraj Nandiganahalli, Sangjin Lee, Inseok Hwang · 2016
ion of domain: To succinctly describe the aircraft’s motion for the purpose of mode confusion detection, the hybrid states X ×Q are mapped to the intent domain I. The flight intent of the automation I k ∈ I is defined based on the sign of the continuous state derivatives (i.e., ẋ , where is a small positive number to account for uncertainties) for each discrete flight mode qk. This is mathematically given by z : X ×Q→ I as: I k = z(xk, qk), I ∈ I (4) For example, if (ḣk > 0) ∧ (qk := V/S mode), then I k = climb, where ∧ is the logical and operator. Thus, the abstracted model for the hybrid system M is described in the intent domain I, which is much smaller compared to the original infinite-dimensional domain. Thus, the state space explosion problem is effectively addressed. Abstraction of transition: It should however be noted that in addition to the above abstraction of domain, the transition relations must also be abstracted to obtain an intent-based FSM. Such an abstracted intent-based FSM model M of the automation describes the evolution of flight intents of the automation, governed by the aircraft’s continuous states and the control inputs satisfying the guard condition as in Eq. (2), and can be verified using a discrete model-checker such as the NuSMV. The abstracted transitionion of transition: It should however be noted that in addition to the above abstraction of domain, the transition relations must also be abstracted to obtain an intent-based FSM. Such an abstracted intent-based FSM model M of the automation describes the evolution of flight intents of the automation, governed by the aircraft’s continuous states and the control inputs satisfying the guard condition as in Eq. (2), and can be verified using a discrete model-checker such as the NuSMV. The abstracted transition