Explicit State Model Checking Effects on Learning-Based Testing

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.