|
Online ISSN:1349-8606 |
Progress in Informatics |
|
No.2 November 2005 |
|
Page 57-76 |
PDF(1,527KB) | References |
doi:10.2201/NiiPi.2005.2.5 |
Lightweight formal analysis of Web service flows |
Shin NAKAJIMA |
National Institute of Informatics
|
(Received: April 19, 2005) (Revised: July 12, 2005) (Accepted: July 13, 2005)
|
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.
|
Keywords:
Web service, BPEL, model checking, lightweight formal methods, EFA, SPIN
|
|
PDF(1,527KB) | References |
National Institute of Informatics is a member of CrossRef.
|