Programs of a software product line can be synthesized by composing modules that implement features. Besides high-level domain constraints that govern the compatibility of features, there are also low-level implementation constraints: a feature module can reference elements that are defined in other feature modules. Safe composition is the guarantee that all programs in a product line are type safe: i.e., absent of references to undefined elements (such as classes, methods, and variables). We show how safe composition properties can be verified for AHEAD product lines using feature models and SAT solvers. Categories and Subject Descriptors D.2.2 [Design Tools and Techniques]: Modules and interfaces; D.2.4 [Software Program Verification]: Assertion checkers; Software Architectures]: Data abstraction, Languages. General Terms Design, Languages, Verification. Keywords compositional programming, product lines, SAT solvers, features.
Sahil Thaker, Don S. Batory, David Kitchin, Willia