Date of Award
2015
Document Type
Dissertation
Degree Name
Ph.D. in Engineering Science
Department
Computer and Information Science
First Advisor
Conrad Cunningham
Second Advisor
Tony Ammeter
Third Advisor
Yixin Chen
Relational Format
dissertation/thesis
Abstract
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.
Recommended Citation
Yasmin, Nighat, "Specification And Mechanical Verification Of Performance Profiles Of Software Components" (2015). Electronic Theses and Dissertations. 456.
https://egrove.olemiss.edu/etd/456
Concentration/Emphasis
Emphasis: Computer Science