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.
|Commitee:||Krintz, Chandra, Su, Jianwen|
|School:||University of California, Santa Barbara|
|School Location:||United States -- California|
|Source:||DAI-B 70/03, Dissertation Abstracts International|
|Keywords:||Interface grammars, Model checking, Software, Software verification, Verification|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be