Title page for ETD etd-0821103-122029

Document Type thesis

Author Name Roberts, Brian Glenn

Email Address flicken+ETD at alum.wpi.edu

URN etd-0821103-122029

Title Modular Detection of Feature Interactions Through Theorem Proving: A Case Study

Degree MS

Department Computer 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/Defense 2003-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

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

Document Type	thesis
Author Name	Roberts, Brian Glenn
Email Address	flicken+ETD at alum.wpi.edu
URN	etd-0821103-122029
Title	Modular Detection of Feature Interactions Through Theorem Proving: A Case Study
Degree	MS
Department	Computer 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/Defense	2003-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