Semantics based verification and synthesis of BPEL4WS abstract processes
- 1 January 2004
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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
This publication has 2 references indexed in Scilit:
- LAO∗: A heuristic search algorithm that finds solutions with loopsArtificial Intelligence, 2001
- An axiomatic basis for computer programmingCommunications of the ACM, 1969