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

Research output: Contribution in Book/Catalog/Report/Conference proceedingChapter

73 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationACM International Conference Proceeding Series
Number of pages8
Publication statusPublished - 1 Jan 2012


Dive into the research topics of 'Towards an incremental automata-based approach for software product-line model checking'. Together they form a unique fingerprint.

Cite this