高级检索

    机载系统软件需求的建模与分时组合验证方法

    Modeling and Compositional Verification by Time Period for Airborne System Software Requirements

    • 摘要: 机载系统在航空航天领域起着至关重要的作用,其突出的安全性使得软件需求的形式化验证成为一个非常重要的问题. 但是随着机载系统需求复杂度和设备数量的增加,其形式化验证中出现了状态空间爆炸的问题. 为了缓解该问题,提出了一种机载系统需求的建模与分时组合验证方法. 这种方法通过利用时间维度,将复杂的验证系统分解为相互独立的组件,实现了对各组件的独立验证,进而综合出整个系统的验证结果. 通过实际的案例研究,证明了该方法的可行性. 并通过评估说明该方法不但可以验证一些传统单体验证不能验证的系统,缓解状态空间爆炸,而且可以避免不考虑分时所造成的误报. 这一方法为机载系统的软件需求验证提供了一种新的技术途径,有助于提高验证的准确性和效率,确保机载系统的安全性.

       

      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.

       

    /

    返回文章
    返回