Information Technology Reference
In-Depth Information
Fig. 4.
Sequence diagram for possible scenario
That is,
Agency
is responsible for the claim
LateCancel
if
Client
sends a message
to cancel the reservation before
Agency
sends the message to
Bank
charging the
client. Now, consider the scenario described in Figure 4 and an initial call of
PropAnalysis
only with
log
Client
and
log
Agency
. The values for the logs can be
written as follows:
log
Client
=(
{
Client
}
,
[(
Send,Request
)
,
(
Rec, Confirm
)
,
(
Rec, Justify
)
,
(
Send,Cancel
)])
log
Agency
=(
{
Agency
}
,
[(
Send,Request
)
,
(
Send, Book
)
,
(
Send,Debit
)])
Then, it is not possible to verify if the claim is valid, because the result of
merge
[
{
log
Client
,log
Agency
}
]
will produce 20 different scenarios where in ten of
them the position of
Cancel
Send
is before
Debit
Send
.
Now, we call
IncrPropAnalysis
with the result of the previous analysis and
log
Bank
that should contain the following value:
log
Bank
=(
{
Bank
}
,
[(
Rec, Debit
)
,
(
Send,Justify
)])
The bank's log adds a restriction to the previous scenarios. Now we know that
Client
tries to cancel the reservation after the message
(
Rec, Debit
)
. After exe-
cute
IncrPropAnalysis
we remain with four scenarios in
iscen
becauseweare
not sure about the position of the event
(
Rec, Confirm
)
. However, we obtain
iok
=
∅
and can conclude that the claim should be rejected.
6Con lu on
This paper has presented some parts of the LISE context [15], a project with
the objective to create a formal framework to precisely define liability in IT
systems and establish liability in case of failure. Our framework provides a model
for formally specifying the aspects of liability in a contractual setting. We also
present the specification for a log analyzer that can be used to establish the
validity of claims with relation to a given distributed log architecture. Finally,
we explore the aspects of incremental analysis for this log analyzer.
Search WWH ::
Custom Search