Abstract:
Airborne systems serve a pivotal function in the aerospace industry. Their exceptional safety requirements make the formal verification of software requirements a critical and pressing issue. However, with the ever-increasing complexity of airborne system requirements and the growing number of onboard devices, formal verification has encountered the serious challenge of state space explosion. To alleviate this problem, this paper proposes a novel approach for the modeling and compositional verification of airborne system requirements based on time partitioning. This approach utilizes the time dimension to decompose a complex verification system into mutually independent components, enabling the independent verification of each component and subsequently synthesizing the overall verification results of the entire system. The feasibility and practicality of the proposed method are demonstrated through a real-world case study. The evaluation further shows that the proposed method not only enables the verification of systems that are beyond the capability of traditional monolithic verification approaches and effectively alleviates state space explosion, but also avoids false alarms that may arise from neglecting time-based partitioning. This innovative method provides a new and promising technical path for the formal verification of software requirements in airborne systems, contributing to enhanced verification accuracy and efficiency, and ultimately ensuring the operational safety and reliability of airborne systems.