@InProceedings{Wieczorek2009,
  author    = {Sebastian Wieczorek and Vitaly Kozyura and Andreas Roth and Michael Leuschel and Jens Bendisposto and Daniel Plagge and Ina Kathrin Schieferdecker},
  booktitle = {Testing of Software and Communication Systems, 21st {IFIP} {WG} 6.1 International Conference, {TESTCOM} 2009 and 9th International Workshop, {FATES} 2009, Eindhoven, The Netherlands, November 2-4, 2009. Proceedings},
  title     = {Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models},
  doi       = {10.1007/978-3-642-05031-2_12},
  pages     = {179--194},
  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.},
  file      = {:2009/Wieczorek2009 - Applying Model Checking to Generate Model Based Integration Tests from Choreography Models.pdf:PDF},
  keywords  = {Model Checking, Model-based Testing, Formal Methods, Integration Testing, Service Choreography Models},
  type      = {conference},
  year      = {2009}
}