Information Technology Reference
In-Depth Information
∀u. ∀s.
[
SUM
a
a,i.
[0
,
31)
ψ
(
u, a,i
)](
s
;
u
)
→ s
10000
(P1)
∀u. ∀s.
[
SUM
a
a,i.
[0
,
31)
ψ
(
u, a, i
)](
s
;
u
)
∧
(
¬limit off
(
u
)
S
limit on
(
u
))
→
(P2)
s
10000
∀u. ∀s.∀m.
[
AVG
a
a,i.
[0
,
91)
ψ
(
u, a,i
)](
s
;
u
)
∧
(P3)
[
MAX
a
a.
[0
,
8)
withdraw
(
u, a
)](
m
;
u
)
→ m
2
· s
∀s.
[
AVG
u
u, c.
[
CNT
i
a,i.
[0
,
31)
ψ
(
u, a, i
)](
c
;
u
)](
s
)
→ s
150
(P4)
∀u. ∀c.
[
CNT
j
v,p,j.
[
AVG
a
a,i.
[0
,
31)
ψ
(
u, a, i
)](
v
;
u
)
∧
(P5)
[0
,
31)
ψ
(
u, p, j
)
∧
2
· v ≺ p
](
c
;
u
)
→ c
5
Fig. 3.
Policy formalizations, where
ψ
(
u, a,i
) abbreviates
withdraw
(
u, a
)
∧ ts
(
i
).
τ
0
,
Γ
0
)
,
...
,
eval
(
ψ
,
i
1,
τ
i−
1
,
Γ
i−
1
)
were called previously in this order, where
Γ
j
=(
p
D
j
)
p∈
R
f
is the family of interpretations of flexible predicates at
j
,for
every time point
j
−
∈
N
.
4 Experimental Evaluation
We compare our prototype implementation, which extends our monitoring tool
MonPoly [5] for MFOTL, with the relational database PostgreSQL [22] and
the stream-processing tool STREAM [2]. For our evaluation, we consider the
following five policies. Figure 3 contains their MFOTL
Ω
formalizations.
(P1) The sum of withdrawals of each user over the last 30 days does not exceed
the limit of $10,000.
(P2) Similar to (P1), except that the withdrawals must not exceed $10,000 only
when the flag for checking the limit is set.
(P3) The maximal withdrawal of each user over the last seven days must be
at most be twice as large as the average of the user's withdrawals over
the last 90 days.
(P4) The average of the number of withdrawals of all users over the last 30 days
should be less than a given threshold of 150.
(P5) For each user, the number of peaks over the last 30 days does not exceed
a threshold of 5, where a peak is a value at least twice the average over
some time window.
Note that in the formalization of the policy (P2), the event
limit on
(
u
)setsthe
limit flag for the user
u
, while
limit off
(
u
) unsets it.
We use synthetically generated logs
1
with different time spans (in days). The
logs contain withdraw events from 500 users, except for (P5), for which we con-
sider only 100 users. Each user makes on average five withdrawals per day. Table 1
shows the running times of the three tools on a standard desktop computer with
1
Our prototype, the formulas, and the input data are available as an archive at
