Worcester Polytechnic Institute Electronic Theses and Dissertations Collection

Title page for ETD etd-0821103-122029


Document Typethesis
Author NameRoberts, Brian Glenn
Email Address flicken+ETD at alum.wpi.edu
URNetd-0821103-122029
TitleModular Detection of Feature Interactions Through Theorem Proving: A Case Study
DegreeMS
DepartmentComputer Science
Advisors
  • Prof. Kathi Fisler, Advisor
  • Prof. George T. Heineman, Reader
  • Prof. Michael Gennert, Department Head
  • Keywords
  • feature-oriented programming
  • software verification
  • modular verification
  • theorem proving
  • feature interaction
  • Date of Presentation/Defense2003-08-11
    Availability unrestricted

    Abstract

    Feature-oriented programming is a way of designing a program around the features 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 interactions and has used it to search for feature interactions in email. Li et al. performed automatic verification of Hall's system using model-checking verifications tools. 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 captures the essential steps for using modular techniques for modeling and verifying a system. This enables verification of individual modules, without examining the source code of the other modules in the system. We have used Hall's email system as a test case for validating the methodology.

    Files
  • roberts.pdf

  • Browse by Author | Browse by Department | Search all available ETDs

    [WPI] [Library] [Home] [Top]

    Questions? Email etd-questions@wpi.edu
    Maintained by webmaster@wpi.edu