Information Technology Reference
In-Depth Information
logs
,prop,scen,ok
iscen, iok
←
IncrPropAnalysis
(
)=
PRE
logs
∈
LOG ARCH
∧
prop
∈
PROP
∧
scen
∈F
(
LOG FILE
)
∧
ok
∈F
(
LOG FILE
)
∧
agents
(
prop
)
⊆
agents
(
scen
)
∧
agents
(
prop
)
⊆
agents
(
ok
)
THEN
iscen
:=
logs
∪{
extract
agents
(
prop
)
[
union
(
{
merge
[
log
}
]
|
log
∈
scen
}
)];
logs
∪{
iok
:=
extract
agents
(
prop
)
[
union
(
{
merge
[
log
}
]
|
log
∈
ok
}
)]
END
END
Now we can compare:
scen, ok
←
PropAnalysis
(
logs, prop
)
scen
,ok
←
logs
,prop
PropAnalysis
(
logs
∪
)
logs
,prop,scen,ok
iscen, iok
←
IncrPropAnalysis
(
)
The result is:
ok
⊆
ok
and
scen
⊆
iok
⊆
iscen
⊆
scen
This result can be concluded using the following property.
Property 2.
(extraction by parts) Let
log
be a log,
log arch
a log architecture,
and
ags
a set of agents. We have:
extract
ags
[
merge
[
log arch
∪{
log
}
)]
⊆
extract
ags
[
merge
[
log arch
∪{
extract
ags
(
log
)
}
)]
This property suggests that when an extraction is made before the merge some
information about the order of events may be lost and may result in a large set
of scenarios for
merge
.Since
IncrPropAnalysis
uses the results
scen
and
ok
of
PropAnalysis
, some information may be lost with the extraction of the events
that only concern the agents of the property.
Application. Although we do not obtain exact results, this operation is inter-
esting because it does not retest the researched property, what can be a complex
step. Moreover in some cases we may obtain conclusive results. For instance, it
is always the case where
iok
=
∅
or
iok
=
iscen
.
Example 9.
Suppose the claim
LateCancel
=(
Client, Agency, prop
LateCancel
)
such that:
agents
(
prop
LateCancel
)=
{
Client, Agency
}∧
val
(
prop
LateCancel
)=
λlog.
(
agents
(
log
)=
{
Client, Agency
}|
(
Send,Cancel
)
∈
events
(
log
)
∧
(
Send,Debit
)
∈
events
(
log
)
∧
pos
((
Send,Cancel
)
,log
)
<pos
((
Send,Debit
)
,log
))
Search WWH ::
Custom Search