Reverse Unfolding of Petri Nets and its Application in Program Data Race Detection
Author:
Affiliation:

Clc Number:

Fund Project:

National Natural Science Foundation of China (61602279, 61472229); National Key Research and Development Plan (2016YFC0801406); Taishan Scholars Program of Shandong Province (ts20190936); Excellent Youth Innovation Team Foundation of Shandong Higher School (2019KJN024); Postdoctoral Innovation Foundation of Shandong Province (201603056); Shandong-Chongqing Science and Technology Cooperation Plan (cstc2020jscx-lyjsAX0008); Open Foundation of First Institute of Oceanography, MNR (2018002); Shandong University of Science and Technology Research Fund (2015TDJH102)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    The unfolding technique can partially alleviate the state explosion in Petri nets through branching processes. However, all states of a system are still contained in its unfolding net. To deal with some practical problems, only the coverability determination of a specific state is needed. In view of this, reducing the scale of the unfolding net is feasible. This study proposes a target-oriented reverse unfolding algorithm for the coverability determination of 1-safe Petri nets, which combines a heuristic technique to reduce the scale of unfolding nets, thereby improving the efficiency of coverability determination. Furthermore, the reverse unfolding is applied to the formal verification of concurrent programs, and their data race detection is converted into the coverability determination of a specific state in 1-safe Petri nets. The experiment compares the efficiency between forward nfolding and reverse unfolding in the coverability determination of a Petri net. The results show that when the Petri net has more forward branches than backward branches, reverse unfolding is more efficient than forward unfolding. Finally, the key factors influencing the efficiency of reverse unfolding are analyzed.

    Reference
    Related
    Cited by
Get Citation

Zongyin Hao, Faming Lu. Reverse Unfolding of Petri Nets and its Application in Program Data Race Detection. International Journal of Software and Informatics, 2021,11(4):405~428

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:
  • Revised:
  • Adopted:
  • Online: December 23,2021
  • Published: