Abstract
Choreography models describe the communication protocols between services. Testing of service choreographies is an important task for the quality assurance of service-based systems as used e.g. in the context of service-oriented architectures (SOA). The formal modeling of service choreographies enables a model-based integration testing (MBIT) approach. We present MBIT methods for our service choreography modeling approach called Message Choreography Models (MCM). For the model-based testing of service choreographies, MCMs are translated into Event-B models and used as input for our test generator which uses the model checker ProB.
Chapter PDF
References
Business Process Modeling Notation (BPMN) Specification 2.0, Submitted Draft Proposal V0.9, http://www.omg.org/cgi-bin/doc?bmi/08-11-01
Abrial, J.-R.: The B–Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: A roadmap for the Rodin toolset. In: Abstract State Machines, B and Z (2008)
Abrial, J.-R., Hallerstede, S.: Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B. Fundam. Inform. 77(1-2), 1–28 (2007)
Aho, A.V., Dahbura, A.T., Lee, D., Uyar, M.Ü.: An Optimization Technique for Protocol Conformance Test Generation Based on UIO Sequences and Rural Chinese Postman Tours. IEEE Trans. Commun. 39, 1604–1615 (1991)
Ali, S., Briand, L., Jaffar-Ur Rehman, M., Asghar, H., Iqbal, M.Z., Nadeem, A.: A State-Based Approach to Integration Testing Based on UML Models. Information & Software Technology 49(11–12), 1087–1106 (2007)
Ambert, F., Bouquet, F., Chemin, S., Guenaud, S., Legeard, B., Peureux, F., Utting, M., Vacelet, N.: BZ-Testing-Tools: A Tool-Set for Test Generation from Z and Busing Constraint Logic Programming. In: Proc. of FATES 2002, pp. 105–120 (2002)
Butler, M.: Decomposition Structures for Event-B. In: Integrated Formal Methods (2009)
Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221–236. Springer, Heidelberg (2005)
Craggs, I., Sardis, M., Heuillard, T.: AGEDIS Case Studies: Model-Based Testing in Industry. In: Proc. of ECMDA 2003, pp. 129–132 (2003)
Gallagher, L., Offutt, A.J., Cincotta, A.: Integration Testing of Object-oriented Components using Finite State Machines. J. Software Testing, Verification, and Reliability (2006)
Hoare, C.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Jaffuel, E., Legeard, B.: LEIRIOS Test Generator: Automated Test Generation from B Models. B 2007, 277–280 (2007)
Jard, C., Jeron, T.: TGV: theory, principles and algorithms. J. Software Tools for Technology Transfer 7(4), 297–315 (2005)
Kavantzas, N., Burdett, D., Ritzinger, G., Lafon, Y.: Web services choreography description language. W3C candidate recomm (2005), http://www.w3.org/TR/ws-cdl-10
Leuschel, M.: The High Road to Formal Validation. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 4–23. Springer, Heidelberg (2008)
Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Satpathy, M., Leuschel, M., Butler, M.: ProTest: An Automatic Test Environment for B Specifications. In: Proc. ENTCS 111, pp. 113–136 (2005)
Satpathy, M., Butler, M., Leuschel, M., Ramesh, S.: Automatic Testing from Formal Specifications. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 95–113. Springer, Heidelberg (2007)
Snook, F., Butler, M.: UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)
Tretmans, J., Brinksma, E.: TorX: Automated Model Based Testing. In: EMSOFT (2002)
Utting, U., Legeard, B.: Practical Model-Based Testing – A Tools Approach. Morgan Kaufmann Publ., San Francisco (2007)
Web Services Reliable Messaging (WS-ReliableMessaging), Version 1.1. OASIS Consortiom, http://docs.oasis-open.org/ws-rx/wsrm/v1.1/wsrm.pdf
Weyuker, E.: Testing component-based software – a cautionary tale. IEEE Software 15(5), 54–59 (1998)
Wieczorek, S., Roth, A., Stefanescu, A., Charfi, A.: Precise Steps for Choreography Modeling for SOA Validation and Verification. In: SOSE, pp. 148–153. IEEE, Los Alamitos (2008)
Wieczorek, S., Roth, A., Stefanescu, A., Kozyura, V., Charfi, A., Kraft, F.M., Schieferdecker, I.: Viewpoints for Modeling Choreographies in Service-Oriented Architectures. In: Proc. of WICSA 2009. IEEE Computer Society, Los Alamitos (to appear, 2009)
Wieczorek, S., Stefanescu, A., Großmann, J.: Enabling Model-Based Testing for SOA Integration Testing. In: MOTIP, pp. 77–82. Fraunhofer IRB Verlag (2008)
Wieczorek, S., Stefanescu, A., Schieferdecker, I.: Model-based Integration Testing of Enterprise Services. In: Proc. TAICPART. IEEE Computer Society, Los Alamitos (2009)
Wieczorek, S., Stefanescu, A., Schieferdecker, I.: Test Data Provision for ERP Systems. In: Proc. of ICST, pp. 396–403. IEEE Computer Society, Los Alamitos (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wieczorek, S. et al. (2009). Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models. In: Núñez, M., Baker, P., Merayo, M.G. (eds) Testing of Software and Communication Systems. FATES TestCom 2009 2009. Lecture Notes in Computer Science, vol 5826. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-05031-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-05031-2_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-05030-5
Online ISBN: 978-3-642-05031-2
eBook Packages: Computer ScienceComputer Science (R0)