Automated ITL Specification Generation from Industrial Aerospace Requirements
In the development and verification of safety-critical aerospace 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.
Wed 20 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
16:50 - 17:50 | Industry Session 3: AI-Assisted Requirements Engineering and Early-Stage AnalysisIndustry Day at 2F Conference Room Chair(s): Jeroen Keiren Eindhoven University of Technology, The Netherlands | ||
16:50 20mIndustry talk | Automated ITL Specification Generation from Industrial Aerospace Requirements Industry Day Zhi Ma Xidian University, Xiao Liang Xidian University, Cheng Wen Xidian University, Rui Chen Beijing Institute of Control Engineering; Beijing Sunwise Information Technology, Bin Gu Beijing Institute of Control Engineering, Shengchao Qin Xidian University, Cong Tian Xidian University, Mengfei Yang China Academy of Space Technology | ||
17:10 20mIndustry talk | Shift-Left Requirements Verification: Integrating LLMs and Formal Methods for Automotive Systems Industry Day Zi Pong Lim Nanyang Technological University, bozhi wu Singapore Management University, Yon Shin Teo Aumovio SE, Shang-Wei LIN Singapore Institute of Technology, Yi Li Nanyang Technological University | ||
17:30 20mIndustry talk | Pragmatic Uses of AI in Formal Methods–Based Railway Projects: Early Lessons and Perspectives Industry Day | ||