Detecting Feature Interactions in Web Services with Timed Automata

With the rapid development of Web services, feature interactions have become one of the critical problems in Web services composition. This paper proposes a model checking method for detecting feature interactions in Web services composition. By the proposed method, the Web services descriptions written in WS-BPEL are translated into timed automata, and then we apply a well known model checking tool UPPAAL that supports this formalism to modeling Web services composition and analyzing feature interactions. We take a particular case study, an automatic stock trading system, as an example to illustrate the effectiveness of the proposed method.