Checking the Inconsistent Data in Concurrent Systems by Petri Nets with Data Operations
Dongming Xiang, Guanjun Liu, Chungang Yan, Changjun Jiang · 2016
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 new method 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.