Checking the Inconsistent Data in Concurrent Systems by Petri Nets with Data Operations
Checking the Inconsistent Data in Concurrent Systems by Petri Nets with Data Operations
复制标题
DOI：
10.1109/icpads.2016.0073
复制
发表时间：
2016-12
期刊：
影响因子：
--
通讯作者：
Dongming Xiang;Guanjun Liu;Chungang Yan;Changjun Jiang
中科院分区：
文献类型：
--
作者：
Dongming Xiang;Guanjun Liu;Chungang Yan;Changjun Jiang
一般的Petri网不适合模拟并发读和可覆盖写的数据操作。因此，定义了带数据操作的Petri网（PN-DO），它扩展了带有写弧和一些其他组件的上下文网络。定义了可达图的执行语义，提出了一种比传统可达图规模更小的可达图构造方法。基于这种可达性图，提出了一种检测数据不一致和缺失错误的方法。同时，通过实例分析说明了方法的有效性。
The general Petri nets are not suitable to model the data operations of concurrent read and coverable write. Therefore, Petri net with data operations (PN-DO) is defined, which extends contextual nets with write arcs and some other components. Its execution semantics are defined, and a newmethod is proposed to construct its reachability graph that is of a smaller scale than traditional reachability graph. Based on this kind of reachability graph, we propose a method to check the errors of inconsistent data and missing data. Meanwhile, case studies are given to illustrate the effectiveness of our methods.