creators_name: Wieczorek, S. creators_name: Kozyura, V. creators_name: Roth, A. creators_name: Leuschel, Michael creators_name: Bendisposto, Jens creators_name: Plagge, Daniel creators_name: Schieferdecker, I. creators_id: leuschel@cs.uni-duesseldorf.de creators_id: plagge@cs.uni-duesseldorf.de type: article datestamp: 2009-09-07 08:16:40 lastmod: 2010-04-19 15:05:57 metadata_visibility: show title: Applying Model Checking to Generate Model-based Integration Tests from Choreography Models ispublished: inpress subjects: deploy_tooldev subjects: deploy_industrial_bus subjects: deploy_tooldev_modela subjects: deploy_tooldev_rodinplugins full_text_status: public 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. date: 2009 date_type: published publication: 21st IFIP Int. Conference on Testing of Communicating Systems and the 9th Int. Workshop on Formal Approaches to Testing of Software TESTCOM/FATES 2009 publisher: Springer LNCS refereed: TRUE citation: Wieczorek, S. and Kozyura, V. and Roth, A. and Leuschel, Michael and Bendisposto, Jens and Plagge, Daniel and Schieferdecker, I. (2009) Applying Model Checking to Generate Model-based Integration Tests from Choreography Models. 21st IFIP Int. Conference on Testing of Communicating Systems and the 9th Int. Workshop on Formal Approaches to Testing of Software TESTCOM/FATES 2009 . (In Press) document_url: http://deploy-eprints.ecs.soton.ac.uk/146/1/testcom_camera_ready.pdf