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

Abstract

<p>Software product lines are widely used due to their advantageous reuse of shared features while still allowing optional 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 subsequent products. This paper presents an incremental and compositional model-checking technique that allows efficient 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 sequentially composed. This flexibility is important because it means that many more real-world systems can be model-checked. We have implemented the technique, and demonstrate and evaluate it on a medical device product line.</p>