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

作者简介:

徐恒(1994-), 男, 博士生, CCF学生会员, 主要研究领域为系统安全性分析, 形式化方法. ;黄志球(1965-), 男, 博士, 教授, 博士生导师, CCF杰出会员, 主要研究领域为软件工程, 软件安全性, 形式化方法. ;胡军(1973-), 男, 博士, 副教授, CCF 专业会员, 主要研究领域为模型驱动的系统安全性分析, 软件验证. ;陶传奇(1984-), 男, 博士, 教授, 博士生导师, CCF高级会员, 主要研究领域为软件工程, 软件安全性, 形式化方法. ;王金永(1983-), 男, 博士, 讲师, CCF专业会员, 主要研究领域为形式化方法与应用, 安全人工智能. ;石帆(1995-), 男, 博士生, 主要研究领域为形式化方法, 强化学习.

通讯作者:

黄志球, E-mail: zqhuang@nuaa.edu.cn

中图分类号:

基金项目:

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


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

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    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 cross-linking 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.

    参考文献
    相似文献
    引证文献
引用本文

徐恒,黄志球,胡军,陶传奇,王金永,石帆.基于MTRDL的自动飞行系统模式需求建模与验证方法.软件学报,2024,35(9):4265-4286

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2023-09-11
  • 最后修改日期:2023-10-30
  • 录用日期:
  • 在线发布日期: 2024-01-05
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号