Modeling and Analysis of Real-Time Cooperative Systems Using Petri Nets
Modeling and Analysis of Real-Time Cooperative Systems Using Petri Nets
复制标题
DOI：
10.1109/tsmca.2007.902622
复制
发表时间：
2007-09
期刊：
影响因子：
--
通讯作者：
Yuyue Du;Changjun Jiang;Mengchu Zhou
中科院分区：
文献类型：
--
作者：
Yuyue Du;Changjun Jiang;Mengchu Zhou
现有的形式化技术不适合对实时协同系统中传递值的不确定性和批处理功能进行优雅的建模。此外，系统的正确行为不仅取决于通过运行工作流获得的结果的逻辑正确性，还取决于在关键截止日期之前生产它们的时间。为此，本文提出了一个基于时间Petri网、工作流技术和时态逻辑的跨组织逻辑工作流网（ILWN），用于对实时协作系统进行建模和分析。通过对ILWN模型的某些行为附加逻辑表达式，减小了模型的规模。因此，ILWNs可以有效地缓解状态爆炸问题在一定程度上。此外，本文还分析了ILWNs的一个子类：或限制ILWNs的可靠性。给出了仅基于静态网结构的严格分析方法。本文提出的概念和技术，说明了在电子商务中的卖方-买方的例子。
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.