Scenario-specific inconsistency checking for requirement auto-modeling via LLMs and GCN

In software development, ensuring requirements consistency is critical, especially for time-dependent behaviors, where scenario-specific inconsistencies may emerge. Traditional manual modeling methods are labor-intensive and often overlook temporal complexities, making them unsuitable for complex and scalable systems. To address this, automated modeling techniques are needed to improve efficiency. However, existing automated methods lack the formal precision required for verifying inconsistencies using theorem provers like Z3 and CVC4. To resolve this, we propose a novel method named Requirement Auto-Modeling Inconsistency Checking with LLMs and GCN (RAMIC-LG), which integrates Large Language Models (LLMs) and Graph Convolutional Network (GCN). This method leverages LLMs to automatically extract use cases from requirement documents and convert them into semi-formal Clock Constraint Specification Language (CCSL) expressions. GCN is then used to analyze these constraints and detect inconsistencies, offering a more efficient and flexible alternative to traditional verification tools. Experimental results demonstrate that RAMIC-LG achieves 0.865 accuracy, 0.884 recall, 0.865 precision, 0.867 F1 score and 0.952 node coverage in detecting temporal inconsistencies, outperforming baseline approaches.