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.
","abstract_html":"<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>","abstract_has_math":false,"creators":["Yasmin, Nighat"],"institution":null,"degree_name":"Ph.D. in Engineering Science","degree_level":"Dissertation","degree_discipline":"Computer and Information Science","degree_department":null,"school":null,"contributors":["Conrad Cunningham","Tony Ammeter","Yixin Chen"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2015,"date_issued":"2015-01-01T08:00:00Z","date_published":"2015-01-01T08:00:00Z","updated_at":"2026-07-24T03:05:36Z","subjects":["Functionality Specification","Performance Prediction","Performance Specification","Proof Rules","Resolve","Verification Conditions","Computer Sciences"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://egrove.olemiss.edu/etd/456","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Conrad Cunningham","Tony Ammeter","Yixin Chen"]},{"key":"dc:creator","label":"Author","values":["Yasmin, Nighat"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.available","label":"Dc Date Available","values":["2019-06-27T07:00:00Z"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer and Information Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D. in Engineering Science"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Functionality Specification","Performance Prediction","Performance Specification","Proof Rules","Resolve","Verification Conditions","Computer Sciences"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://egrove.olemiss.edu/etd/456"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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.
"]},{"key":"dc:title","label":"Title","values":["Specification And Mechanical Verification Of Performance Profiles Of Software Components"]}]}],"canonical_facts":{"dc:contributor":["Conrad Cunningham","Tony Ammeter","Yixin Chen"],"dc:creator":["Yasmin, Nighat"],"dc:date.available":["2019-06-27T07:00:00Z"],"dc:description.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.
"],"dc:identifier":["https://egrove.olemiss.edu/etd/456"],"dc:subject":["Functionality Specification","Performance Prediction","Performance Specification","Proof Rules","Resolve","Verification Conditions","Computer Sciences"],"dc:title":["Specification And Mechanical Verification Of Performance Profiles Of Software Components"],"thesis:degree_discipline":["Computer and Information Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D. in Engineering Science"]},"updated_at":"2026-07-24T03:05:36Z"}