Abstract
One of the ultimate goals of Service Oriented Computing (SOC) is to provide support for the automatic on-demand discovery of basic functionalities that, once combined, correctly compute a user defined task. To this aim, it is necessary for services to come equipped with a computer-understandable interface that allow applications to match the provided functionalities with the user needs. In this context, a prominent issue concerns the compliance between the operations invoked by the client – the client protocol – and the operations executed by the service – the service protocol. Process calculi, the theoretical tools investigated in the Work Package 2 of Sensoria, can contribute to the solution of this problem. The idea we present in this chapter is to describe the externally observable message-passing behaviour of services as process calculi expressions; following recently adopted terminology, we call this description the service contract. We show how, in certain cases, service contracts can be automatically extracted out of service behaviour, and how they can be used to formally check the compliance among the communication protocols of interacting services.
This work has been partially sponsored by the project Sensoria, IST-2005-016004.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Acciai, L., Boreale, M.: Type abstractions of name-passing processes. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 302–317. Springer, Heidelberg (2007)
Acciai, L., Boreale, M.: Spatial and Behavioral Types in the Pi-Calculus. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 372–386. Springer, Heidelberg (2008)
Bravetti, M., Zavattaro, G.: A Foundational Theory of Contracts for Multi-party Service Composition. Fundamenta Informaticae 89(4), 451–478 (2008)
Bravetti, M., Zavattaro, G.: Contract-Based Discovery and Composition of Web Services. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol. 5569, pp. 261–295. Springer, Heidelberg (2009)
Bravetti, M., Zavattaro, G.: Towards a Unifying Theory for Choreography Conformance and Contract Compliance. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol. 4829, pp. 34–50. Springer, Heidelberg (2007), http://www.cs.unibo.it/~bravetti/html/techreports.html
Carpineti, S., Castagna, G., Laneve, C., Padovani, L.: A Formal Account of Contracts for Web Services. In: Bravetti, M., Núñez, M., Tennenholtz, M. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 148–162. Springer, Heidelberg (2006)
Christensen, S., Hirshfeld, Y., Moller, F.: Bisimulation equivalence is decidable for basic parallel processes. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 143–157. Springer, Heidelberg (1993)
De Nicola, R., Hennessy, M.: Testing Equivalences for Processes. Theoretical Computer Science 34, 83–133 (1984)
Esparza, J.: More Infinite Results. In: Current trends in Theoretical Computer Science: entering the 21st century, pp. 480–503 (2001)
Fournet, C., Gouthier, G.: The Reflexive Chemical Abstract Machine and the Join Calculus. In: Proc. of POPL 1996, pp. 372–385. ACM Press, New York (1996)
Fournet, C., Hoare, C.A.R., Rajamani, S.K., Rehof, J.: Stuck-Free Conformance. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 242–254. Springer, Heidelberg (2004)
Milner, R.: A complete axiomatization for observational congruence of finite-state behaviours. Information and Computation 81, 227–247 (1989)
Hirshfeld, Y., Moller, F.: Decidability Results in Automata and Process theory. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 102–148. Springer, Heidelberg (1996)
Igarashi, A., Kobayashi, N.: A Generic Type System for the Pi-Calculus. In: Proc. of POPL, pp. 128–141. ACM Press, New York (2001); Full version appeared in Theoretical Computer Science 311(1-3), 121–163 (2004)
Kobayashi, N., Suenaga, K., Wischik, L.: Resource Usage Analysis for the Pi-Calculus. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 298–312. Springer, Heidelberg (2006)
OASIS. Web Services Business Process Execution Language Version 2.0
Rensink, A., Vogler, W.: Fair testing. Information and Computation 205(2), 125–198 (2007)
Sangiorgi, D.: The name discipline of uniform receptiveness. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256. Springer, Heidelberg (1997); Theoretical Computer Science 221(1-2), 457–493 (1999)
Stirling, C.: Modal Logics for Communicating Systems. Theoretical Computer Science 49(2-3), 311–347 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Boreale, M., Bravetti, M. (2011). Advanced Mechanisms for Service Composition, Query and Discovery. In: Wirsing, M., Hölzl, M. (eds) Rigorous Software Engineering for Service-Oriented Systems. Lecture Notes in Computer Science, vol 6582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20401-2_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-20401-2_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20400-5
Online ISBN: 978-3-642-20401-2
eBook Packages: Computer ScienceComputer Science (R0)