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

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

Modeling and Verification for Automatic Flight System Mode Requirements Based on MTRDL

In the automatic flight process of civil aircraft, Automatic Flight Sytem mode transition is an important factor affecting safety.With the rapid growth of the function 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 between multiple flight modes necessary in the automatic flight process, but also in the complex data and control cross-linking relationships between mode transition process and the external environment.These cross-linking relationships also imply the safety properties of flight mode transition process, which increases the application difficulty of formal methods.In this paper, a domain specific modeling and verification framework is proposed: First, a modeling language MTRDL for Automatic Flight System mode transition requirements and a modeling method based on extended SysML language are proposed; Secondly, the safety requirement template based on MTRDL is proposed, which can be automatically transformed into formal safety properties; Finally, the effectiveness of the method in the requirement verification of Automatic Flight System mode transition is proved by a case study of a certain aircraft''s itemized requirements.