×

A generic framework for \(n\)-protocol compatibility checking. (English) Zbl 1245.68028

Summary: Service-oriented computing promotes the development of new systems from existing services which are usually accessed through their public interfaces. In this context, interfaces must be compatible in order to avoid interoperability issues. In this article, we propose a new framework for checking the compatibility of \(n\) service interfaces. Our framework is generic, in the sense that it implements several compatibility notions useful for different application areas, and extensible since new further notions can easily be incorporated. We consider a service interface model which takes behavioural descriptions with value-passing and non-observable actions into account. Our compatibility checking framework has been fully implemented into a prototype tool which relies on the rewriting logic-based system Maude.

MSC:

68M14 Distributed systems
68N01 General topics in the theory of software
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aldini, A.; Bernardo, M.: On the usability of process algebra: an architectural view, Theoretical computer science 335, No. 2–3, 281-329 (2005) · Zbl 1080.68071
[2] Aït-Bachir, A.; Dumas, M.; Fauvet, M. C.: BESERIAL: behavioural service interface analyser, Lncs 5240, 374-377 (2008)
[3] Attiogbé, C.; André, P.; Ardourel, G.: Checking component composability, Lncs 4089, 8-33 (2006)
[4] Bouhoula, A.; Jouannaud, J. P.; Meseguer, J.: Specification and proof in membership equational logic, Theoretical computer science 236, No. 1, 35-132 (2000) · Zbl 0938.68057
[5] Bordeaux, L.; Salaün, G.; Berardi, D.; Mecella, M.: When are two web services compatible?, Lncs 3324, 15-28 (2004)
[6] Brand, D.; Zafiropulo, P.: On communicating finite-state machines, Journal of the ACM 30, No. 2, 323-342 (1983) · Zbl 0512.68039
[7] Cámara, J.; Martin, J. A.; Salaün, G.; Cubo, J.; Ouederni, M.; Canal, C.; Pimentel, E.: ITACA: an integrated toolbox for the automatic composition and adaptation of web services, , 627-630 (2009)
[8] Canal, C.; Pimentel, E.; Troya, J. M.: Compatibility and inheritance in software architectures, Science of computer programming 41, No. 2, 105-138 (2001) · Zbl 0988.68026
[9] Chae, H. S.; Lee, J. S.; Bae, J. H.: An approach to checking behavioral compatibility between web services, International journal of software engineering and knowledge engineering 18, No. 2, 223-241 (2008)
[10] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J.: Maude: specification and programming in rewriting logic, Theoretical computer science 285, 187-243 (2002) · Zbl 1001.68059
[11] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C.: All about maude – A high-performance logical framework: how to specify, program, and verify systems in rewriting logic, Lncs 4350 (2007) · Zbl 1115.68046
[12] Cortellessa, V.; Potena, P.: Path-based error propagation analysis in composition of software services, Lncs 4829, 97-112 (2007)
[13] Cubo, J.; Salaün, G.; Canal, C.; Pimentel, E.; Poizat, P.: A model-based approach to the verification and adaptation of WF/.NET components, Entcs 215, 39-55 (2008)
[14] De Alfaro, L.; Henzinger, T.: Interface automata, Proc. of ESEC/FSE’01, 109-120 (2001)
[15] Deng, S. G.; Wu, Z.; Zhou, M.; Li, Y.; Wu, J.: Modeling service compatibility with pi-calculus for choreography, Lncs 4215, 26-39 (2006)
[16] Durán, F.; Ouederni, M.; Salaün, G.: Checking protocol compatibility using maude, Entcs 255, 65-81 (2009) · Zbl 1364.68282
[17] Frantzen, L.; Tretmans, J.; Willemse, T.: A symbolic framework for model-based testing, Lncs 4262, 40-54 (2006)
[18] Foster, H.; Uchitel, S.; Kramer, J.: LTSA-WS: a tool for model-based verification of web service compositions and choreography, , 771-774 (2006)
[19] Fu, X.; Bultan, T.; Su, J.: Analysis of interacting BPEL web services, Proc. of WWW’04, 621-630 (2004)
[20] Fu, X.; Bultan, T.; Su, J.: Synchronizability of conversations among web services, IEEE transactions in software engineering 31, No. 12, 1042-1055 (2005)
[21] Garavel, H.; Mateescu, R.; Lang, F.; Serwe, W.: CADP 2006: a toolbox for the construction and analysis of distributed processes, Lncs 4590, 158-163 (2007) · Zbl 1316.68074
[22] J.F. Groote, A.H.J. Mathijssen, M.A. Reniers, Y.S. Usenko, M.J. van Weerdenburg, The formal specification language mCRL2, in: E. Brinksma, D. Harel, A. Mader, P. Stevens, and R. Wieringa (Eds.), Methods for Modelling Software Systems (MMOSS), Dagstuhl Seminar Proceedings, 2007. · Zbl 1171.68400
[23] Hameurlain, N.: Flexible behavioural compatibility and substitutability for component protocols: a formal specification, Proc. of SEFM’07, 391-400 (2007)
[24] Hennessy, M.; Lin, H.: Symbolic bisimulations, Theoretical computer science 138, No. 2, 353-389 (1995) · Zbl 0874.68187
[25] Ingolfsdottir, A.; Lin, H.: A symbolic approach to value-passing processes, , 427-478 (2001) · Zbl 1027.68092
[26] Manning, C. D.; Schütze, H.: Foundations of statistical natural language processing, (1999) · Zbl 0951.68158
[27] Martens, A.: On compatibility of web services, Petri net newsletter 65, 12-20 (2003)
[28] Martens, A.; Moser, S.; Gerhardt, A.; Funk, K.: Analyzing compatibility of BPEL processes, , 147-156 (2006)
[29] Martín, J. A.; Pimentel, E.: Automatic generation of adaptation contracts, Entcs 229, 115-131 (2009) · Zbl 1347.68090
[30] Mateescu, R.; Poizat, P.; Salaün, G.: Adaptation of service protocols using process algebra and on-the-fly reduction techniques, Lncs 5364, 84-99 (2008)
[31] Meseguer, J.: Conditional rewriting logic as a unified model of concurrency, Theoretical computer science 96, No. 1, 73-155 (1992) · Zbl 0758.68043
[32] Meseguer, J.: Membership algebra as a logical framework for equational specification, Lncs 1376, 18-61 (1998) · Zbl 0903.08009
[33] Milner, R.: A calculus of communicating systems, (1980) · Zbl 0452.68027
[34] Milner, R.; Parrow, J.; Walker, D.: Modal logics for mobile processes, Theoretical computer science 114, No. 1, 149-171 (1993) · Zbl 0778.68033
[35] M. Ouederni, Maude Compatibility Checker, Available at http://www.lcc.uma.es/ meriem/tools.html.
[36] Pedersen, T.; Patwardhan, S.; Michelizzi, J.: Wordnet::similarity – measuring the relatedness of concepts, , 1024-1025 (2004)
[37] Plasil, F.; Visnovsky, S.: Behavior protocols for software components, IEEE transactions in software engineering 28, No. 11, 1056-1076 (2002)
[38] Poizat, P.; Royer, J. C.: A formal architectural description language based on symbolic transition systems and temporal logic, Journal of UCS 12, No. 12, 1741-1782 (2006)
[39] Ramadge, P. J. G.; Wonham, W. M.: The control of discrete event systems, Proceedings of the IEEE 77, No. 1, 81-98 (1989)
[40] Salaün, G.; Bordeaux, L.; Schaerf, M.: Describing and reasoning on web services using process algebra, International journal of BPIM 1, No. 2, 116-128 (2006)
[41] Shi, Y.; Zhang, L.; Liu, F.; Lin, L.; Shi, B.: Compatibility analysis of web services, Proc. of WI’05, 483-486 (2005)
[42] Yellin, D. M.; Strom, R. E.: Protocol specifications and components adaptors, ACM transactions on programming languages and systems 19, No. 2, 292-333 (1997)
[43] Wong, P. Y. H.; Gibbons, J.: Verifying business process compatibility, Proc. of QSIC’08, 126-131 (2008)
[44] Wonham, W. M.; Ramadge, P. J.: On the supremal controllable sublanguage of a given language, SIAM journal on control and optimization 25, No. 3, 637-659 (1987)
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.