摘要：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.
关键词：Web service; BPEL; model checking; lightweight formal methods; EFA; SPIN
Loading...
