Dissertation/Thesis Abstract

Interface grammars for modular software verification
by Hughes, Graham, Ph.D., University of California, Santa Barbara, 2009, 203; 3350382
Abstract (Summary)

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.

Indexing (document details)
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
Copyright © 2019 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy
ProQuest