Automated LTL Specification Generation from Industrial Aerospace Requirements

TL;DR

This paper introduces AeroReq2LTL, a framework using large language models to automate the translation of aerospace requirements into LTL, improving accuracy and usability in safety-critical software development.

Contribution

AeroReq2LTL employs a data dictionary and a template-based language to enhance LTL generation from complex aerospace requirements using LLMs.

Findings

Achieved 85% precision and 88% recall in LTL generation on real aerospace data.

Outputs are compatible with existing verification tools.

Addresses challenges of domain-specific terminology and implicit structure in industrial requirements.

Abstract

In the development and verification of safety-critical aero-space software, Linear Temporal Logic (LTL) has been widely used to specify complex system properties derived from requirements. However, a significant gap remains in industrial practice: translating natural language (NL) requirements into formal LTL properties is a labor-intensive and error-prone process that requires rare expertise in both aerospace control engineering and formal methods. While recent NL-to-LTL tools (e.g., NL2SPEC, NL2TL, NL2LTL) are capable of automating parts of this process, they often fail on real requirement documents in industrial settings, due to complex domain terminology or implicit temporal and logical structure. To address these challenges, we present AeroReq2LTL, a framework that automates LTL property generation for aerospace requirements using large language models (LLMs), with two key industrial innovations: (i) a data dictionary that normalizes technical jargon into precise atomic propositions; and (ii) a template-based requirement language that makes temporal cues and logical relations explicit before translation. On a real aerospace dataset, AeroReq2LTL achieves 85% precision and 88% recall in LTL generation, and its outputs can be directly consumed by existing verification tools.