Information Technology Reference
In-Depth Information
As the main contribution of this paper, we define an algorithm to automatically de-
rive, from a finite-state property definition, a runtime monitor that can process such
aggregated traces. We prove that the current formulation of our algorithm produces
monitors that are guaranteed not to miss property violations. As we also show, the mon-
itor processes the compressed event stream in bounded time, while not producing more
false positives than a naıve monitor that traverses the original property state machine
using all possible permutations of the original event trace. Our algorithm can be eas-
ily parameterized with di
erent acceptance conditions that can decrease the number of
warnings further while allowing for some missed violations.
To summarize, this paper presents the following original contributions:
ff
-
a general trace model in which trace producers supply, for certain periods of time,
aggregated information about events that occurred during those periods,
-
an algorithm that automatically constructs a monitor for such traces from a finite-
state property definition,
-
a proof that the algorithm always converges and that the resulting monitor is guaran-
teed not to miss any actual violations and is optimally precise given the aggregated
trace information it receives, and
-
a complexity estimation for the resulting monitoring algorithm.
The remainder of this paper is structured as follows. Section 2 presents a motivating
example, leading to a description of
constraint automata
in Section 3. Section 4 defines
a process for translating finite state automata into constraint automata, and Section 5 re-
gards complexity and implementation considerations. The paper discusses related work
in Section 6 and concludes in Section 7.
2
Introductory Example
Consider the automaton illustrated in Figure 1. We follow the model of a trace classi-
fier, where di
erent error messages, for instance as
implemented through JavaMOP [8]. In this example, both the event sequenceslogout
·
login and login
·
logout are in the language of the automaton, yet they lead to dif-
ferent states, which in our model means that they would be classified di
ff
erent accepting states can cause di
ff
ff
erently.
login
logout
A
1
A
2
S
logout
logout
B
1
B
2
B
3
login
Fig. 1.
A deterministic automaton
