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 products, and argue that what a feature model M really defines is a poset of partial products called a partial product line, PPL(M). We argue that such PPLs can be viewed as special partial product Kripke structures (ppKS) specifiable by a suitable version of CTL (partial product CTL or ppCTL). We show that any feature model M is representable by a ppCTL theory $$\varPhi (M)$$ such that for any ppKs K, $$K\models \varPhi (M)$$ iff $$K = PPL (M)$$; hence, $$\varPhi (M)$$ is a sound and complete representation of the feature model.