darmstadt.de

As software product lines are increasingly used for safety-critical systems, researchers have adapted formal verification techniques such as model checking and theorem proving to cope with compile-time variability. While the focus of the ongoing debate lies on the verification mechanisms itself, it becomes increasingly difficult for researchers to maintain an overview about the various accompany-ing modeling techniques. We survey existing approaches as a first step towards a unifying view on variability mechanisms in formal modeling techniques for product lines. We illustrate the approaches by means of a running example to illustrate their commonalities and differences. Categories and Subject Descriptor