Abstract
Workflow-based service composition languages foster the rapid design and development of distributed applications. The behavioral verification of service Compositions has widely been addressed at design time, using model-checking. Testing is a complementary technique when it comes to check the behavioral conformance of a service implementation with respect to its specification or to a user or a service need. In this paper we address this issue with an automatic approach based on symbolic testing and an SMT solver.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
OASIS: Web Services Business Process Execution Language (WSBPEL) Version 2.0. Technical report, OASIS (April 2007)
ter Beek, M.H., Bucchiarone, A., Gnesi, S.: Formal Methods for Service Composition. Annals of Mathematics, Computing & Teleinformatics 1(5), 1–10 (2007)
Poizat, P., Royer, J.C.: A Formal Architectural Description Language based on Symbolic Transition Systems and Modal Logic. JUCS 12(12), 1741–1782 (2006)
Bentakouk, L., Poizat, P., Zaïdi, F.: A Formal Framework for Service Orchestration Testing based on Symbolic Transition Systems. In: Proc. of TESTCOM, pp. 16–32 (2009)
Bentakouk, L., Poizat, P., Zaïdi, F.: A Formal Framework for Service Orchestration Testing based on Symbolic Transition Systems. Long version, in P. Poizat Webpage (2009)
Bozkurt, M., Harman, M., Hassoun, Y.: Testing Web Services: A Survey. Technical report, King’s College London (2010)
Mayer, P.: Design and Implementation of a Framework for Testing BPEL Compositions. PhD thesis, Leibnitz University, Germany (2006)
Bartolini, C., Bertolino, A., Marchetti, E., Parissis, I.: Data flow-based validation of web services compositions: Perspectives and examples. In: de Lemos, R., Di Giandomenico, F., Gacek, C., Muccini, H., Vieira, M. (eds.) Architecting Dependable Systems V. LNCS, vol. 5135, pp. 298–325. Springer, Heidelberg (2008)
Bartolini, C., Bertolino, A., Marchetti, E., Polini, A.: Towards automated WSDL-based testing of web services. In: Bouguettaya, A., Krueger, I., Margaria, T. (eds.) ICSOC 2008. LNCS, vol. 5364, pp. 524–529. Springer, Heidelberg (2008)
Hallé, S., Hughes, G., Bultan, T., Alkhalaf, M.: Generating interface grammars from wsdl for automated verification of web services. In: ICSOC/ServiceWave, pp. 516–530 (2009)
Lallali, M., Zaïdi, F., Cavalli, A., Hwang, I.: Automatic Timed Test Case Generation for Web Services Composition. In: Proc. of ECOWS (2008)
Kaschner, K., Lohmann, N.: Automatic test case generation for interacting services. In: ICSOC Workshops, pp. 66–78 (2008)
Jeannet, B., Jéron, T., Rusu, V., Zinovieva, E.: Symbolic test selection based on approximate analysis. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 349–364. Springer, Heidelberg (2005)
Gaston, C., Le Gall, P., Rapin, N., Touil, A.: Symbolic execution techniques for test purpose definition. In: Uyar, M.Ü., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, pp. 1–18. Springer, Heidelberg (2006)
Frantzen, L., Huerta, M., Kiss, Z., Wallet, T.: On-The-Fly Model-Based Testing of Web Services with Jambition. In: Laneve, C., Su, J. (eds.) WS-FM 2009. LNCS, vol. 6194. Springer, Heidelberg (2010)
Cabot, J., Clarisó, R., Riera, D.: UMLtoCSP: a Tool for the Formal Verification of UML/OCL Models using Constraint Programming. In: Proc. of ASE, pp. 547–548.
Kovács, M., Varró, D., Gönczy, L.: Formal analysis of BPEL workflows with compensation by model checking. Int. Journal of Computer Sciences & Engineering, 35–49 (2008)
Mateescu, R., Poizat, P., Salaün, G.: Adaptation of service protocols using process algebra and on-the-fly reduction techniques. In: Bouguettaya, A., Krueger, I., Margaria, T. (eds.) ICSOC 2008. LNCS, vol. 5364, pp. 84–99. Springer, Heidelberg (2008)
Mateescu, R., Rampacek, S.: Formal Modeling and Discrete-Time Analysis of BPEL Web Services. In: Advances in Enterprise Engineering I, vol. 10. LNBIP, pp. 179–193 (2008)
Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans. Softw. Eng. 29(2), 99–115 (2003)
Ziadi, T., Hélouët, L., Jézéquel, J.M.: Towards a uml profile for software product lines. In: Proc. of Software Product-Family Engineering, pp. 129–139 (2003)
Gastin, P., Oddoux, D.: Fast LTL to Büchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 53. Springer, Heidelberg (2001)
Pickin, S., Jard, C., Jéron, T., Jézéquel, J.M., Traon, Y.L.: Test synthesis from uml models of distributed software. IEEE Trans. Software Eng. 33(4), 252–269 (2007)
King, J.C.: Symbolic Execution and Program Testing. Communications of the ACM 19(7), 385–394 (1976)
Khurshid, S., Păsăreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)
Frantzen, L., Tretmans, J., Willemse, T.A.C.: A Symbolic Framework for Model-Based Testing. In: Proc. of FATES/RV (2006)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 118–149 (2003)
de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Garavel, H., Mateescu, R., Lang, F., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)
Conchon, S., Contejean, E., Kanig, J.: Ergo: a theorem prover for polymorphic first-order logic modulo theories (2006), http://ergo.lri.fr/papers/ergo.ps
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bentakouk, L., Poizat, P., Zaïdi, F. (2011). Checking the Behavioral Conformance of Web Services with Symbolic Testing and an SMT Solver. In: Gogolla, M., Wolff, B. (eds) Tests and Proofs. TAP 2011. Lecture Notes in Computer Science, vol 6706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21768-5_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-21768-5_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21767-8
Online ISBN: 978-3-642-21768-5
eBook Packages: Computer ScienceComputer Science (R0)