Files in this item



application/pdfPatrick_Meredith.pdf (2MB)
(no description provided)PDF


Title:Efficient, expressive, and effective runtime verification
Author(s):Meredith, Patrick
Director of Research:Rosu, Grigore
Doctoral Committee Chair(s):Rosu, Grigore
Doctoral Committee Member(s):Caccamo, Marco; Havelund, Klaus; Marinov, Darko
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Runtime Verification
Software Engineering
Predictive Analysis
Runtime Monitoring
Runtime Monitoring Semantics
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.
Issue Date:2012-09-18
Rights Information:Copyright 2012 Patrick O'Neil Meredith
Date Available in IDEALS:2012-09-18
Date Deposited:2012-08

This item appears in the following Collection(s)

Item Statistics