Efficiently Verifying Mutually Exclusive Inconsistency of Requirements for Embedded Systems

Formal methods have demonstrated tremendous potential for verifying requirements consistency, particularly for safety-critical systems. In our previous research, we included environment characteristics in the scope of formal specification verification for embedded systems and proposed a requirement consistency verification method based on an environment model. However, we found that this method was not sufficiently efficient. To address this issue, this paper defines this environment model introduced inconsistency as mutually exclusive inconsistency, based on its representation characteristics, and proposes an efficient static verification approach for embedded systems. We reduce the consistency verification problem to the traversal of a graph. To support the proposed approach, we implement a requirement consistency verification tool, called Env-Consistency, and apply it to industrial cases. To illustrate the advantages of this approach, several sets of comparative experiments are designed, which demonstrates our approach is both effective and efficient.