Model‐Based Formal Verification of Mode Transition Logic in Safety‐Critical Avionics

Abstract

Flight mode transitions in automatic flight systems (AFS) is critical for linking pilot commands, automatic control logic, and aircraft behavior. Ensuring correctness is challenging due to complex interactions among modes and ambiguities in natural‐language requirements. This study aims to provide a systematic framework for modeling and formally verifying flight mode transition requirements. We propose FMSysML, a SysML‐based profile that captures the structural and behavioral semantics of flight modes and enforces static semantic consistency rules. An automated transformation pipeline converts FMSysML models into NuXMV for formal verification. Safety properties are derived in three categories: global mode transition logic based on the flight mode transition matrix, domain constraints extracted from modes, modules, and events, and operational properties anchored to attribute semantics. A case study on industrial‐scale AFS requirements demonstrates that the framework can automatically construct analyzable formal models and generate over 1100 properties, including more than 900 derived from the flight mode transition matrix. Due to state‐space explosion, a representative subset of 187 properties was verified using NuXMV. Verification successfully identified six latent requirement or modeling defects, highlighting issues such as under‐specified guard conditions. The proposed framework enables scalable, traceable, and practical formal verification of safety‐critical flight mode transitions, bridging the gap between informal requirements and formal analysis in complex avionics systems.