"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."
| Identifer | oai:union.ndltd.org:wpi.edu/oai:digitalcommons.wpi.edu:etd-theses-1947 |
| Date | 21 August 2003 |
| Creators | Roberts, Brian Glenn |
| Contributors | Kathi Fisler, Advisor, George T. Heineman, Reader, Michael A. Gennert, Department Head |
| Publisher | Digital WPI |
| Source Sets | Worcester Polytechnic Institute |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | Masters Theses (All Theses, All Years) |
Page generated in 0.0028 seconds