zbMATH — the first resource for mathematics

AutoSyn: A new approach to automated synthesis of composite web services with correctness guarantee. (English) Zbl 1191.68816
Summary: How to compose existing web services automatically and to guarantee the correctness of the design (e.g., freeness of deadlock and unspecified reception, and temporal constraints) is an important and challenging problem in web services. Most existing approaches require a detailed specification of the desired behaviors of a composite service beforehand and then perform certain formal verification to guarantee the correctness of the design, which makes the composition process both complex and time-consuming. In this paper, we propose a novel approach, referred to as AutoSyn to compose web services, where the correctness is guaranteed in the synthesis process. For a given set of services, a composite service is automatically constructed based on \(L^*\) algorithm, which guarantees that the composite service is the most general way of coordinating services so that the correctness is ensured. We show the soundness and completeness of our solution and give a set of optimization techniques for reducing the time consumption. We have implemented a prototype system of AutoSyn and evaluated the effectiveness and efficiency of AutoSyn through an experimental study.

68U35 Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.)
68M11 Internet topics
Full Text: DOI
[1] Hull R, Su J. Tools for composite web services: a short overview. SIGMOD Rec, 2005, 34(2): 86–95 · Zbl 05444238 · doi:10.1145/1083784.1083807
[2] Berardi D, Calvanese D, Giacomo G, et al. Automatic composition of transition-based semantic web services with messaging. In: Proceeding of 31th International Conference on Very Large Databases, Trondheim, Norway, 2005. 613–624
[3] Fu X, Bultan T, Su J. Conversation protocols: a formalism for specification and verification of reactive electronic services. Theor Comput Sci, 2004, 328(1–2): 19–37 · Zbl 1071.68002 · doi:10.1016/j.tcs.2004.07.004
[4] Probert R L, Saleh K. Synthesis of communication protocols: Survey and assessment. IEEE Trans Comput, 1991, 40(4): 468–476 · Zbl 05104320 · doi:10.1109/12.88466
[5] Magee J, Kramer J, Uchitel S, et al, LTSA-WS: a tool for model-based verification of web service compositions and choreography, In: Proceeding of International Conference on Software Engineering, Shanghai, China, 2006. 771–774
[6] Rintanen J. Computational complexity of plan and controller synthesis under partial observability. Technical Report, 2005. http://users.rsise.anu.edu.au/jussi/Rintanen05compl.pdf .
[7] Pistore M, Traverso P, Bertoli P, et al. Automated synthesis of composite bpel4ws web services. In: Proceeding of International Conference on Web Services, Orlando, Florida, USA, 2005. 293–301
[8] Rivest R L, Schapire R E. Inference of finite automata using homing sequences. Inf Comput, 1993, 103(2): 299–347 · Zbl 0786.68082 · doi:10.1006/inco.1993.1021
[9] Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge, MA: MIT Press, 2000
[10] Manolios P, Trefler R J. Safety and liveness in branching time. In: Proceeding of 16th Annual IEEE Symposium on Logic in Computer Science, Boston, MA, USA, 2001. 366–374
[11] Garey M R, Johnson, D S. Computers and Intractability: A Guide to the Theory of NP-Completeness. New York: Freeman W. H. & Co., 1990 · Zbl 0411.68039
[12] Alur R, Cerny P, Madhusudan P, et al. Synthesis of interface specifications for java classes. In: Proceeding of Symposium on Principles of Programming Languages, Long Beach, California, USA, 2005. 98–109 · Zbl 1369.68126
[13] Milner R. Communicating and Mobile Systems: the Pi-Calculus. Cambridge: Cambridge University Press, 1999 · Zbl 0942.68002
[14] Berg T, Jonsson B, Leucker M, et al. Insights to angluin’s learning. In: Proceeding of International Workshop on Software Verification and Validation, Mumbai, India, 2003 · Zbl 1272.68164
[15] Wombacher A, Fankhauser P, Neuhold E J. Transforming bpel into annotated deterministic finite state automata for service discovery. In: Proceeding of International Conference of Web Services, San Diego, California, USA, 2004. 316–323
[16] Berardi D, Calvanese D, Giacomo G D, et al. \(\epsilon\)SC: A tool for automatic composition of services based on logics of programs. In: Proceeding of Workshop on Technologies for E-Services, Toronto, Canada, 2004. 80–94
[17] Cobleigh J M, Giannakopoulou D, Pasareanu C S. Learning assumptions for compositional verification. In: Proceeding of International Conference on Tools and algorithms for the Construction and Analysis of Systems, Warsaw, Poland, 2003. 331–346 · Zbl 1031.68545
[18] Berardi D, Calvanese D, Giacomo G, et al. Automatic composition of e-services that export their behavior. In: Proceeding of International Conference on Service Oriented Computing, Trento, Italy, 2003. 43–58
[19] Fan W, Geerts F, Gelade W. Complexity and composition of synthesized web services. In: Proceeding of Symposium on Principles of Database Systems, Vancourver, Canada, 2008. 231–240
[20] Pathak J, Basu S, Lutz R, et al. Parallel web service composition in moscoe: A choreography-based approach. In: Proceeding of European Conference on Web Services, Zurich, Switzerland, 2006. 3–12
[21] Mitra S, Kumar R, Basu S. Automated choreographer synthesis for web services composition using i/o automata. In: Proceeding of International Conference on Web Services, Salt Lake City, Utah, USA, 2007. 364–371
[22] Marconi A, Pistore M, Traverso P. Specifying data-flow requirements for the automated composition of web services. In: Proceeding of IEEE International Conference on Software Engineering and Formal Methods, Pune, India, 2006. 147–156
[23] Ponnekanti S, Fox A. Sword: A developer toolkit for web service composition. In: Proceeding of World Wide Web Conference, Honolulu, Hawaii, USA, 2002
[24] Sirin E, Parsia B, Wu D, et al. HTN planning for web service composition using shop2. J Web Semant, 2004, 1(4): 377–396
[25] Pu K, Hristidis V, Koudas N. Syntactic rule based approach toweb service composition. In: Proceeding of International Conference on Data Engineering, Atlanta, Georgia, USA, 2006. 31–40
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.