Title
Feature-Aware Verification
Abstract
A software product line is a set of software products that are distinguished in terms of features (i.e., end-user--visible units of behavior). 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. We explore how feature-aware verification can improve the automatic detection of feature interactions in software product lines. Feature-aware verification uses product-line verification techniques and supports the specification of feature properties along with the features in separate and composable units. It integrates the technique of variability encoding to verify a product line without generating and checking a possibly exponential number of feature combinations. We developed the tool suite SPLverifier for feature-aware verification, which is based on standard model-checking technology. We applied it to an e-mail system that incorporates domain knowledge of AT&T. We found that feature interactions can be detected automatically based on specifications that have only feature-local knowledge, and that variability encoding significantly improves the verification performance when proving the absence of interactions.
Year
Venue
Keywords
2011
CoRR
programming language,software engineering
Field
DocType
Volume
Functional verification,Intelligent verification,Computer science,Runtime verification,Theoretical computer science,Feature model,Software product line,Software construction,High-level verification,Software verification
Journal
abs/1110.0021
Citations 
PageRank 
References 
0
0.34
19
Authors
5
Name
Order
Citations
PageRank
Sven Apel13980184.13
Hendrik Speidel200.34
Philipp Wendler325114.51
Alexander von Rhein431611.35
Dirk Beyer51736100.85