Information Technology Reference
In-Depth Information
Example 2.
(claim
LateCancel
) Let us consider another claim where having can-
celed the reservation,
Client
is still charged by
Agency
. Then,
Client
complains
to
Agency
that s/he sent the message to cancel the reservation. On the other
side,
Agency
complains that
Client
did not send the message before the reser-
vation date. In this example, the time that the client sends the message can be
confused with the time that the message is received by
Hotel
. It is necessary to
make clear in the agreement between
Agency
and
Client
how such details will
be taken into account.
In such situations, liability can be specified in terms of well-defined properties
written in function of events recorded in the logs. Consider, for example, the
scenario in Figure 3. In this scenario
Agency
does not send the request of reser-
vation to
Hotel
, but still charges the client by sending a message to
Bank
.
Client
receives the justification from
Bank
and could think that, although s/he has no
confirmation from
Hotel
(maybe
Client
does not even know that should receive
a confirmation from
Hotel
), the fact that s/he was charged by
Agency
assures
the confirmation of the reservation.
Fig. 3.
Sequence diagram for possible scenario where claim
NoRoom
will happen
For the agreement to work it is necessary that the values found in the logs can
be trusted by all entities of the system and that it contains no error. In this pa-
per, we assume that this hypothesis is valid and the values that compose the logs
correspond exactly to what happened (no duplication, no replication, no loss).
2.2 Notation B
This formal framework is based on the B-method [1]. This methodology was cho-
sen because it allows specifications that are focused both on data and behavior.
Another important aspect for our lawyer partners is the industrial status of this
approach [5, 2] that is a positive argument in term of trust, a central notion in law.
We give here a short summary of the B notations we use in this paper. Given two
sets,
A
and
B
, the set of relations between
A
and
B
, the set of functions from
A
to
B
,
and the set of partial functions from
A
to
B
are respectively denoted by
A
↔
B
,
A
the relational
image of
U
under the relation
R
(set of all elements that are under relation
R
with
an element of
U
), and
union
→
B
,and
A
→
B
.Wenote
F
(
A
)
all finite subsets of
A
,
R
[
U
]
the generalized union of
A
(union of all elements
of the set
A
). We denote by
f
−
1
the inverse function for
f
and by
iseq
(
A
)
(
A
)
the set of
Search WWH ::
Custom Search