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