Automated synthesis of composite services with correctness guarantee

ABSTRACT

In this paper, we propose a novel approach for composing existing web services to satisfy the correctness constraints to the design, including freeness of deadlock and unspecified reception, and temporal constraints in Computation Tree Logic formula. An automated synthesis algorithm based on learning algorithm is introduced, which guarantees that the composite service is the most general way of coordinating services so that the correctness is ensured. We have implemented a prototype system evaluating the effectiveness and efficiency of our synthesis approach through an experimental study.

REFERENCES

• 1: Daniela Berardi , Diego Calvanese , Giuseppe De Giacomo , Richard Hull , Massimo Mecella, Automatic composition of transition-based semantic web services with messaging, Proceedings of the 31st international conference on Very large data bases, August 30-September 02, 2005, Trondheim, Norway
• 2: Alessandro Cimatti , Edmund M. Clarke , Enrico Giunchiglia , Fausto Giunchiglia , Marco Pistore , Marco Roveri , Roberto Sebastiani , Armando Tacchella, NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.359-364, July 27-31, 2002
• 3: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.
• 4: Xiang Fu , Tevfik Bultan , Jianwen Su, Analysis of interacting BPEL web services, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA [doi>10.1145/988672.988756]
• 5: Richard Hull , Jianwen Su, Tools for composite web services: a short overview, ACM SIGMOD Record, v.34 n.2, June 2005 [doi>10.1145/1083784.1083807]
• 6: Panagiotis Manolios , Richard Trefler, Safety and Liveness in Branching Time, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.366, June 16-19, 2001
• 7: Ronald L. Rivest , Robert E. Schapire, Inference of finite automata using homing sequences, Information and Computation, v.103 n.2, p.299-347, April 1993 [doi>10.1006/inco.1993.1021]

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.3 INFORMATION STORAGE AND RETRIEVAL
      H.3.5 On-line Information Services
          Subjects: Web-based services

General Terms:
Algorithms, Design

Keywords:
composition synthesis, correctness constraints, learning algorithm