Hierarchical Nested Modeling and Verification Method for AFS Mode Transition Based on SysML

The Automatic Flight System (AFS) plays a crucial role in modern aviation, with flight mode transitions being key to managing different flight phases and control processes. However, its complex static structure and dynamic hierarchical modes pose challenges for system modeling and safety analysis. This paper proposes a hierarchical nested formal modeling and safety verification approach to address these challenges. First, a metamodel for AFS mode transitions is created. System Modeling Language (SysML) is then utilized with domain-specific extensions and customizations for modeling requirements-related models and elements. Secondly, a comprehensive system-level hierarchical nested model is established based on these requirements. Finally, the customized SysML model is translated into NuSMV for automated model verification. A case study on the approach and landing phase of an aircraft demonstrates the effectiveness of this approach, enhancing system development efficiency and safety.