Symbolic model checking of software product lines
Andreas Claßen, Patrick Heymans, Pierre‐Yves Schobbens, Axel Legay · 2011
We study the problem of model checking software product line (SPL) behaviours against temporal properties. This is more difficult than for single systems because an SPL with n features yields up to 2n individual systems to verify. As each individual verification suffers from state explosion, it is crucial to propose efficient formalisms and heuristics.