# Difference between revisions of "ERE Monitoring Algorithm"

Line 19: | Line 19: | ||

(R1 + R2){a} = R1{a} + R2{a} | (R1 + R2){a} = R1{a} + R2{a} | ||

− | (R1 R2){a} = (R1{a}) R2 + ''if'' (epsilon in R1) then R2{a} else empty endif | + | (R1 R2){a} = (R1{a}) R2 + ''if'' (epsilon in R1) ''then'' R2{a} ''else'' empty ''endif'' |

R*{a} = (R{a}) R* | R*{a} = (R{a}) R* | ||

! R{a} = ! (R{a}) | ! R{a} = ! (R{a}) | ||

− | b{a} = if (b == a) then epsilon else empty endif | + | b{a} = ''if'' (b == a) ''then'' epsilon ''else'' empty ''endif'' |

epsilon{a} = empty | epsilon{a} = empty | ||

empty{a} = empty | empty{a} = empty |

## Revision as of 04:30, 30 October 2008

**Under construction!**

Regular expressions can be easily understood by ordinary software engineers and programmers, as shown by the immense interest in and the success of scripting languages like Perl, based essentially on regular expression pattern matching. We believe that regular expressions provide an elegant and powerful specification language also for monitoring requirements, because an execution trace of a program is in fact a string of states. Extended regular expressions (EREs) add complementation to regular expressions, which brings additional benefits by allowing one to specify patterns that must not occur during an execution. Complementation gives one the power to express patterns on strings non-elementarily more compactly. Also, one important observation about the use of ERE in the context of runtime verification is that ERE patterns are often used to describe *buggy* patterns instead of desired properties.

Our approach is to generate a minimal binary transition tree finite state
machines (BTT-FSM) instead from an ERE using coinductive techniques.
Briefly, in our approach we use the concept of derivatives
of a regular expression which is based on the idea of ``event
consumption*, in the sense that an extended regular expression R*
and an event a produce another extended regular expression, denoted
R{a}, with the property that for any trace w, a w in R if
and only if w in R{a}. Let's consider an operation _{_}
which takes an ERE and an event, then we give several equations
which define its operational semantics recursively, on the structure
of regular expressions:

(R1 + R2){a} = R1{a} + R2{a} (R1 R2){a} = (R1{a}) R2 +if(epsilon in R1)thenR2{a}elseemptyendifR*{a} = (R{a}) R* ! R{a} = ! (R{a}) b{a} =if(b == a)thenepsilonelseemptyendifepsilon{a} = empty empty{a} = empty

### Publications

More information can be found in the following paper:

*Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation*- Feng Chen and Grigore Rosu
, ENTCS 89, issue 2, pp 108 - 127. 2003.**RV'03**

PDF, ENTCS, RV'03, DBLP, BIB