Efficient Parametric Runtime Verification with Deterministic String Rewriting

From FSL
Jump to: navigation, search

ASE'13, to appear (currently, non-final version)

Efficient Parametric Runtime Verification with Deterministic String Rewriting
Patrick Meredith and Grigore Rosu
ASE'13, IEEE/ACM, pp 70-80. 2013
Abstract. Early efforts in runtime verification show that parametric regular and temporal logic specifications can be monitored efficiently. These approaches, however, have limited expressiveness: their specifications always reduce to monitors with finite state. More recent developments showed that parametric context-free properties can be efficiently monitored with overheads generally lower than 12-15%. While context-free grammars are more expressive than finite-state languages, they still do not allow every computable safety property. This paper presents a monitor synthesis algorithm for string rewriting systems (SRS). SRSs are well known to be Turing complete, allowing for the formal specification of any computable safety property. Earlier attempts at Turing complete monitoring have been relatively inefficient. This paper demonstrates that monitoring parametric SRSs is practical. The presented algorithm uses a modified version of Aho-Corasick string searching for quick pattern matching with an incremental rewriting approach that avoids reexamining parts of the string known to contain no redexes.
PDF, Slides(PPT), Slides(KEY), Slides(PDF), MOP, DOI, ASE'13, BIB


2012 Technical Report

Efficient Parametric Runtime Verification with Deterministic String Rewriting
Patrick Meredith and Grigore Rosu
Technical Report http://www.ideals.illinois.edu/handle/2142/30467, March 2012
Abstract. Early efforts in runtime verification and monitoring show that parametric regular and temporal logic specifications can be monitored efficiently. These approaches, however, have limited expressiveness, since their specifications always reduce to monitors which are finite state machines. More recent developments showed that parametric context-free properties can be efficiently monitored with overheads generally lower than 12--15\%. While context-free grammars are more expressive than finite-state approaches, they still do not allow every computable safety property. This paper presents a monitor synthesis algorithm for string rewriting systems (SRS). SRSs are well known to be Turing complete, allowing for the formal specification of any computable safety property. Earlier attempts at Turing complete monitoring have been relatively inefficient. This paper demonstrates that monitoring parametric SRSs is practical. The presented monitoring algorithm uses a modified version of the Aho-Corasick string searching algorithm for quick pattern matching with an incremental rewriting approach that avoids reexamining parts of the string known to contain no redexes.
PDF, TR@UIUC, BIB


Personal tools
Namespaces

Variants
Actions
Navigation