Explicit State Model Checking Effects on Learning-Based Testing

Iram Jaffar ()
Additional contact information
Iram Jaffar: Computer Science Department, Quaid-i-Azam University, Islamabad, Pakistan

International Journal of Innovations in Science & Technology, 2024, vol. 6 Special Issue: 7, issue 7, 258-271

Abstract: Exploring the impact of integrating an explicit state model checker into the learning-based testing (LBT) framework presents an intriguing challenge. Traditionally, LBT has leveraged symbolic model checkers such as NuSMV and SAL, which use Binary Decision Diagrams (BDDs) to analyze multiple states concurrently. In contrast, explicit state model checkers evaluate one state at a time, a key distinction that suggests potential advantages for explicit state checking in the context of LBT. Thus, it is valuable to investigate how integrating an explicit state model checking algorithm might influence the performance of LBT. Model checkers explore the state space to verify conformance with user-defined correctness requirements, typically represented as Linear Temporal Logic (LTL) formulas. If a property violation is detected, it is presented as a counterexample. NuSMV and SAL employ different algorithms for generating and displaying counterexamples. This paper specifically examines the effect of SPIN-generated counterexamples on the LBT process. Evaluation metrics include Total LBT Iterations, First Bug Reporting Time (in milliseconds), Counterexample Length, Precision, and Efficiency, among others. Total Model Checking Time (in milliseconds) captures the cumulative time spent verifying the model over all iterations. SPIN consistently requires the least time for all specifications compared to other model checkers. As a result, experiments demonstrate that SPIN is more efficient when integrated with LBT, leading to faster convergence of the LBT hypothesis to the target System Under Test (SUT) in comparison to NuSMV and SAL.

Keywords: Software Testing; Explicit State Model Checking; Learning-Based Testing; Counterexamples (search for similar items in EconPapers)
Date: 2024
References: Add references at CitEc
Citations:

Downloads: (external link)
https://journal.50sea.com/index.php/IJIST/article/view/1100/1649 (application/pdf)
https://journal.50sea.com/index.php/IJIST/article/view/1100 (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:abq:ijist1:v:6:y:2024:i:7:p:258-271

Access Statistics for this article

International Journal of Innovations in Science & Technology is currently edited by Prof. Dr. Syed Amer Mahmood

More articles in International Journal of Innovations in Science & Technology from 50sea
Bibliographic data for series maintained by Iqra Nazeer ().