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