Integrating ensemble learning and Large Language Models for efficient formal verification of IP-based aerospace systems
Zhi Ma, Cheng Wen, Bin Yu, Jie Su · Information Fusion · 2025
IP-based software design aims to enhance productivity and system reliability by reusing complex software modules known as Intellectual Property (IP) components. In safety-critical software systems, ensuring the security and correctness of these components necessitates formal verification of each IP. Traditional formal verification involves collecting data from multiple member models of an IP, formalizing these as property specifications, and verifying the correctness of the implementation model against these specifications. This process is inherently complex and labor-intensive, resulting in low verification efficiency and limited adaptability to varying code structures. To address these challenges, this paper employs IP components from complex spacecraft-embedded systems as a case study to explore the application prospects of ensemble learning and Large Language Model (LLM) in real industrial scenarios. We propose an intelligent verification framework capable of automatically extracting property specifications from the knowledge models of IP components and dynamically adjusting verification methods based on the type of verification target. Experimental results demonstrate that the proposed framework achieves high accuracy and scalability in aerospace verification tasks. Compared to traditional manual verification, the new framework significantly reduces verification time and minimizes the risk of human errors. Furthermore, this study analyzes the challenges of deploying ensemble learning and LLMs in industrial environments and suggests directions for future improvements. • We propose an innovative verification framework that automatically extracts property specifications from the knowledge model of IP components and adjusts its approach based on verification objectives. • Our study is the first to apply this framework in the high-risk aerospace-embedded domain, providing insights into its specific challenges and requirements. • Compared to traditional manual verification, our framework reduces verification time and human error, highlighting the need for domain-specific terminology and better integration with formal verification tools.