Title :
Semantics based verification and synthesis of BPEL4WS abstract processes
Author :
Duan, Ziyang ; Bernstein, Arthur ; Lewis, Philip ; Lu, Shiyong
Author_Institution :
Dept. of Comput. Sci., SUNY, Stony Brook, NY, USA
Abstract :
We introduce a logic model to formally specify the semantics of workflows and their composite tasks described as BPEL4WS abstract processes. Based on the model, we present a set of inference rules to deduce the strongest postcondition and weakest precondition of a workflow and demonstrate that automatic workflow verification is possible due to the restrictions on data manipulation in an abstract process. We then sketch an algorithm that automatically synthesizes a workflow given its specification and a task library.
Keywords :
formal specification; inference mechanisms; logic programming; program verification; programming language semantics; workflow management software; BPEL4WS abstract processes; automatic workflow verification; data manipulation; formal specification; inference rules; logic model; semantics based synthesis; semantics based verification; task library; workflow postcondition; workflow precondition; workflow semantics; Art; Computational modeling; Computer science; Control system synthesis; Disaster management; Inference algorithms; Libraries; Logic; Web services; Workflow management software;
Conference_Titel :
Web Services, 2004. Proceedings. IEEE International Conference on
Print_ISBN :
0-7695-2167-3
DOI :
10.1109/ICWS.2004.1314805
