Information Technology Reference
In-Depth Information
efficiency, we extend [13] to generate a nested FSM for each conversation thread, avoid-
ing the potential state explosion that comes from constructing their product. This allows
FSM generation in polynomial time and space in the length of the local protocol. The
(nested) FSMs are stored in a hash table with conversation id as the key. Transition func-
tions are similarly hashed, each entry having the shape: ( current state , transition )
( next state , assertion , var ),where transition is a triple ( label , sender , receiver ) and var
is the variable binder for the message payload. Due to standard MPST well-formedness
(message label distinction), any nested FSM is uniquely identifiable from any unordered
message, i.e. message-to-transition matching in a conversation FSM is deterministic.
The upper part of Figure 6 relates to in-conversation messages, which carry the con-
versation id (matching an entry in the FSM hash table), sender and receiver fields, and
the message label and payload. This information allows the monitor to retrieve the cor-
responding FSM (by matching the message signature to the FSM's transition function).
Assertions associated to communication actions are evaluated by invoking an external
logic engine; a monitor can be configured to use various logic engines, such as for the
validation of assertions, automata-based specifications (e.g. security automata), or other
stateful properties. Our current implementation uses a basic Python predicate evaluator,
which is sufficient for the use case protocols we have developed so far.
Monitoring Interrupts. FSM generation for interruptible local protocols again makes
use of nested FSMs. Each interruptible induces a nested FSM given by the main
interruptible block, as illustrated in Figure 7 for the User local protocol. The monitor
internally augments the nested FSM with a scope id, derived from the signature of the
interruptible block, and an interrupt table, which records the interrupt message signa-
tures that may be thrown or received in this scope. Interrupt messages are marked via
the same meta data field used to designate invitation and in-conversation messages, and
are are validated in a similar way except that they are checked against the interrupt ta-
ble. However, if an interrupt arrives that does not have a match in the interrupt table
of the immediate FSM(s), the check searches upwards through the parent FSMs; the
interrupt is invalid if it cannot be matched after reaching the outermost FSM is reached.
4
Evaluation
Our dynamic MPST verification framework has been implemented and integrated into
the current release of the Ocean Observatories infrastructure [30]. This section reports
on our integration efforts and the performance of our framework.
4.1
Experience: OOI Integration
The current release of OOI is based on a Service-Oriented Architecture, with all of
the distributed system services accessible by RPC. As part of their efforts to move to
agent-based systems in the next release, and to support distributed governance for more
than just individual RPC calls, we engineered the following step-by-step transition. The
first step was to add our Scribble monitor to the message interceptor stack of their mid-
dleware [31]. The second was to propose our conversation programming interface to
Search WWH ::




Custom Search