面向自然语言需求的验证性质生成方法

作者：李晓劼; 杨志斌; 王翰丰; 周勇; 李维

来源：小型微型计算机系统, 2022, 1-12.

• 形式化验证
• 模式定义语言
• 自然语言处理
• 规约生成

安全关键系统和软件的安全性、可靠性需要形式化验证来保障，使用形式化验证的前提是从自然语言需求文本中提取相关验证性质并将其转化为形式化规约，这已成为当前形式化验证领域研究的热点和难点。当前的形式化规约提取工作大多针对英文需求，较少针对中文自然语言需求。此外，由于AADL具有强大的表达能力和完善的验证机制，已成为航空航天领域的主要建模语言之一，而现有的工作较少考虑如何从需求中提取AADL模型的验证性质。为了解决上述问题，本文提出一种面向自然语言需求的AADL模型验证性质自动生成方法，从自然语言需求中提取验证的相关性质，并将其转化为AADL模型验证工具AGREE可识别的形式化规约。首先，定义了模式定义语言（Contract Pattern Language，CPL），将需求划分为不同模式，并给出由固定句型和占位符组成的需求模板；其次，通过自然语言处理技术解析需求文本，获取替换需求模板中占位符的原子命题，以便生成完整的形式化规约；最后，设计并实现了相关工具，并将其用于工业界实际案例来说明该方法的可用性和有效性。

• 单位
  航宇救生装备有限公司; 南京航空航天大学