Modular detection of feature interactions through theorem proving: A case study

Feature-oriented programming is a way of designing a program around the fea-tures it performs, rather than the objects or files it manipulates. This should lead to an extensible and flexible “product-line ” architecture that allows custom systems to be assembled with particular features included or excluded as needed. Composing these features together modularly, while leading to flexibility in the feature-set of the finished product, can also lead to unexpected interactions that occur between features. Robert Hall presented a manual methodology for locating these inter-actions and has used it to search for feature interactions in email[Hal00]. Li et al. performed automatic verification of Hall’s system using model-checking verifica-tions tools[LKF02a, LKF02b]. Model-checking verification is state-based, and is not well-suited for verifying recursive data structures, an area where theorem-proving verification tools excel. In this thesis, we propose a methodology for using formal theorem-proving tools for modularly verifying feature-oriented systems. The methodology presented cap