Lightweight formal analysis of Web service flows
Shin Nakajima · Progress in Informatics · 2005
BPEL (Business Process Execution Language) is proposed as a standard language to describe Web service fl ows.A fl ow may contain multiple activities that are executed concurrently, and thus removing faults such as deadlocks or violations of application-specifi c properties is not easy.This paper proposes techniques to extract a behavioral specifi cation from the BPEL program and to verity it with the model checking technique.