Runtime Verification is a quickly growing technique for providingmany of the guarantees of formal verification, but in a manner that isscalable. It useful information available from actual runs of programs tomake verification decisions, rather than the purely static informationused in formal verification.One of the main facets of Runtime Verification is runtime monitoring, wheresafety properties are checked against the execution of a program during (or insome cases after) its run.Prior work on efficient monitoring focusedprimarily on finite state properties.Non-finite state techniques existed, butadded orders of magnitude of runtime overhead on the monitored system.Thevast majority of runtime monitoring has also been limited to the applicationdomain, with violations of safety properties only found on the actual trace ofa given program.This thesis describes research that demonstrates that various logicalformalisms, including those more powerful than finite logics, can beefficiently monitored in multiple monitoring domains.The demonstratedmonitoring domains run the gamut from the application level with the Javaprogramming language, to monitoring traces \emph{predicted} from a given run ofa program, to hardware based monitors designed to ensure proper peripheraloperation.The logical formalisms include multicategory finite state machines,extended regular expressions, past-time linear temporal logic with optimizationfor hardware based monitors, context-free grammars, linear temporal logic withboth past and future operators, and string rewriting.This combination ofdomains and logical formalisms show that monitoring can be both expressive andefficient, regardless of the expressive power of the logical formalism, andthat monitoring can be used not only for flat traces generated by softwareapplications, but also in predictive traces and a hardware context.
【 预 览 】
附件列表
Files
Size
Format
View
Efficient, expressive, and effective runtime verification
PDF
download
878987797
028-85220240
