In: Formal Methods and Software Engineering: 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003, pages 452-470. Volume 2885 of Lecture Notes in Computer Science --- Springer-Verlag, November 2003.
Abstract: The purpose of this paper is to provide the designers of cooperative workflows with a formalism that has a high expressive power and a strong theoretical basis. The existing techniques for correctness analysis of real-time cooperative systems, however, are not suitable to representing passing value indeterminacy and batch data processing function. Moreover, the correct behaviors of cooperative systems depend on not only the logical correctness of the results obtained but also the time of producing them before critical deadlines. To deal with previous problems, logical time Petri nets (LTPN) are first introduced based on time Petri nets and temporal logic. It can reduce the state explosion problem to a certain extent. Then logical time workflow nets (LTWN) and interorganizational LTWNs (ILTWN) are presented for specifying and verifying real-time cooperative systems. Their soundness properties are formally defined and analyzed. A rigorous approach for correctness analysis of ILTWNs is given based only on their static net structures. The use of our concepts and techniques is illustrated with a example of modeling and analysis of an offer-order-deliver-pay system.