Electronic Theses and Dissertations

Date of Award


Document Type


Degree Name

Ph.D. in Engineering Science


Computer and Information Science

First Advisor

Conrad Cunningham

Second Advisor

Tony Ammeter

Third Advisor

Yixin Chen

Relational Format



Software performance predictability is vital to a system design and unpredictable performance is a leading cause of software failure. The emphasis of this dissertation is on verification that component-based software performs as specified. Performance profiles (specifications) depend on functional specifications and are necessary for all components for modular verification. Modular verification process is scalable because it uses profiles as contracts and allows verification of a single component in isolation with the assumption that any underlying component would have already been verified or will be verified to meet its specifications independently. This dissertation presents an integration of performance specification (profiles) with functional specifications within a single language. It contains a mechanizable and modular proof system to verify the performance bounds of reusable software components built reusing other components. The proof system forms the basis for a prototype verification condition (VC) generator. Experimentation with the VC generator illustrates that software component performance can be formally specified and verified. This dissertation discusses only duration (timing) aspect of performance, but the results can be extended to include space constraints.


Emphasis: Computer Science



To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.