Path-Sensitive Reachability Analysis of Web Service Interfaces

WCFA(Web Service Interface Control Flow Automata) is enhanced by allowing pre/post-conditions for certain web service invocations to be declared. The formal definition of WCFA is given. Global behaviors of web service compositions(described by a set of WCFA) are captured by ARG(Abstract Reachability Graph), in which each control point is equipped with a state formula and a call stack. The algorithm for constructing ARG uses a path-sensitive analysis to compute the state formulas. Pre/post-conditions are verified during the construction, where unreachable states are detected and pruned. Assertions can be made at nodes of ARG to express both safety properties and call stack inspection properties. Then a SAT solver is used to check whether the assertions are logical consequences of the state formulas(or/and call stacks).