Compositional model checking of software product lines using variation point obligations

This paper introduces a technique for incremental and compositional model checking that allows efficient reuse of model-checking results associated with the features in a product line. As the use of product lines has increased, so has the need to verify the models used to construct the products in the product line. However, this effort is currently hampered by the difficulty of composing model-checking results for the features in a way that allows reuse for subsequent products. The contributions of this paper are to remove restrictions on how the features can be sequentially composed, to describe how to generate obligations such that all sequentially composed systems can be verified, and to show how to compositionally model check the product in the product line by reusing the variation-point obligations. The paper develops the technique and its implementation in the context of a medical-device product line.