R.: Generating Variation-point Obligations for Compositional Model Checking of Software Product Lines

Software product lines are widely used due to their ad-vantageous reuse of shared features while still allowing op-tional and alternative features in the individual products. Especially for high-integrity product lines, we would like to use model checking to verify that key properties hold as each new product is built. However, this goal is currently hampered by the complexity of composing model-checking results for the features in a way that allows reuse for sub-sequent products. This paper presents an incremental and compositional model-checking technique that allows effi-cient reuse of model checking results associated with the features in a product line. It goes beyond related work in that it removes restrictions on how the features can be se-quentially composed. This flexibility is important because it means that many more real-world systems can be model-checked. We have implemented the technique, and demon-strate and evaluate it on a medical device product line.