A prominent challenge in model checking lies in alleviating the state explosion problem of complicated systems. Compositional model checking is a mathematically founded technique for reasoning about complex systems by employing a modular approach. Software product lines are a development paradigm with the specific objective of constructing a family of interrelated software products. To aid the modular model checking of software artifacts in the same product line, Liu et al. put forth a new compositional model-checking algorithm for sequentially composed systems.

The first part of the paper consists of a motivating example that pertains to a pacemaker product line, as well as an overview of the basics of sequential composition and computation tree logic. The paper then examines in a mathematical manner the compositional model-checking algorithm, which is based on variation point obligations. It discusses in detail the soundness of the algorithm and the application to a pacemaker product line. The paper ends with a critical review of previous contributions in software product lines and compositional verification.

Developing a method to utilize prior model-checking results for determining the correctness of a new software product in the same product line is of great importance. Nevertheless, both the proposed algorithm and the correctness proof assume that readers have a strong background in mathematics. The intended audience of the paper is limited to advanced researchers.