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:

    Unfolding technology can partially alleviate the state explosion problem in Petri net through branching processes. However, an unfolding still contains all states of a system. Some practical problems only need to determine the coverability of a specific state, which is expected to reduce the scale of unfolding net. This study proposes a target-oriented reverse unfolding algorithm for the coverability problem of 1-safe Petri nets, which combines heuristic technology to reduce the scale of unfolding nets, thereby improving the efficiency of coverability determination. Furthermore, the reverse unfolding technology is applied to the formal verification of concurrent programs, and the data race detection problem is converted into the coverability problem of a specific state in 1-safe Petri nets. The experiment compares the efficiency between forward unfolding and reverse unfolding in the coverability problem of 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

郝宗寅,鲁法明. Petri网的反向展开及其在程序数据竞争检测的应用.软件学报,2021,32(6):1612-1630

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 31,2020
  • Revised:October 26,2020
  • Adopted:
  • Online: February 07,2021
  • Published: June 06,2021
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063