{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/34253"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/34253","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Efficient, expressive, and effective runtime verification","abstract":"Runtime Verification is a quickly growing technique for providing many of the guarantees of formal verification, but in a manner that is scalable. It useful information available from actual runs of programs to make verification decisions, rather than the purely static information used in formal verification. One of the main facets of Runtime Verification is runtime monitoring, where safety properties are checked against the execution of a program during (or in some cases after) its run. Prior work on efficient monitoring focused primarily on finite state properties. Non-finite state techniques existed, but added orders of magnitude of runtime overhead on the monitored system. The vast majority of runtime monitoring has also been limited to the application domain, with violations of safety properties only found on the actual trace of a given program. This thesis describes research that demonstrates that various logical formalisms, including those more powerful than finite logics, can be efficiently monitored in multiple monitoring domains. The demonstrated monitoring domains run the gamut from the application level with the Java programming language, to monitoring traces \\emph{predicted} from a given run of a program, to hardware based monitors designed to ensure proper peripheral operation. The logical formalisms include multicategory finite state machines, extended regular expressions, past-time linear temporal logic with optimization for hardware based monitors, context-free grammars, linear temporal logic with both past and future operators, and string rewriting. This combination of domains and logical formalisms show that monitoring can be both expressive and efficient, regardless of the expressive power of the logical formalism, and that monitoring can be used not only for flat traces generated by software applications, but also in predictive traces and a hardware context.","abstract_html":"Runtime Verification is a quickly growing technique for providing many of the guarantees of formal verification, but in a manner that is scalable. It useful information available from actual runs of programs to make verification decisions, rather than the purely static information used in formal verification. One of the main facets of Runtime Verification is runtime monitoring, where safety properties are checked against the execution of a program during (or in some cases after) its run. Prior work on efficient monitoring focused primarily on finite state properties. Non-finite state techniques existed, but added orders of magnitude of runtime overhead on the monitored system. The vast majority of runtime monitoring has also been limited to the application domain, with violations of safety properties only found on the actual trace of a given program. This thesis describes research that demonstrates that various logical formalisms, including those more powerful than finite logics, can be efficiently monitored in multiple monitoring domains. The demonstrated monitoring domains run the gamut from the application level with the Java programming language, to monitoring traces \\emph{predicted} from a given run of a program, to hardware based monitors designed to ensure proper peripheral operation. The logical formalisms include multicategory finite state machines, extended regular expressions, past-time linear temporal logic with optimization for hardware based monitors, context-free grammars, linear temporal logic with both past and future operators, and string rewriting. This combination of domains and logical formalisms show that monitoring can be both expressive and efficient, regardless of the expressive power of the logical formalism, and that monitoring can be used not only for flat traces generated by software applications, but also in predictive traces and a hardware context.","abstract_has_math":false,"creators":["Meredith, Patrick"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Rosu, Grigore","Caccamo, Marco","Havelund, Klaus","Marinov, Darko"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2012,"date_issued":"2012-09-18T21:08:01Z","date_published":"2012-09-18T21:08:01Z","updated_at":"2026-07-22T22:25:30Z","subjects":["Runtime Verification","Software Engineering","Predictive Analysis","Runtime Monitoring","Runtime Monitoring Semantics"],"languages":["en"],"rights":["Copyright 2012 Patrick O'Neil Meredith"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/34253","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Rosu, Grigore","Caccamo, Marco","Havelund, Klaus","Marinov, Darko"]},{"key":"dc:creator","label":"Author","values":["Meredith, Patrick"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2012-09-18T21:08:01Z","2012-08"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Runtime Verification","Software Engineering","Predictive Analysis","Runtime Monitoring","Runtime Monitoring Semantics"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2012 Patrick O'Neil Meredith"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/34253"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Runtime Verification is a quickly growing technique for providing many of the guarantees of formal verification, but in a manner that is scalable. It useful information available from actual runs of programs to make verification decisions, rather than the purely static information used in formal verification. One of the main facets of Runtime Verification is runtime monitoring, where safety properties are checked against the execution of a program during (or in some cases after) its run. Prior work on efficient monitoring focused primarily on finite state properties. Non-finite state techniques existed, but added orders of magnitude of runtime overhead on the monitored system. The vast majority of runtime monitoring has also been limited to the application domain, with violations of safety properties only found on the actual trace of a given program. This thesis describes research that demonstrates that various logical formalisms, including those more powerful than finite logics, can be efficiently monitored in multiple monitoring domains. The demonstrated monitoring domains run the gamut from the application level with the Java programming language, to monitoring traces \\emph{predicted} from a given run of a program, to hardware based monitors designed to ensure proper peripheral operation. The logical formalisms include multicategory finite state machines, extended regular expressions, past-time linear temporal logic with optimization for hardware based monitors, context-free grammars, linear temporal logic with both past and future operators, and string rewriting. This combination of domains and logical formalisms show that monitoring can be both expressive and efficient, regardless of the expressive power of the logical formalism, and that monitoring can be used not only for flat traces generated by software applications, but also in predictive traces and a hardware context.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2012-07-06T19:27:41Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 meredith-2012-thesis.zip: 17462947 bytes, checksum: 391ee99f9ceaa518bff062d5508ec48b (MD5) Patrick_Meredith.pdf: 2193448 bytes, checksum: e50abee2f391532242484a9fdfe05e27 (MD5)","Made available in DSpace on 2012-09-18T21:08:01Z (GMT). No. of bitstreams: 3 Patrick_Meredith.pdf: 2183998 bytes, checksum: 87c6987b2d9d6570f22781245e52214c (MD5) license.txt: 4066 bytes, checksum: a67d5e1735b2dff3a0ed28ddbcfc1c9d (MD5) meredith-2012-thesis.zip: 17525709 bytes, checksum: 59ff89015ade44721401bd85cbc26e38 (MD5)"]},{"key":"dc:title","label":"Title","values":["Efficient, expressive, and effective runtime verification"]}]}],"canonical_facts":{"dc:contributor":["Rosu, Grigore","Caccamo, Marco","Havelund, Klaus","Marinov, Darko"],"dc:creator":["Meredith, Patrick"],"dc:date":["2012-09-18T21:08:01Z","2012-08"],"dc:description":["Runtime Verification is a quickly growing technique for providing many of the guarantees of formal verification, but in a manner that is scalable. It useful information available from actual runs of programs to make verification decisions, rather than the purely static information used in formal verification. One of the main facets of Runtime Verification is runtime monitoring, where safety properties are checked against the execution of a program during (or in some cases after) its run. Prior work on efficient monitoring focused primarily on finite state properties. Non-finite state techniques existed, but added orders of magnitude of runtime overhead on the monitored system. The vast majority of runtime monitoring has also been limited to the application domain, with violations of safety properties only found on the actual trace of a given program. This thesis describes research that demonstrates that various logical formalisms, including those more powerful than finite logics, can be efficiently monitored in multiple monitoring domains. The demonstrated monitoring domains run the gamut from the application level with the Java programming language, to monitoring traces \\emph{predicted} from a given run of a program, to hardware based monitors designed to ensure proper peripheral operation. The logical formalisms include multicategory finite state machines, extended regular expressions, past-time linear temporal logic with optimization for hardware based monitors, context-free grammars, linear temporal logic with both past and future operators, and string rewriting. This combination of domains and logical formalisms show that monitoring can be both expressive and efficient, regardless of the expressive power of the logical formalism, and that monitoring can be used not only for flat traces generated by software applications, but also in predictive traces and a hardware context.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2012-07-06T19:27:41Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 meredith-2012-thesis.zip: 17462947 bytes, checksum: 391ee99f9ceaa518bff062d5508ec48b (MD5) Patrick_Meredith.pdf: 2193448 bytes, checksum: e50abee2f391532242484a9fdfe05e27 (MD5)","Made available in DSpace on 2012-09-18T21:08:01Z (GMT). No. of bitstreams: 3 Patrick_Meredith.pdf: 2183998 bytes, checksum: 87c6987b2d9d6570f22781245e52214c (MD5) license.txt: 4066 bytes, checksum: a67d5e1735b2dff3a0ed28ddbcfc1c9d (MD5) meredith-2012-thesis.zip: 17525709 bytes, checksum: 59ff89015ade44721401bd85cbc26e38 (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/34253"],"dc:language":["en"],"dc:rights":["Copyright 2012 Patrick O'Neil Meredith"],"dc:subject":["Runtime Verification","Software Engineering","Predictive Analysis","Runtime Monitoring","Runtime Monitoring Semantics"],"dc:title":["Efficient, expressive, and effective runtime verification"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:30Z"}