A model checking strategy to test services in orchestrations

Very late binding, run-time integration of software elements owned and managed by third parties, run-time changes. These are just some of the characteristics of the service oriented computing paradigm which strongly affect static and dynamic verification capabilities. In this domain verification and testing research communities have to face new issues and revise existing solutions; possibly profiting of the new opportunities that the new paradigm makes available. In this paper, focusing on service orchestrations, we propose a novel approach to automatic test case generation aiming in particular at checking the behaviour of services participating to a given orchestration. The approach exploits the availability of a runnable model and uses model checking techniques to derive test cases suitable to detect possible integration problems.