2026-09-19T22:00:21Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/34253 2023-07-10 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Rosu, Grigore Rosu, Grigore Caccamo, Marco Havelund, Klaus Marinov, Darko Meredith, Patrick 2012-09-18T21:08:01Z 2012-09-18T21:08:01Z 2012-08 2012-09-18T21:08:01Z 2012-08 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) http://hdl.handle.net/2142/34253 en Copyright 2012 Patrick O'Neil Meredith Runtime Verification Software Engineering Predictive Analysis Runtime Monitoring Runtime Monitoring Semantics Efficient, expressive, and effective runtime verification Computer Science 1434 Computer Science 0112 University of Illinois at Urbana-Champaign Dissertation Ph.D. PHD:Computer Science -UIUC 10KS0112PHD