Lightweight formal analysis of Web service flows

Abstract

BPEL (Business Process Execution Language) is proposed as a standard language to describe Web service flows. A flow may contain multiple activities that are executed concurrently, and thus removing faults such as deadlocks or violations of application-specific properties is not easy. This paper proposes techniques to extract a behavioral specification from the BPEL program and to verity it with the model checking technique. © 2005 National Instiute of Informatics.