Towards Practical Requirement Analysis and Verification: A Case Study on Software IP Components in Aerospace Embedded Systems

TL;DR

This paper tackles the challenge of practically analyzing and verifying aerospace software IP components by combining LLM-driven translation of natural language requirements into Linear Temporal Logic ($LTL$) with a triple-verification strategy. It introduces a two-module framework: prompt-based LLMs to generate formal specifications and three verification techniques (model checking, static analysis, and runtime/symbolic execution) to assess implementation conformance, demonstrated on five CAST IP components. Results show successful safety verification across multiple IPs and substantial (though not complete) verification of functional properties, underscoring the value and limitations of a multi-tool, $LTL$-driven workflow for security-critical IP reuse. The approach offers a practical path toward automating requirement analysis and verification in aerospace embedded systems, reducing manual effort while highlighting areas for improvement in NL standardization, scalability, and IP integration.

Abstract

IP-based software design is a crucial research field that aims to improve efficiency and reliability by reusing complex software components known as intellectual property (IP) components. To ensure the reusability of these components, particularly in security-sensitive software systems, it is necessary to analyze the requirements and perform formal verification for each IP component. However, converting the requirements of IP components from natural language descriptions to temporal logic and subsequently conducting formal verification demands domain expertise and non-trivial manpower. This paper presents a case study on software IP components derived from aerospace embedded systems, with the objective of automating the requirement analysis and verification process. The study begins by employing Large Language Models to convert unstructured natural language into formal specifications. Subsequently, three distinct verification techniques are employed to ascertain whether the source code meets the extracted temporal logic properties. By doing so, five real-world IP components from the China Academy of Space Technology (CAST) have been successfully verified.

Figures (5)

• Figure 1: The workflow of our study
• Figure 2: A General Model for Aerospace Embedded Software IP
• Figure 3: Implementation of Software IP
• Figure 4: Prompt: Conversion of Implicit Requirement Descriptions into Explicit Forms
• Figure 5: Prompt: Translate Explicit Requirements into LTL Formulas