Backward validation of communicating complex state machines in web services environments

Communicating Finite State Machines (CFSM) lack the high level syntactic and structural abstractions of Communicating Complex State Machines (CCSM), such as nesting and encapsulation, to model highly complex protocols that are likely to arise in web services environments. The incorporation of these features in a protocol specification model would require the design of a new validation technique to efficiently check for protocol errors, such as deadlocks and non-reachable transitions. A reachability graph is used to represent the execution states of the protocol and to verify their consistency. In this paper, we propose a new validation technique for protocols modeled with complex FSM, called RLRA (Reverse Leaping Reachability Analysis), which enables the detection of all deadlock errors. It is a backtracking approach, which first identifies an initial set of suspected states, those possibly containing deadlocks, then refines this set to those likely to cause deadlock, and finally backtracks through the graph while checking for errors until the root state of the protocol is reached. Leap graphs are employed to prune the number of execution states examined, and thereby mitigate the combinatorial explosion of the state space. Extensive tests and comparisons were performed, which show the effectiveness of our technique.