Difference between revisions of "ERE Monitoring Algorithm"

From FSL
Jump to: navigation, search
 
(14 intermediate revisions by 3 users not shown)
Line 1: Line 1:
 
__NOTOC__ __NOEDITSECTION__
 
__NOTOC__ __NOEDITSECTION__
{{shortcut|[[MOP]] <br /> [[Special:EREPlugin|ERE Plugin]] <br /> [[ERE Plugin Input Syntax]] <br /> [[ERE Plugin Output Syntax]] <br /> ERE Monitoring Algorithm}}
+
{{shortcut|[[Special:EREPlugin|ERE Plugin]] <br /> [[ERE Plugin Input Syntax | ERE Input Syntax]] <br /> [[ERE Plugin Output Syntax | ERE Output Syntax]]}}
  
'''''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.
  
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 compactlyGenerating optimal ERE monitors is highly non-trivial and the interested reader should refer to the below papersOne 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 an FSM description 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) ''then'' R2{a} ''else'' empty ''endif''
 +
        R*{a} = (R{a}) R*
 +
      ! R{a} = ! (R{a})
 +
        b{a} = ''if'' (b == a) ''then'' epsilon ''else'' empty ''endif''
 +
  epsilon{a} = empty
 +
    empty{a} = empty
 +
 
 +
For a given ERE one generates all possible derivatives that the ERE
 +
can generate for all possible sequences of events. This set of
 +
derivatives is finite and its size depends on the size of the initial
 +
ERE.  However a number of these derivative EREs can be equivalent
 +
to each other.  We check the equivalence of EREs using an automatic
 +
procedure based on coinduction, getting a set of equivalence classes
 +
of derivativesThese equivalence classes form distinct states in
 +
the optimal FSM. For a given ERE one generates all possible derivatives that the ERE
 +
can generate for all possible sequences of events.  This set of
 +
derivatives is finite and its size depends on the size of the initial
 +
EREHowever a number of these derivative EREs can be equivalent
 +
to each other.  We check the equivalence of EREs using an automatic
 +
procedure based on coinduction, getting a set of equivalence classes
 +
of derivatives.  These equivalence classes form distinct states in
 +
the optimal FSM that is generated at the end.  This technique can avoid the
 +
huge state blow up that is caused by the generally taught technique of building
 +
a non-deterministic FSM and determinizing it, because equivalence class minimization is done
 +
by need, rather than after the deterministic FSM is fully generated.
  
 
=== Publications ===
 
=== Publications ===

Latest revision as of 06:27, 24 June 2009

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 an FSM description 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) then R2{a} else empty endif
       R*{a} = (R{a}) R*
      ! R{a} = ! (R{a})
        b{a} = if (b == a) then epsilon else empty endif
  epsilon{a} = empty
    empty{a} = empty

For a given ERE one generates all possible derivatives that the ERE can generate for all possible sequences of events. This set of derivatives is finite and its size depends on the size of the initial ERE. However a number of these derivative EREs can be equivalent to each other. We check the equivalence of EREs using an automatic procedure based on coinduction, getting a set of equivalence classes of derivatives. These equivalence classes form distinct states in the optimal FSM. For a given ERE one generates all possible derivatives that the ERE can generate for all possible sequences of events. This set of derivatives is finite and its size depends on the size of the initial ERE. However a number of these derivative EREs can be equivalent to each other. We check the equivalence of EREs using an automatic procedure based on coinduction, getting a set of equivalence classes of derivatives. These equivalence classes form distinct states in the optimal FSM that is generated at the end. This technique can avoid the huge state blow up that is caused by the generally taught technique of building a non-deterministic FSM and determinizing it, because equivalence class minimization is done by need, rather than after the deterministic FSM is fully generated.

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
RV'03, ENTCS 89, issue 2, pp 108 - 127. 2003.
PDF, ENTCS, RV'03, DBLP, BIB

Personal tools
Namespaces

Variants
Actions
Navigation