Generic contract-regulated web service composition specification and verification

Abstract

This paper presents a novel formal method to describe contracrt-regulated service composition components using abstract concepts and (semi-) automatically verify the specification. We model web service component behaviours and the contracts based on Tecton language expressed using "concept descriptions", to be used with Violet verification system to prove properties of service composition component. The verified generic contract-regulated composition specification at an abstract level will be used in a variety of instances as BPEL specification without repeating the proof. The main advantage of this method is to improve the reusability of specification and seamlessly integrate behaviour descriptions with contacts. © 2013 Springer-Verlag.