基于MTRDL的自动飞行系统模式需求建模与验证方法  

Requirement Modeling and Verification for Automatic Flight System Modes Based on MTRDL

作　　者：徐恒 黄志球[1] 胡军[1] 陶传奇 王金永 石帆 XU Heng;HUANG Zhi-Qiu;HU Jun;TAO Chuan-Qi;WANG Jin-Yong;SHI Fan(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China;School of Information Engineering,Xuzhou University of Technology,Xuzhou 221018,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京210016 [2]徐州工程学院信息工程学院,江苏徐州221018

出　　处：《软件学报》2024年第9期4265-4286,共22页Journal of Software

基　　金：国家自然科学基金(U2241216);中央高校基本科研业务费专项资金(NT2022027,NJ2022027);河南省科技攻关项目(222102210048)。

摘　　要：在民机自动飞行过程中,自动飞行系统模式转换是影响安全的重要因素,随着现代民机机载系统的功能与复杂度的快速增长,在需求阶段对自动飞行系统模式转换的安全性分析和验证成为重要的挑战.飞行模式转换的复杂性不仅体现在自动飞行过程中必需的多重飞行模式之间的交互关系,还体现在模式转换与外部环境之间复杂的数据与控制交联关系,这些交联关系同时隐含了飞行模式转换的安全性质,这些特征提高了形式化方法的应用难度.提出一种领域特定的建模验证框架:首先,提出面向自动飞行系统模式转换的领域需求建模语言MTRDL和基于该语言扩展于SysML上的建模方法;其次,提出基于安全需求模板的安全性质辅助规约方法;最后,通过对某机型的若干条目化需求的实例研究,证明所提方法在自动飞行系统模式转换需求验证中的有效性.During the automatic flight of civil aircraft,the transition of automatic flight system modes is an important factor affecting safety.With the rapid growth of functions and complexity of modern civil aircraft airborne systems,the safety analysis and verification of automatic flight system mode transition in the requirement phase has become an important challenge.The complexity of flight mode transition is not only reflected in the interaction among multiple flight modes necessary during the automatic flight but also in the complex data and control cross-linking relationships between the mode transition process and the external environment.Additionally,these crosslinking relationships imply the safety properties of the flight mode transition process,which increases the application difficulty of formal methods.This study proposes a domain specific modeling and verification framework.First,a modeling language MTRDL for transition requirements of automatic flight system modes and a modeling method based on extended SysML language are put forward.Secondly,the safety property-assisted protocol method based on safety requirement templates is proposed.Finally,the effectiveness of the method in the requirement verification of automatic flight system mode transition is proven by a case study of a certain aircraft’s itemized requirements.

关 键 词：自动飞行系统模式 形式化方法 SysML建模 安全性质 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]