Open Access

ARTICLE

Identifying Counterexamples Without Variability in Software Product Line Model Checking

by Ling Ding¹, Hongyan Wan^2,*, Luokai Hu¹, Yu Chen¹

1 School of Computer Science, Hubei University of Education, Wuhan, 430205, China
2 School of Computer Science and Artificial Intelligence, Wuhan Textile University, Wuhan, 430200, China

* Corresponding Author: Hongyan Wan. Email:

Computers, Materials & Continua 2023, 75(2), 2655-2670. https://doi.org/10.32604/cmc.2023.035542

Received 25 August 2022; Accepted 14 December 2022; Issue published 31 March 2023

Abstract

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.

---

Keywords

---