根据工业航空航天需求自动生成 LTL 规范

在安全关键型航空航天软件的开发和验证中，线性时序逻辑（LTL）已被广泛用于指定从需求导出的复杂系统属性。然而，工业实践中仍存在重大差距：将自然语言 (NL) 要求转化为正式的 LTL 属性是一个劳动密集型且容易出错的过程，需要航空航天控制工程和形式化方法方面的宝贵专业知识。虽然最近的 NL 到 LTL 工具（例如 NL2SPEC、NL2TL、NL2LTL）能够自动执行此过程的部分内容，但由于复杂的领域术语或隐式的时间和逻辑结构，它们经常无法处理工业环境中的实际需求文档。为了应对这些挑战，我们提出了 AeroReq2LTL，这是一个使用 大语言模型 (LLM) 自动生成满足航空航天要求的 LTL 属性的框架，具有两项关键的工业创新：(i) 将技术术语标准化为精确的原子命题的数据字典； (ii) 基于模板的需求语言，在翻译前使时间线索和逻辑关系变得明确。在真实的航空航天数据集上，AeroReq2LTL 在 LTL 生成中实现了 85% 的精度和 88% 的召回率，并且其输出可以直接由现有验证工具使用。