A framework for testing SWS from a user perspective based on WSMO goals. Translation of WSMO goal specifications into B formal models. Model checking for auto-generation of test cases from goal specifications. Independent to model-based generation, test case evaluation via mutation analysis. Tool implementation to automate the proposed steps for the test case evaluation.