×

A WSDL-based type system for asynchronous WS-BPEL processes. (English) Zbl 1217.68061

Summary: We tackle the problem of providing rigorous formal foundations to current software engineering technologies for web services, and especially to WSDL and WS-BPEL, two of the most used XML-based standard languages for web services. We focus on a simplified fragment of WS-BPEL sufficiently expressive to model asynchronous interactions among web services in a network context. We present this language as a process calculus-like formalism, that we call WS-CALCULUS, for which we define an operational semantics and a type system. The semantics provides a precise operational model of programs, while the type system forces a clean programming discipline for integrating collaborating services. We prove that the operational semantics of WS-CALCULUS and the type system are ‘sound’ and apply our approach to some illustrative examples. We expect that our formal development can be used to make the relationship between WS-BPEL programs and the associated WSDL documents precise and to support verification of their conformance.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N15 Theory of programming languages
68M11 Internet topics
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] van der Aalst WMP, Lassen KB (2008) Translating unstructured workflow processes to readable BPEL: Theory and implementation. Inf Softw Technol 50(3):131–159 · doi:10.1016/j.infsof.2006.11.004
[2] Acciai L, Boreale M (2008) Spatial and behavioral types in the pi-calculus. In: CONCUR. LNCS, vol 5201. Springer, Berlin, pp 372–386 · Zbl 1160.03312
[3] Acciai L, Boreale M (2008) A type system for client progress in a service-oriented calculus. In: Concurrency, graphs and models. LNCS, vol 5065. Springer, Berlin, pp 642–658 · Zbl 1143.68469
[4] Amadio R, Castellani I, Sangiorgi D (1998) On bisimulations for the asynchronous pi-calculus. Theor Comput Sci 195(2):291–324 · Zbl 0915.68009 · doi:10.1016/S0304-3975(97)00223-5
[5] Arkin A, Askary S, Fordin S, Jekeli W, Kawaguchi K, Orchard D, Pogliani S, Riemer D, Struble S, Takacsi-Nagy P, Trickovic I, Zimek S (2002) Web service choreography interface (WSCI) 1.0. Tech rep, W3C. Available at http://www.w3.org/TR/wsci/
[6] Banerji A, Bartolini C, Beringer D, Chopella V, Govindarajan K, Karp A, Kuno H, Lemon M, Pogossiants G, Sharma S, Williams S (2002) Web services conversation language (WSCL) 1.0. Tech rep, W3C Note. Available at http://www.w3.org/TR/2002/NOTE-wscl10-20020314
[7] Battle S, Bernstein A, Boley H, Grosof B, Gruninger M, Hull R, Kifer M, Martin D, McIlraith S, McGuinness D, Su J, Tabet S (2005) Semantic web services framework (SWSF) 1.0. Tech rep, SWSL Committee. Available at http://www.daml.org/services/swsf/1.0/
[8] Bettini L, Coppo M, D’Antoni L, De Luca M, Dezani-Ciancaglini M, Yoshida N (2008) Global progress in dynamically interleaved multiparty sessions. In: CONCUR. LNCS, vol 5201. Springer, Berlin, pp 418–433 · Zbl 1160.68456
[9] Boag S, Chamberlin D, Fernández M, Florescu D, Robie J, Siméon J (2007) Xquery 1.0: an XML query language. Tech rep, W3C. Available at http://www.w3.org/TR/xquery/
[10] Bocchi L, Laneve C, Zavattaro G (2003) A calculus for long-running transactions. In: FMOODS. LNCS, vol 2884. Springer, Berlin, pp 124–138 · Zbl 1253.68056
[11] Bonelli E, Compagnoni AB (2007) Multipoint session types for a distributed calculus. In: TGC. LNCS, vol 4912. Springer, Berlin, pp 240–256
[12] Boreale M, Bruni R, De Nicola R, Loreti M (2008) Sessions and pipelines for structured service programming. In: FMOODS. LNCS, vol 5051. Springer, Berlin, pp 19–38
[13] van Breugel F, Koshkina M (2006) Models and verification of BPEL. Tech rep, Department of Computer Science and Engineering, York University. Available at http://www.cse.yorku.ca/\(\sim\)franck/research/drafts/tutorial.pdf
[14] Bruni R, Butler M, Ferreira C, Hoare C, Melgratti H, Montanari U (2005) Comparing two approaches to compensable flow composition. In: CONCUR. LNCS, vol 3653. Springer, Berlin, pp 383–397 · Zbl 1134.68316
[15] Bruni R, Melgratti H, Montanari U (2005) Theoretical foundations for compensations in flow composition languages. In: POPL. ACM, New York, pp 209–220 · Zbl 1369.68070
[16] Busi N, Gorrieri R, Guidi C, Lucchi R, Zavattaro G (2005) Choreography and orchestration: a synergic approach for system design. In: ICSOC. LNCS, vol 3826. Springer, Berlin, pp 228–240
[17] Butler M, Ferreira C (2004) An operational semantics for StAC, a language for modelling long-running business transactions. In: COORDINATION. LNCS, vol 2949. Springer, Berlin, pp 87–104 · Zbl 1081.68643
[18] Caires L, Vieira H (2009) Conversation types. In: ESOP. LNCS, vol 5502. Springer, Berlin, pp 285–300 · Zbl 1234.68291
[19] Carbone M, Honda K, Yoshida N (2007) A calculus of global interaction based on session types. In: DCM. ENTCS, vol 171. Elsevier, Amsterdam, pp 127–151 · Zbl 1277.68171
[20] Carbone M, Honda K, Yoshida N (2007) Structured communication-centred programming for web services. In: ESOP. LNCS, vol 4421. Springer, Berlin, pp 2–17 · Zbl 1187.68064
[21] Carpineti S, Laneve C (2006) A basic contract language for web services. In: ESOP. LNCS, vol 3924. Springer, Berlin, pp 197–213 · Zbl 1178.68122
[22] Carpineti S, Laneve C, Padovani L (2009) PiDuce–a project for experimenting Web services technologies. Sci Comput Program 74(10):777–811 · Zbl 1194.68077 · doi:10.1016/j.scico.2009.03.002
[23] Castagna G, Gesbert N, Padovani L (2009) A theory of contracts for Web services. ACM Trans Program Lang Syst 31:5 · Zbl 1295.68080
[24] Chaki S, Rajamani SK, Rehof J (2002) Types as models: model checking message-passing programs. In: POPL. ACM, New York, pp 45–57 · Zbl 1323.68365
[25] Christensen E, Curbera F, Meredith G, Weerawarana S (2001) Web services description language (WSDL) 1.1. Tech rep, W3C. Available at http://www.w3.org/TR/wsdl/
[26] Clark J, DeRose S (1999) XML path language (XPath) Version 1.0. Tech rep, W3C. Available at http://www.w3.org/TR/xpath/
[27] Cook W, Patwardhan S, Misra J (2006) Workflow patterns in ORC. In: COORDINATION. LNCS, vol 4038. Springer, Berlin, pp 82–96
[28] Dragoni N, Mazzara M (2010) A formal semantics for the WS-BPEL recovery framework: the pi-calculus way. In: WS-FM. LNCS, vol 6194. Springer, Berlin, pp 92–109
[29] Erl T (2009) SOA design patterns. Prentice Hall, New York
[30] Foster H, Uchitel S, Magee J, Kramer J (2006) LTSA-WS: a tool for model-based verification of web service compositions and choreography. In: ICSE. ACM, New York, pp 771–774
[31] Fu X, Bultan T, Su J (2005) Synchronizability of conversations among web services. IEEE Trans Softw Eng 31(12):1042–1055 · Zbl 05114773 · doi:10.1109/TSE.2005.141
[32] Gay S, Vasconcelos V (2010) Linear type theory for asynchronous session types. J Funct Program 20(1):19–50 · Zbl 1185.68194 · doi:10.1017/S0956796809990268
[33] Geguang P, Xiangpeng Z, Shuling W, Zongyan Q (2005) Semantics of BPEL4WS-like fault and compensation handling. In: FM. LNCS, vol 3582. Springer, Berlin, pp 350–365 · Zbl 1120.68324
[34] Geguang P, Huibiao Z, Zongyan Q, Shuling W, Xiangpeng Z, Jifeng H (2006) Theoretical foundations of scope-based compensable flow language for web service. In: FMOODS. LNCS, vol 4037. Springer, Berlin, pp 251–266
[35] Geguang P, Xiangpeng Z, Shuling W, Zongyan Q (2006) Towards the semantics and verification of BPEL4WS. In: DCM. ENTCS, vol 151. Elsevier, Amsterdam, pp 33–52 · Zbl 1120.68324
[36] Gudgin M, Hadley M, Rogers T (2006) Web services addressing 1.0–Core. Tech rep, W3C. Available at http://www.w3.org/TR/ws-addr-core
[37] Guidi C, Lucchi R, Gorrieri R, Busi N, Zavattaro G (2006) SOCK: a calculus for service oriented computing. In: ICSOC. LNCS, vol 4294. Springer, Berlin, pp 327–338
[38] Guidi C, Lanese I, Montesi F, Zavattaro G (2008) On the interplay between fault handling and request-response service invocations. In: ACSD. IEEE, New York, pp 190–198
[39] Hinz S, Schmidt K, Stahl C (2005) Transforming BPEL to Petri nets. In: BPM. LNCS, vol 3649. Springer, Berlin, pp 220–235
[40] Honda K, Vasconcelos VT, Kubo M (1998) Language primitives and type discipline for structured communication-based programming. In: ESOP. LNCS, vol 1381. Springer, Berlin, pp 122–138
[41] Honda K, Yoshida N, Carbone M (2008) Multiparty asynchronous session types. In: POPL. ACM, New York, pp 273–284 · Zbl 1295.68150
[42] Igarashi A, Kobayashi N (2004) A generic type system for the pi-calculus. Theor Comput Sci 311(1–3):121–163 · Zbl 1070.68105 · doi:10.1016/S0304-3975(03)00325-6
[43] Kazhamiakin R, Pistore M (2006) Static verification of control and data inWeb service compositions. In: ICWS. IEEE, New York, pp 83–90 · Zbl 1225.68032
[44] Kitchin D, Cook W, Misra J (2006) A language for task orchestration and its semantic properties. In: CONCUR. LNCS, vol 4137. Springer, Berlin, pp 477–491 · Zbl 1151.68360
[45] Kobayashi N (2003) Type systems for concurrent programs. In: UNU/IIST. LNCS, vol 2757. Springer, Berlin, pp 439–453 · Zbl 1274.68076
[46] Kobayashi N, Suenaga K, Wischik L (2006) Resource usage analysis for the {\(\pi\)}-calculus. In: VMCAI. LNCS, vol 3855. Springer, Berlin, pp 298–312 · Zbl 1176.68135
[47] Kobayashi N (2008) Typical: type-based static analyzer for the picalculus. Tool available at http://www.kb.ecei.tohoku.ac.jp/koba/typical
[48] Kovács M, Gönczy L, Varró D (2008) Formal analysis of BPEL workflows with compensation by model checking. J Comput Syst Sci Eng 23(5):35–49
[49] Lanese I, Martins F, Ravara A, Vasconcelos V (2007) Disciplining orchestration and conversation in service-oriented computing. In: SEFM. IEEE, New York, pp 305–314
[50] Laneve C, Zavattaro G (2005) Foundations of web transactions. In: FoSSaCS. LNCS, vol 3441. Springer, Berlin, pp 282–298 · Zbl 1118.68335
[51] Laneve C, Zavattaro G (2005) Web-pi at work. In: TGC. LNCS, vol 3705. Springer, Berlin, pp 182–194 · Zbl 1151.68539
[52] Lapadula A, Pugliese R, Tiezzi F (2006) A WSDL-based type system for WS-BPEL. In: COORDINATION. LNCS, vol 4038. Springer, Berlin, pp 145–163 · Zbl 1217.68061
[53] Lapadula A, Pugliese R, Tiezzi F (2007) A calculus for orchestration of web services. In: ESOP. LNCS, vol 4421. Springer, Berlin, pp 33–47 · Zbl 1187.68070
[54] Lapadula A, Pugliese R, Tiezzi F (2007) C WS: a timed service-oriented calculus. In: ICTAC. LNCS, vol 4711. Springer, Berlin, pp 275–290 · Zbl 1147.68846
[55] Lapadula A, Pugliese R, Tiezzi F (2008) A formal account of WS-BPEL. In: COORDINATION. LNCS, vol 5052. Springer, Berlin, pp 199–215
[56] Leymann F (2001) Web services flow language (WSFL 1.0). Tech rep, IBM. Available at http://xml.coverpages.org/wsfl.html
[57] Lohmann N (2008) A feature-complete Petri net semantics for WS-BPEL 2.0. In: WSFM. LNCS, vol 4937. Springer, Berlin, pp 77–91
[58] Mazzara M, Lucchi R (2007) A pi-calculus based semantics for WS-BPEL. J Log Algebr Program 70(1):96–118 · Zbl 1178.68367 · doi:10.1016/j.jlap.2006.05.007
[59] Meredith L, Bjorg S (2003) Contracts and types. Commun ACM 46(10):41–47 · Zbl 05393987 · doi:10.1145/944217.944236
[60] Mezzina LG (2008) Typses: a tool for type checking session types. Tool available at http://www.di.unipi.it/mezzina
[61] OASIS WSBPEL TC (2007) Web services business process execution language version 2.0. Tech rep, OASIS. Available at http://docs.oasis-open.org/wsbpel/2.0/OS/
[62] Object Management Group (1996) The common object request broker: architecture and specification (CORBA 2.0). Tech rep, OMG. Available at http://www.corba.org/
[63] Ouyang C, Dumas M, ter Hofstede AHM, van der Aalst WMP (2006) From BPMN process models to BPEL web services. In: ICWS. IEEE, New York, pp 285–292
[64] Ouyang C, Verbeek E, van der Aalst W, Breutel S, Dumas M, ter Hofstede A (2007) Formal semantics and analysis of control flow in WS-BPEL. Sci Comput Program 67(2–3):162–198 · Zbl 1122.68073 · doi:10.1016/j.scico.2007.03.002
[65] Schmidt K (2000) LoLA–a low level analyser. In: ICATPN. LNCS, vol 1825. Springer, Berlin, pp 465–474 · Zbl 0986.68684
[66] Thatte S (2001) Xlang: Web services for business process design. Tech rep, Microsoft. Available at http://xml.coverpages.org/xlang.html
[67] Viroli M (2004) Towards a formal foundational to orchestration languages. In: WSFM. ENTCS, vol 105. Elsevier, Amsterdam, pp 51–71 · Zbl 1271.68196
[68] Wright A, Felleisen M (1994) A syntactic approach to type soundness. Inf Comput 115(1):38–94 · Zbl 0938.68559 · doi:10.1006/inco.1994.1093
[69] XMethods (2010). http://www.xmethods.com
[70] Yoshida N, Vasconcelos VT (2007) Language primitives and type discipline for structured communication-based programming revisited: two systems for higher-order session communication. In: SecReT. ENTCS, vol 171/4. Elsevier, Amsterdam, pp 73–93
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.