软件学报

作者：徐恒，黄志球，胡军，陶传奇，王金永，石帆

单位：徐恒，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21001611,黄志球，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21001602,胡军，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21001603,陶传奇，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21001604,王金永，徐州工程学院 信息工程学院, 江苏 徐州 22101805,石帆，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21001606

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

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

在民机自动飞行过程中, 自动飞行系统模式转换是影响安全的重要因素, 随着现代民机机载系统的功能与复杂度的快速增长, 在需求阶段对自动飞行系统模式转换的安全性分析和验证成为重要的挑战. 飞行模式转换的复杂性不仅体现在自动飞行过程中必需的多重飞行模式之间的交互关系, 还体现在模式转换与外部环境之间复杂的数据与控制交联关系, 这些交联关系同时隐含了飞行模式转换的安全性质, 这些特征提高了形式化方法的应用难度. 提出一种领域特定的建模验证框架: 首先, 提出面向自动飞行系统模式转换的领域需求建模语言MTRDL和基于该语言扩展于SysML上的建模方法; 其次, 提出基于安全需求模板的安全性质辅助规约方法; 最后, 通过对某机型的若干条目化需求的实例研究, 证明所提方法在自动飞行系统模式转换需求验证中的有效性.

来源：2024年第9期

《软件学报》期刊编辑部

查看软件学报杂志2024年第9期