Information Technology Reference
In-Depth Information
S enter a loop: in each iteration, S
sends C the current account status,
and C has the choice to make a pay-
ment (but only for an amount that
would not overdraw the account) or
end the session. In the first case, C
sends the payee and amount to S, and
the loop is repeated. In the other case,
or if the authentication failed, the ses-
sion ends.
Our toolchain performs the veri-
fication across several levels, as ex-
plained below.
global protocol OnlineWallet
( role S, role C, role A) {
login(id: string ,pw: string )
from C to A;
choice at A{
login_ok() from A to C, S;
rec LOOP {
account(balance: int ,
overdraft: int ) from S to C;
choice at C{
@<amount <= balance+overdraft>
pay(payee: string , amount: int )
from C to S;
continue LOOP;
} or {
quit() from C to S; }}
} or {
login_fail(error: string )
from A to C, S; }}
Global Protocol Correctness. The
first level of verification is in the de-
signoftheglobalprotocol.TheScribblein Fig. 1 describes interactions between
session participants from the global perspective using message passing sequences,
branching (choice) and recursion. Each message has an operator (a label) and a
payload. The toolchain validates that the protocol is coherent and deadlock-free,
and thus projectable [7] for each role. For example, in each case of a choice con-
struct, the deciding party (e.g. at A ) must correctly communicate the decision
outcome unambiguously to all other roles involved; a choice is badly-formed if
the actions of the deciding party would cause a race condition on the selected
case between the other roles, or if it is ambiguous to another role whether the
decision has already been made or is still pending. The interested reader may
refer to [6,12] for a comprehensive overview of the Scribble syntax, a tutorial,
and further references to the formal conditions for protocol correctness.
Fig. 1. OnlineWallet protocol in Scribble
Local Protocol Conformance. The second level is runtime verification to
ensure that each endpoint program conforms to the core protocol structure ac-
cording to its role . There are two main factors. First, we verify that the type
(operation and payload) of each message matches its specification (operations
can be mapped directly to message headers, or to method calls, class names or
other relevant artifacts in the program). Second, we verify that the flow of inter-
actions is correct, i.e. interaction sequences, branches and recursions proceed as
expected, respecting the explicit dependencies (e.g. m1() from A to B; m2() from B
to C; imposes an input-output causality at B). These measures rule out errors,
such as communication mismatches, that violate the permitted protocol flow.
Fig. 2 outlines the concrete verification steps. First, local protocols are me-
chanically generated from the validated global protocol. A local protocol is essen-
tially a view of the global protocol from the perspective of one role. The projec-
tion algorithm works by identifying the message exchanges where the participant
is involved, and disregarding the rest while preserving the overall structure of
the global protocol. Each local protocol has a corresponding FSM, generated
by the monitor at runtime. When a party requests to start or join a session,
 
Search WWH ::




Custom Search