×

Session types for safe web service orchestration. (English) Zbl 1283.68065

Summary: We address the general problem of interaction safety in Web service orchestrations. By considering an essential subset of the BPEL orchestration language, we define SeB, a session based style of this subset. We discuss the formal semantics of SeB and present its main properties. We take a new approach to address the formal semantics which is based on a translation into so-called control graphs. Our semantics accounts for BPEL control links and addresses the static semantics that prescribes the valid usage of variables. We also provide the semantics of service configurations.
During a session, a client and a service can engage in a complex series of interactions. By means of the provided semantics, we define precisely what is meant by interaction safety. We then introduce session types in order to prescribe the correct orderings of these interactions. Service providers must declare their provided and required session types. We define a typing algorithm that checks if a service orchestration behaves according to its declared provided and required types.
Using a subtyping relation defined on session types, we show that any configuration of well-typed service partners with compatible session types are interaction safe, i.e., involved partners never receive unexpected messages.

MSC:

68M11 Internet topics

Software:

CADP; BPEL2oWFN; Orc; COWS
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Chinnici, R.; Moreau, J.-J.; Ryman, A.; Weerawarana, S., Web Service Definition Language (WSDL) Version 2.0, W3C (Jun. 2007), Tech. rep.
[2] Lapadula, A.; Pugliese, R.; Tiezzi, F., A WSDL-based type system for asynchronous WS-BPEL processes, Form. Methods Syst. Des., 38, 2, 119-157 (2011) · Zbl 1217.68061
[3] Yoshida, N.; Vasconcelos, V. T., Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication, (Proceedings of the First International Workshop on Security and Rewriting Techniques. Proceedings of the First International Workshop on Security and Rewriting Techniques, SecReT 2006. Proceedings of the First International Workshop on Security and Rewriting Techniques. Proceedings of the First International Workshop on Security and Rewriting Techniques, SecReT 2006, Electronic Notes in Theoretical Computer Science, vol. 171 (4) (2007)), 73-93
[4] Lanese, I.; Martins, F.; Vasconcelos, V. T.; Ravara, A., Disciplining orchestration and conversation in service-oriented computing, (Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods. Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods, SEFM ʼ07 (2007), IEEE Computer Society: IEEE Computer Society Washington, DC, USA), 305-314
[5] Organization for the Advancement of Structured Information Standards (OASIS), Web Services Business Process Execution Language (WS-BPEL) Version 2.0 (Apr. 2007)
[6] König, D.; Lohmann, N.; Moser, S.; Stahl, C.; Wolf, K., Extending the compatibility notion for abstract WS-BPEL processes, (Proceedings of the 17th International Conference on World Wide Web, WWW ʼ08 (2008), ACM: ACM New York, NY, USA), 785-794
[7] Bruni, R.; Lanese, I.; Melgratti, H.; Tuosto, E., Multiparty sessions in SOC, (Lea, D.; Zavattaro, G., Coordination Models and Languages. Coordination Models and Languages, Lecture Notes in Computer Science, vol. 5052 (2008), Springer: Springer Berlin/Heidelberg), 67-82
[8] Honda, K.; Yoshida, N.; Carbone, M., Multiparty asynchronous session types, SIGPLAN Not., 43, 273-284 (2008) · Zbl 1295.68150
[9] Kitchin, D.; Quark, A.; Cook, W.; Misra, J., The ORC programming language, (Lee, D.; Lopes, A.; Poetzsch-Heffter, A., Formal Techniques for Distributed Systems. Formal Techniques for Distributed Systems, Lecture Notes in Computer Science, vol. 5522 (2009), Springer: Springer Berlin/Heidelberg), 1-25 · Zbl 1217.68049
[10] Cardelli, L.; Mitchell, J., Operations on records, (Main, M.; Melton, A.; Mislove, M.; Schmidt, D., Mathematical Foundations of Programming Semantics. Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, vol. 442 (1990), Springer: Springer Berlin/Heidelberg), 22-52 · Zbl 1509.68046
[11] Groote, J.; van de Pol, J., State space reduction using partial \(τ\)-confluence, (Nielsen, M.; Rovan, B., Mathematical Foundations of Computer Science 2000. Mathematical Foundations of Computer Science 2000, Lecture Notes in Computer Science, vol. 1893 (2000), Springer: Springer Berlin/Heidelberg), 383-393 · Zbl 0996.68122
[12] Fernandez, J.; Garavel, H.; Kerbrat, A.; Mounier, L.; Mateescu, R.; Sighireanu, M., CADP a protocol validation and verification toolbox, (Alur, R.; Henzinger, T., Computer Aided Verification. Computer Aided Verification, Lecture Notes in Computer Science, vol. 1102 (1996), Springer: Springer Berlin/Heidelberg), 437-440
[13] Vallecillo, A.; Vasconcelos, V. T.; Ravara, A., Typing the behavior of software components using session types, Fund. Inform., 73, 4, 583-598 (2006) · Zbl 1114.68384
[14] Gay, S.; Hole, M., Types and subtypes for client-server interactions, (Swierstra, S., Programming Languages and Systems. Programming Languages and Systems, Lecture Notes in Computer Science, vol. 1576 (1999), Springer: Springer Berlin/Heidelberg), 74-90
[15] Ng, N.; Yoshida, N.; Pernet, O.; Hu, R.; Kryftis, Y., Safe parallel programming with session Java, (De Meuter, W.; Roman, G.-C., Coordination Models and Languages. Coordination Models and Languages, Lecture Notes in Computer Science, vol. 6721 (2011), Springer: Springer Berlin/Heidelberg), 110-126
[16] Mostrous, D.; Vasconcelos, V., Session typing for a featherweight Erlang, (De Meuter, W.; Roman, G.-C., Coordination Models and Languages. Coordination Models and Languages, Lecture Notes in Computer Science, vol. 6721 (2011), Springer: Springer Berlin/Heidelberg), 95-109
[17] Boreale, M.; Bruni, R.; Caires, L.; De Nicola, R.; Lanese, I.; Loreti, M.; Martins, F.; Montanari, U.; Ravara, A.; Sangiorgi, D.; Vasconcelos, V.; Zavattaro, G., A service centered calculus, (Bravetti, M.; Núñez, M.; Zavattaro, G., Web Services and Formal Methods. Web Services and Formal Methods, Lecture Notes in Computer Science, vol. 4184 (2006), Springer: Springer Berlin/Heidelberg), 38-57
[18] Boreale, M.; Bruni, R.; De Nicola, R.; Loreti, M., Sessions and pipelines for structured service programming, (Barthe, G.; de Boer, F., Formal Methods for Open Object-Based Distributed Systems. Formal Methods for Open Object-Based Distributed Systems, Lecture Notes in Computer Science, vol. 5051 (2008), Springer: Springer Berlin/Heidelberg), 19-38
[19] Fantechi, A.; Najm, E., Session types for orchestration charts, (Lea, D.; Zavattaro, G., Coordination Models and Languages. Coordination Models and Languages, Lecture Notes in Computer Science, vol. 5052 (2008), Springer: Springer Berlin/Heidelberg), 117-134
[20] Kopp, O.; Khalaf, R.; Leymann, F., Deriving explicit data links in WS-BPEL processes, (IEEE SCC (2) (2008)), 367-376
[21] Ouyang, C.; Verbeek, E.; van der Aalst, W. M.P.; Breutel, S.; Dumas, M.; ter Hofstede, A. H.M., Formal semantics and analysis of control flow in WS-BPEL, Sci. Comput. Programming, 67, 2-3, 162-198 (2007) · Zbl 1122.68073
[22] Martens, A., Analyzing web service based business processes, (Cerioli, M., Fundamental Approaches to Software Engineering. Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 3442 (2005), Springer: Springer Berlin/Heidelberg), 19-33 · Zbl 1119.68305
[23] Lapadula, A.; Pugliese, R.; Tiezzi, F., Using formal methods to develop WS-BPEL applications, FOSDʼ12. FOSDʼ12, Sci. Comput. Programming, 77, 3, 189-213 (2012)
[24] Lapadula, A.; Pugliese, R.; Tiezzi, F., A calculus for orchestration of web services, (De Nicola, R., Programming Languages and Systems. Programming Languages and Systems, Lecture Notes in Computer Science, vol. 4421 (2007), Springer: Springer Berlin/Heidelberg), 33-47 · Zbl 1187.68070
[25] Viroli, M., A core calculus for correlation in orchestration languages, Web Services and Formal Methods. Web Services and Formal Methods, J. Log. Algebr. Program., 70, 1, 74-95 (2007) · Zbl 1178.68051
[26] Castagna, G.; Dezani-Ciancaglini, M.; Giachino, E.; Padovani, L., Foundations of session types, (PPDPʼ09 (2009), ACM Press), 219-230
[27] Lago, U. D.; Giamberardino, P. D., Soft session types, (Luttik, B.; Valencia, F., EXPRESS. EXPRESS, EPTCS, vol. 64 (2011)), 59-73 · Zbl 1457.68185
[28] Honda, K.; Vasconcelos, V.; Kubo, M., Language primitives and type discipline for structured communication-based programming, (Hankin, C., Programming Languages and Systems. Programming Languages and Systems, Lecture Notes in Computer Science, vol. 1381 (1998), Springer: Springer Berlin/Heidelberg), 122-138
[29] Acciai, L.; Boreale, M.; Zavattaro, G., Behavioural contracts with request-response operations, (Clarke, D.; Agha, G., Coordination Models and Languages. Coordination Models and Languages, Lecture Notes in Computer Science, vol. 6116 (2010), Springer: Springer Berlin/Heidelberg), 16-30
[30] Castagna, G.; Gesbert, N.; Padovani, L., A theory of contracts for web services, (Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ʼ08 (2008), ACM: ACM New York, NY, USA), 261-272 · Zbl 1295.68080
[31] Laneve, C.; Padovani, L., The pairing of contracts and session types, (Degano, P.; De Nicola, R.; Meseguer, J., Concurrency, Graphs and Models. Concurrency, Graphs and Models, Lecture Notes in Computer Science, vol. 5065 (2008), Springer: Springer Berlin/Heidelberg), 681-700 · Zbl 1143.68330
[32] Lohmann, N., A feature-complete Petri net semantics for WS-BPEL 2.0, (Dumas, M.; Heckel, R., Web Services and Formal Methods. Web Services and Formal Methods, Lecture Notes in Computer Science, vol. 4937 (2008), Springer: Springer Berlin/Heidelberg), 77-91
[33] Massuthe, P.; Schmidt, K., Operating guidelines - an automata-theoretic foundation for the service-oriented architecture, (Fifth International Conference on Quality Software, 2005. Fifth International Conference on Quality Software, 2005, QSIC 2005 (2005), IEEE Computer Society), 452-457
[34] Lohmann, N., Why does my service have no partners?, (Bruni, R.; Wolf, K., Web Services and Formal Methods. Web Services and Formal Methods, Lecture Notes in Computer Science, vol. 5387 (2009), Springer: Springer Berlin/Heidelberg), 191-206
[35] Massuthe, P.; Serebrenik, A.; Sidorova, N.; Wolf, K., Can I find a partner? Undecidability of partner existence for open nets, Inform. Process. Lett., 108, 6, 374-378 (2008) · Zbl 1191.68442
[36] Fiadeiro, J.; Lopes, A., An interface theory for service-oriented design, (Giannakopoulou, D.; Orejas, F., Fundamental Approaches to Software Engineering. Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 6603 (2011), Springer: Springer Berlin/Heidelberg), 18-33
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.