This study is presented in 2nd International Workshop on Quality Assurance for Service-Based Applications (QASBA) on July 15, 2013, Lugano, Switzerland, affiliated with International Symposium on Software Testing and Analysis, ISSTA The presentation will be available.

Why
Some orchestration specifications, such as VxBPEL, support variability to provide flexibility and to increase reusability of service-oriented systems. In such systems, variability information is scattered through the orchestration, which makes the system difficult to detect deadlocks and inconsistencies directly. Moreover, the need to check all possible orchestrations makes verification time consuming, costly and complex task.
How
Feature Transition Systems (FTS), one of the model checking approaches, is used to fulfill the need to formally verify variable orchestrations. Due to the grounding model differences between VxBPEL and FTS, mapping and transformation between these models should be explicitly specified.
What
A step by step transformation from source model, VxBPEL to target model, FTS model is introduced and implemented in Python. The implementation can be found on Git Repository.

Publication: Selma Suloglu, Riza Aktunc, Mustafa Yucefaydali, Verification of Variable Service Orchestrations using Model Checking, In 2nd International Workshop on Quality Assurance for Service-Based Applications (QASBA), July 15, 2013, Lugano, Switzerland. Access to Paper