Open Access iconOpen Access

ARTICLE

crossmark

Identifying Counterexamples Without Variability in Software Product Line Model Checking

Ling Ding1, Hongyan Wan2,*, Luokai Hu1, Yu Chen1

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: email

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

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


Cite This Article

L. Ding, H. Wan, L. Hu and Y. Chen, "Identifying counterexamples without variability in software product line model checking," Computers, Materials & Continua, vol. 75, no.2, pp. 2655–2670, 2023.



cc This work is licensed under a Creative Commons Attribution 4.0 International License , which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
  • 610

    View

  • 362

    Download

  • 0

    Like

Share Link