%A S. Wieczorek
%A V. Kozyura
%A A. Roth
%A Michael Leuschel
%A Jens Bendisposto
%A Daniel Plagge
%A I. Schieferdecker
%J 21st IFIP Int. Conference on Testing of Communicating Systems and the 9th Int. Workshop on Formal Approaches to Testing of Software TESTCOM/FATES 2009
%T Applying Model Checking to Generate Model-based Integration Tests from Choreography Models
%X 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.
%D 2009
%I Springer LNCS
%L deploy146

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>