Abstract:Formal methods have made significant strides in the field of requirements consistency verification. However, as the complexity of embedded system requirements continues to increase, verifying requirements consistency faces the challenge of dealing with an excessively large state space. To effectively reduce the verification state space, while also considering the strong dependency among devices in embedded system requirements, this study proposes a compositional verification method for ensuring the consistency of requirements in complex embedded systems. This method is based on requirement decomposition and identification of dependencies among requirements. By leveraging these dependencies, it assembles verification subsystems, enabling the compositional verification of complex embedded system requirements and facilitating the initial identification of inconsistencies. Specifically, the problem frames approach is employed for requirement modeling and decomposition, while a domain-specific device knowledge base is utilized for modeling the physical characteristics of devices. During the assembly of verification subsystems, models of expected software behavior are generated and dynamically integrated with physical device models. Finally, the feasibility and effectiveness of this method are validated through a case study of an airborne reconnaissance control system, demonstrating a significant reduction in the verification state space through five case evaluations. This method thus provides a practical solution for verifying the requirements of complex embedded systems.