Detecting Data Inconsistency Based on the Unfolding Technique of Petri Nets
Detecting Data Inconsistency Based on the Unfolding Technique of Petri Nets
复制标题
基于Petri网展开技术的数据不一致检测
DOI：
10.1109/tii.2017.2698640
复制
发表时间：
2017-04
影响因子：
12.3
通讯作者：
CJ Jiang
中科院分区：
文献类型：
--
作者：
Dongming Xiang;Guanjun Liu;CG Yan;CJ Jiang
在并发系统中，由于某些并发操作不正确，导致数据不一致的错误。模型检查技术被广泛应用于基于状态转移图的检测。然而，状态空间爆炸问题是该技术的最大障碍，因为状态转移图是基于交错语义的，会导致图尺度的快速增加。此外，数据不一致性与并发操作密切相关，但状态转换图由于其交错语义而难以表征并发性。Petri网展开技术基于并发语义，既可以缓解状态爆炸，又可以表征并发性。本文定义了带数据的Petri网，对具有读、写、删除三种数据操作的并发系统进行建模，并形式化了数据不一致性。我们提出了一种为每个PD-net生成有限完全前缀（FCP）的展开方法。然后，根据FCP构造了一个表示所有转换并发关系的矩阵。此外，还可以通过该矩阵检测数据不一致的误差。介绍了相关算法和开发的工具，并通过实验验证了其有效性和优越性。一个工业信息系统的实例说明了本文研究的有效性。
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.
登录
查看更多内容
DOI：
10.1016/j.eswa.2016.08.006
发表时间：
2016-12
期刊：
Expert Syst. Appl.
影响因子：
--
作者：
M. Piltan;T. Sowlati
通讯作者：
M. Piltan;T. Sowlati
影响因子：
3.7
作者：
J. T. Butler;Tsutomu Sasao;M. Matsuura
通讯作者：
J. T. Butler;Tsutomu Sasao;M. Matsuura
DOI：
10.1145/1882291.1882301
发表时间：
2010-11
期刊：
--
影响因子：
--
作者：
Nishant Sinha;Chao Wang
通讯作者：
Nishant Sinha;Chao Wang
DOI：
--
发表时间：
2007-01
期刊：
--
影响因子：
--
作者：
Sarah L. Hickmott;J. Rintanen;S. Thiébaux;L. White
通讯作者：
Sarah L. Hickmott;J. Rintanen;S. Thiébaux;L. White
DOI：
10.1145/1805286.1805290
发表时间：
2010-07
期刊：
ACM J. Data Inf. Qual.
影响因子：
--
作者：
Hema S. Meda;A. K. Sen;A. Bagchi
通讯作者：
Hema S. Meda;A. K. Sen;A. Bagchi