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)
![[img]](../style/images/fileicons/application_pdf.png)
| PDF (Applying Model Checking to Generate Model-based Integration Tests from Choreography Models) 215Kb |
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.
| Item Type: | Article |
|---|---|
| Subjects: | Tool developments Industrial Deployment > Business Tool developments > Model checking Tool developments > Rodin plug-ins |
| ID Code: | 146 |
| Deposited By: | Dr Andreas Roth |
| Deposited On: | 07 Sep 2009 09:16 |
| Last Modified: | 19 Apr 2010 16:05 |
Repository Staff Only: item control page
