SPLverifier: Model Checking of Software Product Lines

Overview





Uni Logo

Software Product Line Group

Software Systems Lab

Overview

SPLverifier is a tool chain for feature-aware verification of software product lines (SPL). A software product line is a set of software systems, and thus SPLverifier has to verify that all products (distinguished in terms of their features) fulfill their specifications. A feature is a unit of functionality of a software system that satisfies a requirement, represents a design decision, and provides a potential configuration option. Individual products of an SPL are assembled out of features from a common pool. Hence, SPLverifier has to make sure that the features of a product work properly together. Feature interactions —situations in which the combination of features leads to emergent and possibly critical behavior— are a major source of failures in software product lines.

Feature-aware verification with SPLverifier takes information on features and their combinations into account. It supports the specification of feature properties along with the features in separate and composable units. Using SPLverifier, we encode the verification problem (i.e., checking for critical feature interactions) such that we can apply off-the-shelf model-checking technology. Furthermore, SPLverifier uses the technique of variability encoding, which allows it to verify a product line without generating and checking a possibly exponential number of feature combinations.

SPLverifier supports the verification of product lines written in C and Java. The C version uses CBMC or CPAchecker for model checking. The Java version uses the model checker JavaPathfinder or its extension jpf-bdd. Before verification, the systems are prepared with FeatureHouse and the specifications are woven into the code with AutoFeature (C) or AspectJ (Java).

Both SPLverifier versions (C and Java) have been used to detect feature interactions in multiple case studies, including an e-mail-system model that incorporates the domain knowledge of AT&T.

This Web site contains information on feature-aware verification (specification language and variability encoding), the tool SPLverifier (executable), and case studies (code and setups to replicate our experiments). The source code of the tools is available on request.