Worcester Polytechnic Institute Electronic Theses and Dissertations Collection

Title page for ETD etd-01115-201156


Document Typethesis
Author NameWang, Xiaoning
Email Address iamxiaoning at hotmail.com
URNetd-01115-201156
Title A Modular Model Checking Algorithm for Cyclic Feature Compositions
DegreeMS
DepartmentComputer Science
Advisors
  • Kathi Fisler, Advisor
  • Dan Dougherty, Reader
  • Keywords
  • modular verification
  • model checking
  • assume-guarantee reasoning
  • feature-oriented software development
  • verification
  • Date of Presentation/Defense2005-01-11
    Availability unrestricted

    Abstract

    Feature-oriented software architecture is a way of organizing code around the features that the program provides instead of the program's objects and components. In the development of a feature-oriented software system, the developers, supplied with a set of features, select and organize features to construct the desired system. This approach, by better aligning the implementation of a system with the external view of users, is believed to have many potential benefits such as feature reuse and easy maintenance. However, there are challenges in the formal verification of feature-oriented systems: first, the product may grow very large and complicated. As a result, it's intractable to apply the traditional formal verification techniques such as model checking on such systems directly; second, since the number of feature-oriented products the developers can build is exponential in the number of features available, there may be redundant verification work if doing verification on each product. For example, developers may have shared specifications on different products built from the same set of features and hence doing verification on these features many times is really unnecessary. All these drive the need for modular verifications for feature-oriented architectures.

    Assume-guarantee reasoning as a modular verification technique is believed to be an effective solution. In this thesis, I compare two verification methods of this category on feature-oriented systems and analyze the results. Based on their pros and cons, I propose a new modular model checking method to accomplish verification for sequential feature compositions with cyclic connections between the features. This method first builds an abstract finite state machine, which summarizes the information related to checking the property/specification from the concrete feature design, and then applies a revised CTL model checker to decide whether the system design can preserve the property or not. Proofs of the soundness of my method are also given in this thesis.

    Files
  • Thesis-01-12.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