Specification And Mechanical Verification Of Performance Profiles Of Software Components

<p>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.</p>

Name thesis:degree_name

Ph.D. in Engineering Science

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer and Information Science

Year dc:date.available

2015

Author dc:creator

• Yasmin, Nighat

Contributors dc:contributor

• Conrad Cunningham
• Tony Ammeter
• Yixin Chen

• Functionality Specification
• Performance Prediction
• Performance Specification
• Proof Rules
• Resolve
• Verification Conditions
• Computer Sciences

Repository record dc:identifier

https://egrove.olemiss.edu/etd/456

OAI identifier oai:identifier

oai:egrove.olemiss.edu:etd-1455