With PQDT Open, you can read the full text of open access dissertations and theses free of charge.
About PQDT Open
Search
COMING SOON! PQDT Open is getting a new home!
ProQuest Open Access Dissertations & Theses will remain freely available as part of a new and enhanced search experience at www.proquest.com.
Questions? Please refer to this FAQ.
Applying model checking techniques directly to programs has shown extensive promise; however, two related problems hinder applicability of model checking to software on a wider scale. First, the state space explosion problem (i.e., an exponential increase in the search space by increasing number of variables and concurrent components) limits the scalability of model checking techniques and second, the environment generation problem (i.e., finding models for parts of software that are outside the scope of the model checker) limits the applicability of model checking to the domains where such environment models are available. I propose a semi-automated approach to attack the above mentioned problems. Specifically, I propose an interface specification language and require the users to write interface specifications for components of a program that are outside the scope of the current verification effort. My interface specification language allows a user to write an interface grammar for a component to specify the constraints on the ordering of calls made by the program to that component. This approach enables modeling of nested call structures that cannot be expressed by interfaces based on finite state machines. I built an interface compiler that takes the interface grammar for a component as input and generates a stub for that component. The stub generated from the interface grammar of a component is used to replace that component during state space exploration, either to assuage the state space explosion, or to provide an executable environment for the component that is being verified.
Advisor: | Bultan, Tevfik |
Commitee: | Krintz, Chandra, Su, Jianwen |
School: | University of California, Santa Barbara |
Department: | Computer Science |
School Location: | United States -- California |
Source: | DAI-B 70/03, Dissertation Abstracts International |
Source Type: | DISSERTATION |
Subjects: | Computer science |
Keywords: | Interface grammars, Model checking, Software, Software verification, Verification |
Publication Number: | 3350382 |
ISBN: | 978-1-109-08238-8 |