Towards modular verification of software product lines with mCRL2

Abstract

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.