Identifying Counterexamples Without Variability in Software Product Line Model Checking

Product detection based on state abstraction technologies in the software product line (SPL) is more complex when compared to a single system. This variability constitutes a new complexity, and the counterexample may be valid for some products but spurious for others. In this paper, we found that spurious products are primarily due to the failure states, which correspond to the spurious counterexamples. The violated products correspond to the real counterexamples. Hence, identifying counterexamples is a critical problem in detecting violated products. In our approach, we obtain the violated products through the genuine counterexamples, which have no failure state, to avoid the tedious computation of identifying spurious products dealt with by the existing algorithm. This can be executed in parallel to improve the efficiency further. Experimental results show that our approach performs well, varying with the growth of the system scale. By analyzing counterexamples in the abstract model, we observed that spurious products occur in the failure state. The approach helps in identifying whether a counterexample is spurious or genuine. The approach also helps to check whether a failure state exists in the counterexample. The performance evaluation shows that the proposed approach helps significantly in improving the efficiency of abstraction-based SPL model checking.