title: Applying Model Checking to Generate Model-based Integration Tests from Choreography Models
creator: Wieczorek, S.
creator: Kozyura, V.
creator: Roth, A.
creator: Leuschel, Michael
creator: Bendisposto, Jens
creator: Plagge, Daniel
creator: Schieferdecker, I.
subject: Tool developments
subject: Business
subject: Model checking
subject: Rodin plug-ins
description: 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.
publisher: Springer LNCS
date: 2009
type: Article
type: PeerReviewed
format: application/pdf
identifier: http://deploy-eprints.ecs.soton.ac.uk/146/1/testcom_camera_ready.pdf
identifier:   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)  
relation: http://deploy-eprints.ecs.soton.ac.uk/146/