
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

WFNet Based Modeling and Soundness Verification of Interworkflows
Shingo YAMAGUCHI Hajime MATSUO QiWei GE Minoru TANAKA
Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Vol.E90A
No.4
pp.829835 Publication Date: 2007/04/01 Online ISSN: 17451337
DOI: 10.1093/ietfec/e90a.4.829 Print ISSN: 09168508 Type of Manuscript: Special Section PAPER (Special Section on Selected Papers from the 19th Workshop on Circuits and Systems in Karuizawa) Category: Keyword: interworkflow, interoperability, workflow net, Petri net, soundness,
Full Text: PDF>>
Summary:
This paper deals with WFnet based modeling and verification of interorganizational workflows (interworkflows for short) based on the protocol of WfMC. In the protocol, there are three patterns of interoperability: Chained, Nested, and Parallel synchronized; and an interworkflow is constructed by using those interoperability patterns. We first give a WFnet based modeling method. In this modeling method, the three interoperability patterns are respectively expressed in terms of WFnets. They enable us to model a given interworkflow as a WFnet by connecting WFnets representing its constituent workflows. We also indicate that if free choice WFnets are connected by means of any combination of the three patterns then the resultant WFnet is asymmetric choice. Next we discuss verification of WFnets obtained through the modeling method. Intuitively, a WFnet is said to be sound if, for any case, the initial state is always transformed to the final state. Unfortunately, even if every constituent WFnet is sound FC, the resultant WFnet is not always sound. We give a sufficient condition of nonsoundness checkable in polynomial time. We also show that if they are connected by only the Nested pattern then the resultant WFnet is sound.

