Formal Verification of Web Service Behavioural Conformance through Testing

Abstract

Abstract. The value proposition of Web service technology lies in composability, reusability, and substitutability, a set of key characteristics that however give rise to major challenges when realising service-based systems, such as trustworthiness and interoperability. Thus, being able to verify that a Web service implementation conforms to certain functional or non-functional requirements is instrumental in engineering dependable service-based systems. This paper introduces a new approach to verifying the conformance of a Web service implementation against a behavioural specification, through the application of testing. We propose the use of Stream X-machines as an intuitive modelling formalism for constructing the behavioural specification of a stateful Web service, and propose the use of a method for deriving test cases from that specification in an automated way. The test generation method has been proven to produce complete sets of test cases that, under certain realistic assumptions, are guaranteed to reveal all non-conformance faults in a service implementation under test. The verification approach that we put forward can be applied in a range of different contexts and yield significant benefits for all types of stakeholders in a SOA environment, i.e. service providers, service consumers, and service brokers. 1