面向限定自然语言需求的AADL自动生成工具

作者：刘承威; 杨志斌; 周勇; 袁胜浩; 许金淼; 薛垒

来源：小型微型计算机系统, 2019, 40(05): 984-995.

• 安全关键软件
• AADL
• 限定自然语言
• 组合验证

在航空、航天、交通、能源等安全关键领域中,软件的失效可能导致系统处于危险状态,从而导致财产损失、环境破坏甚至人员伤亡,如何保障这类软件的可靠性和安全性一直是学术界和工业界共同面临的难题.近年来,形式化模型驱动的安全关键软件设计与验证方法逐渐受到重视,并被认为是切实可行的重要手段.然而,形式化模型驱动开发方法的生命周期一般较少涉及需求阶段,主要原因是当前工业界的软件需求主要通过自然语言文本描述.而安全关键软件引起严重事故的问题链的最上端原因往往又是软件需求尤其是安全性需求的问题. AADL(Architecture Analysis&Design Language)是一种广泛应用于安全关键软件领域的建模语言标准.本文针对自然语言需求和AADL模型驱动开发方法之间还存在鸿沟的问题,研究基于限定自然语言的安全关键软件需求建模及AADL模型自动生成方法.首先,提出一种基于限定自然语言的需求规约方法,通过结构化的需求组织方式及受限的自然语言以减少需求表达中存在的二义性.其次,给出限定自然语言需求到AADL模型的自动转换方法.此外,本文给出一种结构化的验证性质描述模板,并自动转换到AADL组合验证附件AGREE(Assume Guarantee REasoning Environment) Annex,从而支持对AADL模型进行形式化验证.最后,在AADL开源工具环境OSATE中实现了原型工具,并基于航天导航制导控制子系统进行案例分析.

• 单位
  南京航空航天大学; 上海航天电子技术研究所