Detecting Data Inconsistency Based on the Unfolding Technique of Petri Nets

作者：Xiang, Dongming; Liu, Guanjun^*; Yan, Chungang; Jiang, Changjun^*

来源：IEEE Transactions on Industrial Informatics, 2017, 13(6): 2995-3005.

DOI：10.1109/TII.2017.2698640

• Business process modeling
• concurrent systems
• data inconsistency
• partial order
• Petri nets

The errors of data inconsistency occur in a concurrent system when some concurrent operations are conducted improperly. The model-checking technique is widely used to detect them based on the state transition graph. However, the state space explosion problem is the biggest obstacle for this technique, since the state transition graph is based on the interleaving semantics that can result in a rapid increase of the graph scale. In addition, data inconsistency is closely related with concurrent operations, but the state transition graph hardly characterizes concurrency due to its interleaving semantics. The unfolding technique of Petri nets can both alleviate the state explosion and characterize concurrency because it is based on the concurrent semantics. In this paper, we define Petri net with data to model concurrent systems with three kinds of data operations: read, write, and delete, and then formalize data inconsistency. We propose an unfolding method to produce a finite complete prefix (FCP) for each PD-net. Then, a matrix that represents all concurrency relations of transitions is constructed in view of FCP. Furthermore, the error of data inconsistency can be detected via this matrix. The related algorithms and the developed tool are introduced, and experiments illustrate their effectiveness and advantages. An example of industrial information system shows the usefulness of our study.

• 出版日期2017-12
• 单位同济大学