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

TL;DR

This paper demonstrates an automated approach for analyzing and verifying aerospace software IP components by leveraging large language models and multiple verification techniques, enhancing efficiency and reliability.

Contribution

It introduces a novel automated process combining LLMs and verification methods for requirement analysis and formal verification of aerospace software IP components.

Findings

Successfully verified five real-world aerospace IP components.

Automated requirement extraction reduces manual effort and domain expertise.

The approach improves verification efficiency and accuracy.

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.