Abstract/Details

Automating and evaluating assume -guarantee reasoning


2007 2007

Other formats: Order a copy

Abstract (summary)

Software systems are taking on an increasingly important role in society and are being used in critical applications where their failure could result in human casualties or substantial economic loss. Thus, it is important to validate software systems to ensure their quality. One technique for validating software systems is finite-state verification, in which a finite model of a system is analyzed to ensure that it satisfies a property that specifies a desired system behavior. Unfortunately, the cost of finite-state verification can be exponential in the size of the system being analyzed.

Compositional analysis is a "divide-and-conquer" approach to verification that aims to reduce the cost of verification. One proposed compositional technique is assume-guarantee reasoning. With this technique a system is decomposed into subsystems and these subsystems are analyzed individually. By composing the results of these analyses, it can be determined whether or not a system satisfies a property. Because each subsystem is smaller than the whole system, analyzing each subsystem individually may reduce the overall cost of verification. Often the behavior of a subsystem is dependent on the subsystems with which it interacts, and thus it is usually necessary to provide assumptions about the environment in which a subsystem executes. Because developing assumptions has been a difficult manual task, the evaluation of assume-guarantee reasoning has been limited.

In this thesis we present an algorithm that automatically learns assumptions. Using this algorithm, we undertook a study to determine if assume-guarantee reasoning provides an advantage over monolithic verification. Using two different verifiers, we considered all two-way decompositions for a set of systems and properties. By increasing the number of repeated tasks in these systems, we evaluated the decompositions as they were scaled. We found that in only a few cases can assume-guarantee reasoning verify properties on larger systems than monolithic verification can and in these cases the systems that can be analyzed are only a few sizes larger. Although these results are discouraging, they provide insight about research directions that should be pursued and highlight the importance of experimental evaluation.

Indexing (details)


Subject
Computer science
Classification
0984: Computer science
Identifier / keyword
Applied sciences, Assume-guarantee reasoning, Software verification
Title
Automating and evaluating assume -guarantee reasoning
Author
Cobleigh, Jamieson M.
Number of pages
167
Publication year
2007
Degree date
2007
School code
0118
Source
DAI-B 68/02, Dissertation Abstracts International
Place of publication
Ann Arbor
Country of publication
United States
Advisor
Clarke, Lori A.
University/institution
University of Massachusetts Amherst
University location
United States -- Massachusetts
Degree
Ph.D.
Source type
Dissertations & Theses
Language
English
Document type
Dissertation/Thesis
Dissertation/thesis number
3254895
ProQuest document ID
304847600
Copyright
Database copyright ProQuest LLC; ProQuest does not claim copyright in the individual underlying works.
Document URL
http://search.proquest.com/docview/304847600
Access the complete full text

You can get the full text of this document if it is part of your institution's ProQuest subscription.

Try one of the following:

  • Connect to ProQuest through your library network and search for the document from there.
  • Request the document from your library.
  • Go to the ProQuest login page and enter a ProQuest or My Research username / password.