Title page for ETD etd-01115-201156

Document Type	thesis
Author Name	Wang, Xiaoning
Email Address	iamxiaoning at hotmail.com
URN	etd-01115-201156
Title	A Modular Model Checking Algorithm for Cyclic Feature Compositions
Degree	MS
Department	Computer Science
Advisors	Kathi Fisler, Advisor Dan Dougherty, Reader
Keywords	modular verification model checking assume-guarantee reasoning feature-oriented software development verification
Date of Presentation/Defense	2005-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