Industrial deployment of system engineering methods providing high dependability and productivity

 

Applying Model Checking to Generate Model-based Integration Tests from Choreography Models

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]
Preview
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

Deploy-Project - All right reserved