Information Technology Reference
In-Depth Information
log
Client
=(
{
Client
}
,
[(
Send,Request
)
,
(
Rec, Justify
)])
log
Agency
=(
{
Agency
}
,
[(
Rec, Request
)
,
(
Send,Debit
)])
log
Bank
=(
{
Bank
}
,
[(
Rec, Debit
)
,
(
Send,Justify
)]
)
log
Hotel
=(
{
Hotel
}
,
[])
If we execute
PropAnalysis
for
N oRoom
using all these logs it is clear that
Agency
is liable for
Client
's damages
4
, because only one scenario is generated
and fulfills the property
prop
NoRoom
. However, suppose that obtaining
log
Bank
canbeanissueandthatwewanttoverifyif
Agency
is responsible for the
incident. Then, the property can be analyzed for a reduced architecture using
only
log
Client
and
log
Agency
. This setting will generate the three scenarios de-
scribed in Example 7, but for all of them
prop
NoRoom
holds, which leads to the
conclusion that the claim is valid and
Agency
should be responsible.
5.2
Incremental Analysis
When results are not precise enough, a deeper investigation can be conducted,
for instance, inspecting more logs or in looking for some other dysfunctions. We
focus now on an incremental approach to obtain more precise results when more
logs are later added in the analysis.
Let
logs
and
prop
be respectively the logs and the property that have been
already analyzed. Now let
logs
be a new set of logs, selected in order to ob-
tain more precise results. Here we study how
scen
,ok
←
PropAnalysis
(
logs
∪
logs
,prop
)
can be incrementally computed, reusing the results obtained by
scen, ok
←
PropAnalysis
(
logs, prop
)
.
Incremental calculus for
merge
[
logs∪logs
]
. The following property allows
us to compute
merge
logs
]
[
logs
∪
.
Property 1.
(merge by parts) Let
logs
and
logs
be two sets of logs. We have:
logs
]=
logs
∪{
merge
[
logs
∪
union
(
{
merge
[
log
}
)
|
log
∈
merge
[
logs
]
}
]
logs
,prop
Then, in the first step of
PropAnalysis
(
logs
∪
)
it is possible to reuse
logs
]
the result of
merge
. However, the operation
extract
does not distribute on the operator merge (see Property 2 below).
[
logs
]
to compute
merge
[
logs
∪
scen
and
ok
.
Incremental calculus for
The results of
PropAnalysis
(
logs
∪
logs
,prop
can be approximated using the previous results for
scen
and
ok
in
the following way:
)
4
In law, the term “damage” is associated with an award of money to be paid as
compensation for loss or injury. In this paper we refer to this term in a more general
meaning.
Search WWH ::
Custom Search