MVLSC Home · Issue Contents · Forthcoming Papers
Analysis of Concurrent Systems Based on Interval Order
Xu Yang and Chen Ye
One way to verify the concurrent system is to sort the read and write events and control events in the concurrent system according to the sequence relationship, either in a partial order, or in a strict order. Due to the concurrency of the events and the timing of the written data events, there is an overlap between the events, which requires an interval order for analysis. The order structure of the entire interval order is represented by the start and end sequences, and the order is observed for all equivalent interval orders. Mazurkiewicz traces, Comtraces are hierarchical traces, but neither can describe the interval trace. The petri interval trace with data is the technique to solve the problem in this paper, DPN, the Petri net with data, to describe the interval trace of read and write data. The method used is a BE (Beginnings and Endings) sequence to represent a class of runs based on the interval sequence. The case multi-threaded system represents the interval of writing events, and according to the unfolding of Petri net, the analysis of the running trace involved by read and write data events is successfully analyzed.
Keywords: Concurrent systems, Mazurkiewicz traces, interval order, Petri net with Data