Towards an incremental automata-based approach for software product-line model checking

Most model-checking algorithms are based on automata theory. For instance, determining whether or not a transition system satisfies a Linear Temporal Logic (LTL) formula requires computing strongly connected component of its transition graph. In Software Product-Line (SPL) engineering, the model checking problem is more complex due to the huge amount of software products that may compose the line. Indeed, one has to determine the exact subset of those products that do not satisfy an intended property. Efficient dedicated verification methods have been recently developed to answer this problem. However, most of them does not allow incremental verification. In this paper, we introduce an automata-based incremental approach for SPL model checking. Our method makes use of previous results to determine whether or not the addition of conservative features (i.e., features that do not remove behaviour from the system) preserves the satisfaction of properties expressed in LTL. We provide a detailed description of the approach and propose algorithms that implement it. We discuss how our method can be combined with SPL dedicated verification methods, viz. Featured Transition Systems. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification- Model checking General Terms Theory, Verification.