Maurice H. ter Beek & Erik P. de Vink
Towards Modular Verification of Software Product Lines with mCRL2

We introduce by means of an example a modular verification technique for
analyzing the behavior of software product lines using the mCRL2 toolset. Based
on feature-driven borders, we divide a behavioral model of a product line into
a set of separate components with interfaces and a driver process to coordinate
them. Abstracting from irrelevant components, we verify properties over a
smaller behavioral model, which not only simplifies the model checking task but
also makes the result amenable for reuse. This is a fundamental step forward
for the approach to scale up to industrial-size product lines.