Modeling Product Lines with Kripke Structures and Modal Logic

Product lines are an established framework for software design. They are specified by special diagrams called feature models. For formal analysis, the latter are usually encoded by propositional theories with Boolean semantics. We discuss a major deficiency of this semantics, and show that it can be fixed by considering that a product is an instantiation process rather than its final result. We call intermediate states of this process partial …