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

fYear

2004

fDate

6-9 July 2004

Firstpage

734

Lastpage

737

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Web Services, 2004. Proceedings. IEEE International Conference on

Print_ISBN

0-7695-2167-3

Type

conf

DOI

10.1109/ICWS.2004.1314805

Filename

1314805