TY - JOUR
T1 - Modeling and analysis of real-time cooperative systems using petri nets
AU - Du, Yu Yue
AU - Jiang, Chang Jun
AU - Zhou, Meng Chu
N1 - Funding Information:
Dr. Jiang received one international prize and six prizes of Science and Technology Advancement Awards from PRC Ministry of Education and provincial governments. He also received the awards of National Excellent Doctoral Dissertation, and Excellent Youth Teacher. He has been selected and supported by Encouragement Program for Teaching and Researching of Excellent Young Teacher of Ministry of Education and National Preeminent Youth Foundation.
Funding Information:
Manuscript received November 21, 2004; revised February 10, 2006. This work was supported in part by the “Taishan Scholar” Construction Project of Shandong Province, China; the National Natural Science Foundation of China under Grants 60573018, 60534060, and 60473094; the National Basic Research Program of China (973 Program) under Grants 2003CB316902, 2007CB316502, and 2004CB318001-03; the Open Project of the State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences under Grant SYSKF0604; and the Chang Jiang Scholars Program of PRC Ministry of Education. This paper was recommended by Associate Editor M. P. Fanti.
PY - 2007/9
Y1 - 2007/9
N2 - The existing formal techniques are not suitable for elegantly modeling passing value indeterminacy and describing batch processing function in real-time cooperative systems. Moreover, the correct behavior of the systems depends on not only the logical correctness of the results obtained through running workflows but also the time of producing them before critical deadlines. For these purposes, this paper proposes an interorganizational logical workflow net (ILWN) for modeling and analyzing real-time cooperative systems based on time Petri nets, workflow techniques, and temporal logic. Through attaching logical expressions to some actions of an ILWN model, the size of the model is reduced. Thus, ILWNs can efficiently mitigate the state explosion problem to some extent. Also, this paper analyzes the soundness of a subclass of ILWNs: The or-restricted ILWNs. A rigorous analysis approach is given based on their static net structures only. The concepts and techniques proposed in this paper are illustrated with a seller-buyer example in electronic commerce.
AB - The existing formal techniques are not suitable for elegantly modeling passing value indeterminacy and describing batch processing function in real-time cooperative systems. Moreover, the correct behavior of the systems depends on not only the logical correctness of the results obtained through running workflows but also the time of producing them before critical deadlines. For these purposes, this paper proposes an interorganizational logical workflow net (ILWN) for modeling and analyzing real-time cooperative systems based on time Petri nets, workflow techniques, and temporal logic. Through attaching logical expressions to some actions of an ILWN model, the size of the model is reduced. Thus, ILWNs can efficiently mitigate the state explosion problem to some extent. Also, this paper analyzes the soundness of a subclass of ILWNs: The or-restricted ILWNs. A rigorous analysis approach is given based on their static net structures only. The concepts and techniques proposed in this paper are illustrated with a seller-buyer example in electronic commerce.
KW - Interorganizational workflow
KW - Modeling
KW - Real-time cooperative system
KW - Temporal logic
KW - Time Petri net (TPN)
KW - Verification
KW - Workflow analysis
UR - https://www.scopus.com/pages/publications/34548319662
UR - https://www.scopus.com/pages/publications/34548319662#tab=citedBy
U2 - 10.1109/TSMCA.2007.902622
DO - 10.1109/TSMCA.2007.902622
M3 - Article
AN - SCOPUS:34548319662
SN - 1083-4427
VL - 37
SP - 643
EP - 654
JO - IEEE Transactions on Systems, Man, and Cybernetics Part A:Systems and Humans
JF - IEEE Transactions on Systems, Man, and Cybernetics Part A:Systems and Humans
IS - 5
ER -