Efficient, expressive, and effective runtime verification

Meredith, Patrick

Permalink

https://hdl.handle.net/2142/34253 Copy

Description

Title

Efficient, expressive, and effective runtime verification

Author(s)

Meredith, Patrick

Issue Date

2012-09-18T21:08:01Z

Director of Research (if dissertation) or Advisor (if thesis)

Rosu, Grigore

Doctoral Committee Chair(s)

Rosu, Grigore

Committee Member(s)

• Caccamo, Marco
• Havelund, Klaus
• Marinov, Darko

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(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.

Graduation Semester

2012-08

Permalink

http://hdl.handle.net/2142/34253

Copyright and License Information

Copyright 2012 Patrick O'Neil Meredith

Owning Collections